logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Portability portable experimental Sebastian Fischer (sebf@informatik.uni-kiel.de) Safe-Inferred

Data.Boolean

Description

This library provides a representation of boolean formulas that is used by the solver in Data.Boolean.SatSolver.

We also define a function to simplify formulas, a type for conjunctive normalforms, and a function that creates them from boolean formulas.

Synopsis

# Documentation

data Boolean Source

Boolean formulas are represented as values of type `Boolean`.

Constructors

 Var Int Variables are labeled with an `Int`, Yes `Yes` represents true, No `No` represents false, Not Boolean `Not` constructs negated formulas, Boolean :&&: Boolean and finally we provide conjunction Boolean :||: Boolean and disjunction of boolean formulas.

Instances

 Show Boolean

data Literal Source

Literals are variables that occur either positively or negatively.

Constructors

 Pos Int Neg Int

This function returns the name of the variable in a literal.

This function negates a literal.

This predicate checks whether the given literal is positive.

type CNF = [Clause]Source

Conjunctive normalforms are lists of lists of literals.

We convert boolean formulas to conjunctive normal form by pushing negations down to variables and repeatedly applying the distributive laws.