Package alt-ergo

Automated theorem prover including linear arithmetic

https://alt-ergo.ocamlpro.com/

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.

Version: 2.4.3

General Commands
alt-ergo	Execute Alt-Ergo on the given file.

General Commands