ToySolver.Data.FOL.Formula

Formula of first order logic.

Overloaded operations for formula.

module ToySolver.Data.Boolean

Concrete formula

data Formula a

formulas of first order logic

Constructors

T

F

Atom a

And (Formula a) (Formula a)

Or (Formula a) (Formula a)

Not (Formula a)

Imply (Formula a) (Formula a)

Equiv (Formula a) (Formula a)

Forall Var (Formula a)

Exists Var (Formula a)

Instances

Eq a => Eq (Formula a)

Ord a => Ord (Formula a)

Show a => Show (Formula a)

Boolean (Formula c)

Complement (Formula a)

Variables a => Variables (Formula a)

IsRel (Expr c) (Formula (Atom c))

pushNot :: Complement a => Formula a -> Formula a

convert a formula into negation normal form