This module implements Cooper's algorithm for deciding first order formulas over integers with addition.
Based on the paper: * author: D.C.Cooper * title: Theorem Proving in Arithmetic without Multiplication * year: 1972
Documentation
Terms of Presburger arithmetic.
Term are created by using the Num
class.
WARNING: Presburger arithmetic only supports multiplication
by a constant, trying to create invalid terms will result
in a run-time error. A more type-safe alternative is to
use the '(.*)' operator.