Summary

  1. Declaration of symbols. Declaration of the problem’s vocabulary: simple variables, uninterpreted and interpreted functions, as well as predicates.

  2. Native types and declaration of types Alt-Ergo comes with various built-in types, which correspond to theories handled by built-in solvers. The user can also declare new types thanks to Alt-Ergo’s rich and polymorphic type system à la ML.

  3. Declaration of axioms Specification of the problem’s structure: stating facts by declaring axioms

  4. Setting goals Defining what must be proven.

  5. Theories Alt-Ergo implements (semi-)decision procedures for various theories. It is possible to add new theories.

  6. Control Flow Specific constructs: if [...] then [...] else [...], let [...] in [...] or match [...] with [...]

  7. Syntax of declarations and expressions Additional information on Alt-Ergo’s syntax, defined in BNF. In particular, legal expressions are defined here.

Keywords

Reserved keywords are the following.

The list of all reserved keywords, in alphabetical order, is:

ac, and, axiom, bitv, bool, case_split, check, cut, distinct, else, end, exists, extends,
false, forall, function, goal, if, in, int, let, logic, not, xor, predicate, prop, 
real, rewriting, then, theory, true, type, unit, void, match, with, of

Note that preludes (additional theories which may be loaded) may reserve more keywords.