presburger-0.3: Cooper's decision procedure for Presburger arithmetic.



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



check :: Formula -> BoolSource

Check if a formula is true.

data Term Source

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.


is_constant :: Term -> Maybe IntegerSource

Check if a term is a constant (i.e., contains no variables). If so, then we return the constant, otherwise we return Nothing.

class PP a whereSource


pp :: a -> DocSource


PP Ex 
PP NormProp 
PP Form 
PP Conn 
PP Prop 
PP Pred 
PP PredSym 
PP Term 
PP Formula