This provides an abstract syntax tree for first-order logic with integer arithmetics.
Initial features
Formulas
- Booleans values (
true
andfalse
) - predicates
- negated formulas
- comparisons of terms (<, ≤, >, ≥, =, ≠)
- implications and biconditionals
- conjunctions and disjunctions of formulas
- existentially and universally quantified formulas
Terms
- Boolean values (true and false)
- integers
- strings
- special integers (infimum and supremum)
- symbolic functions
- variables
- binary operations (addition, subtraction, multiplication, division,
modulo, exponentiation) - unary operations (absolute value, numeric negation)