rpms/alt-ergo
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
alt-ergo/README.md
Jerry James 4b29dc3ccc Version 2.3.0. 
New ocaml-alt-ergo-lib and ocaml-alt-ergo-parsers subpackages.
2021-12-30 17:12:44 -07:00

459 B
Raw Permalink Blame History

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.