Automated theorem prover library
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. This package is the core of Alt-Ergo as an OCaml library.
Release | Stable | Testing |
---|---|---|
Fedora Rawhide | 2.3.3-22.fc41 | - |
Fedora 41 | 2.3.3-22.fc41 | - |
Fedora 40 | 2.3.3-17.fc40 | - |
Fedora 39 | 2.3.3-10.fc39 | - |
You can contact the maintainers of this package via email at
alt-ergo dash maintainers at fedoraproject dot org
.