foliage

First-order logic with integer arithmetics

This crate provides an abstract syntax tree for first-order formulas with integer arithmetics.

Supported Formulas

• Booleans values (true and false)
• predicates
• negated formulas
• comparisons of terms (<, ≤, >, ≥, =, ≠)
• implications and biconditionals
• conjunctions and disjunctions of formulas
• existentially and universally quantified formulas

Supported 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)