Data.Integer.Presburger

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

check :: Formula -> Bool

Check if a formula is true.

simplify :: Formula -> Formula

data Formula

Constructors

Formula :/\: Formula

Formula :\/: Formula

Formula :=>: Formula

Not Formula

Exists (Term -> Formula)

Forall (Term -> Formula)

TRUE

FALSE

Term :<: Term

Term :>: Term

Term :<=: Term

Term :>=: Term

Term :=: Term

Term :/=: Term

Integer :| Term

Instances

Show Formula

PP Formula

data Term

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.

Instances

Eq Term

Num Term

Show Term

PP Term

(.*) :: Integer -> Term -> Term

is_constant :: Term -> Maybe Integer

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 where

Methods

pp :: a -> Doc

Instances

PP Ex

PP NormProp

PP Form

PP Conn

PP Prop

PP Pred

PP PredSym

PP Term

PP Formula