How To Install alt-ergo on Fedora 36

In this tutorial we learn how to install alt-ergo in Fedora 36. alt-ergo is Automated theorem prover including linear arithmetic

Introduction

In this tutorial we learn how to install alt-ergo on Fedora 36.

What is alt-ergo

Alt-Ergo is an automated theorem prover implemented in OCaml. It is based on CC(X) - a congruence closure algorithm parameterized by an equational theory X. This algorithm is reminiscent of the Shostak algorithm. Currently CC(X) is instantiated by the theory of linear arithmetics. Alt-Ergo also contains a home made SAT-solver and an instantiation mechanism by which it fully supports quantifiers.

We can use yum or dnf to install alt-ergo on Fedora 36. In this tutorial we discuss both methods but you only need to choose one of method to install alt-ergo.

Install alt-ergo on Fedora 36 Using dnf

Update yum database with dnf using the following command.

sudo dnf makecache --refresh

After updating yum database, We can install alt-ergo using dnf by running the following command:

sudo dnf -y install alt-ergo

Install alt-ergo on Fedora 36 Using yum

Update yum database with yum using the following command.

sudo yum makecache --refresh

After updating yum database, We can install alt-ergo using yum by running the following command:

sudo yum -y install alt-ergo

How To Uninstall alt-ergo on Fedora 36

To uninstall only the alt-ergo package we can use the following command:

sudo dnf remove alt-ergo

alt-ergo Package Contents on Fedora 36

/usr/bin/alt-ergo
/usr/lib/.build-id
/usr/lib/.build-id/d2
/usr/lib/.build-id/d2/82fe5195d258dc79088fdec51ce69b8e13a1c2
/usr/lib64/ocaml/alt-ergo
/usr/lib64/ocaml/alt-ergo/META
/usr/lib64/ocaml/alt-ergo/dune-package
/usr/lib64/ocaml/alt-ergo/opam
/usr/lib64/ocaml/alt-ergo/plugins
/usr/lib64/ocaml/alt-ergo/preludes
/usr/lib64/ocaml/alt-ergo/preludes/b-set-theory-prelude-2018-09-28.ae
/usr/lib64/ocaml/alt-ergo/preludes/fpa-theory-2017-01-04-16h00.why
/usr/share/doc/alt-ergo
/usr/share/doc/alt-ergo/Alt-Ergo--Atelier-B--RSSR-2016.pdf
/usr/share/doc/alt-ergo/Alt-Ergo-2.2--SMT-Workshop-2018.pdf
/usr/share/doc/alt-ergo/CHANGES
/usr/share/doc/alt-ergo/README.md
/usr/share/doc/alt-ergo/examples
/usr/share/doc/alt-ergo/examples/AB-Why3-plugin
/usr/share/doc/alt-ergo/examples/AB-Why3-plugin/p4_34.why
/usr/share/doc/alt-ergo/examples/invalid
/usr/share/doc/alt-ergo/examples/invalid/arith1.why
/usr/share/doc/alt-ergo/examples/invalid/arith2.why
/usr/share/doc/alt-ergo/examples/invalid/arrays.why
/usr/share/doc/alt-ergo/examples/invalid/bitv.why
/usr/share/doc/alt-ergo/examples/lib_usage.ml
/usr/share/doc/alt-ergo/examples/valid
/usr/share/doc/alt-ergo/examples/valid/ac_arith.why
/usr/share/doc/alt-ergo/examples/valid/arith1.why
/usr/share/doc/alt-ergo/examples/valid/arith2.why
/usr/share/doc/alt-ergo/examples/valid/arith3.why
/usr/share/doc/alt-ergo/examples/valid/arith4.why
/usr/share/doc/alt-ergo/examples/valid/arrays.why
/usr/share/doc/alt-ergo/examples/valid/bitv.why
/usr/share/doc/alt-ergo/examples/valid/congruence.why
/usr/share/doc/alt-ergo/examples/valid/enum_arrays.why
/usr/share/doc/alt-ergo/examples/valid/quantifiers.why
/usr/share/licenses/alt-ergo
/usr/share/licenses/alt-ergo/COPYING.md
/usr/share/licenses/alt-ergo/LICENSE.md
/usr/share/licenses/alt-ergo/License.OCamlPro
/usr/share/man/man1/alt-ergo.1.gz

References

Summary

In this tutorial we learn how to install alt-ergo on Fedora 36 using yum and [dnf]((/fedora/36/dnf/).