toysolver-0.3.0: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Copyright(c) Masahiro Sakai 2011-2013
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

ToySolver.Data.FOL.Formula

Contents

Description

Formula of first order logic.

Synopsis

Overloaded operations for formula.

module ToySolver.Data.Boolean

Concrete formula

data Formula a Source

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

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

convert a formula into negation normal form