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.

• To add new uninterpreted symbols (variables or functions) to the signature: logic and the ac modifier for associative and commutative symbols.

• Interpreted functions: function and predicate.

• Built-in types: int, real, bool, prop, unit, bitv, farray.

• Constant and operators for propositions are available: and, or, xor, not, true, false. The construct distinct is available for all types. Quantifiers forall and exists can be used.

• To create new types: type. They keyword of is useful when dealing with structured datatypes, which include records, enums and algebraic datatypes.

• To declare new axioms: axiom, and the special case rewriting.

• To define goals that must be proven valid: goal. cut and check can create intermediate goals that won’t interact with other goals through triggers.

• New theories may be defined using theory (and the keywords extends and end). Inside theories, axiom can be used with additional triggers. The construct case_split is also available.

• Other useful constructs are let […] in, match […] with […] end and if […] then […] else […].

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

ac, and, axiom, bitv, bool, case_split, check, check_sat, chevk_valid, 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.