alt-ergo - Alt-Ergo automatic theorem prover
| Website: | http://alt-ergo.lri.fr |
|---|---|
| License: | CeCILL-C |
| Vendor: | Fedora Project |
- Description:
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.
Packages
| alt-ergo-0.8-5.fc11.src [111 KiB] |
Changelog
by Fedora Release Engineering (2009-02-23):
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild |