Existential and universal quantification used redundant data
representations, while they actually share the same structure. This
unifies both into a single QuantifiedFormula type.
For convenience, support biconditionals with more than one argument.
An n-ary “if and only if” statement
F_1 <-> F_2 <-> ... <-> F_n
is to be interpreted as
F_1 <-> F_2 and F2 <-> F3 and ... and F_(n - 1) <-> F_n
This provides an abstract syntax tree for first-order logic with integer
arithmetics. Initially, the following types of formulas are supported:
- Booleans values (true and false)
- predicates
- negated formulas
- comparisons of terms (<, ≤, >, ≥, =, ≠)
- implications and biconditionals
- conjunctions and disjunctions of formulas
- existentially and universally quantified formulas
In addition, these types of terms are provided:
- 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)
Patrick Lühne