Alt-Ergo’s native language

This page documents Alt-Ergo’s native input language and its syntax.

In order to state a problem, the user may enrich the signature of the theory by adding new symbols and types, using keywords such as logic and type. Axioms can be declared through the axiom construct, and goals are set with goal. Additional constructs allow to define theories or to use if-then-else, let-bindings or pattern-matching. A full description of the syntax is available in the last chapter.

• Summary
  • Keywords
• Declaration of symbols
  • logic: uninterpreted symbols
  • ac modifier: associative and commutative symbols
  • function: user-defined functions
  • predicate: propositional valued functions
• Types
  • Built-in types
  • Built-in operators
  • User-defined
• Declaration of axioms
  • axiom
  • Triggers
  • rewriting
• Setting goals
  • goal
  • Intermediate goals: cut and check
  • check_sat
• Theories
  • Native theories
  • Floating-point Arithmetic
  • User-defined extensions of theories
• Control Flow
  • let [...] in
  • match [...] with
  • if [...] then [...] else
• Syntax of declarations and expressions