Alt-ergo is an automatic theorem prover geared towards application in program verification. it is based on cc(x), a congruence closure algorithm parameterized by an equational theory x. alt-ergo has built-in provers for propositional logic, linear arithmetic, uninterpreted function symbols, associative-commutative function symbols, polymorphic arrays, user-defined polymorphic record types and polymorphic enumeration types. it has restricted support for reasoning over arbitrary user-defined algebraic types, first-order quantifiers, and non-linear arithmetic.

this package contains the development libraries that are useful when writing ocaml programs linking to the alt-ergo api.