Declaration of symbols. Declaration of the problem’s vocabulary: simple variables, uninterpreted and interpreted functions, as well as predicates.
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.
Declaration of axioms Specification of the problem’s structure: stating facts by declaring axioms
Setting goals Defining what must be proven.
Theories Alt-Ergo implements (semi-)decision procedures for various theories. It is possible to add new theories.
Control Flow Specific constructs:
if [...] then [...] else [...],
let [...] in [...]or
match [...] with [...]
Reserved keywords are the following.
Constant and operators for propositions are available:
false. The construct
distinctis available for all types. Quantifiers
existscan be used.
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.