License	GNU LGPLv3
Maintainer	paul.bittner@uni-ulm.de
Safe Haskell	Safe

Propositions

Description

Definition and operations of propositional logic.

Synopsis

data PropositionalFormula a
- = PTrue
- | PFalse
- | PVariable a
- | PNot (PropositionalFormula a)
- | PAnd [PropositionalFormula a]
- | POr [PropositionalFormula a]
type Assignment a = a -> Bool
eval :: Assignment a -> PropositionalFormula a -> Bool
liftBool :: Bool -> PropositionalFormula a
isPTrue :: PropositionalFormula a -> Bool
isPFalse :: PropositionalFormula a -> Bool
isLiteral :: PropositionalFormula a -> Bool
isCNF :: PropositionalFormula a -> Bool
toCNF :: PropositionalFormula a -> PropositionalFormula a
lazyToCNF :: PropositionalFormula a -> PropositionalFormula a
toCNFClauseList :: PropositionalFormula a -> [PropositionalFormula a]
toDNFClauseList :: PropositionalFormula a -> [PropositionalFormula a]
toNNF :: PropositionalFormula a -> PropositionalFormula a
cartesianOr :: [PropositionalFormula a] -> [PropositionalFormula a] -> [PropositionalFormula a]
simplify :: PropositionalFormula a -> PropositionalFormula a
clausifyCNF :: Show a => (a -> a) -> (() -> a) -> PropositionalFormula a -> [[a]]

Documentation

data PropositionalFormula a Source #

Sum type similar to a grammar for building propositional formulas.

Constructors

PTrue
PFalse
PVariable a
PNot (PropositionalFormula a)
PAnd [PropositionalFormula a]
POr [PropositionalFormula a]

Instances

Instances details

Functor PropositionalFormula Source #
Instance details Defined in Propositions Methods fmap :: (a -> b) -> PropositionalFormula a -> PropositionalFormula b (<$) :: a -> PropositionalFormula b -> PropositionalFormula a
Eq a => Eq (PropositionalFormula a) Source #
Instance details Defined in Propositions Methods (==) :: PropositionalFormula a -> PropositionalFormula a -> Bool (/=) :: PropositionalFormula a -> PropositionalFormula a -> Bool
Show a => Show (PropositionalFormula a) Source #	UTF-8 characters for printing propositional operators.
Instance details Defined in Propositions Methods showsPrec :: Int -> PropositionalFormula a -> ShowS show :: PropositionalFormula a -> String showList :: [PropositionalFormula a] -> ShowS
Logic (PropositionalFormula a) Source #	`PropositionalFormula`s form a `Logic`.
Instance details Defined in Propositions Methods ltrue :: PropositionalFormula a Source # lfalse :: PropositionalFormula a Source # lvalues :: [PropositionalFormula a] Source # lnot :: PropositionalFormula a -> PropositionalFormula a Source # land :: [PropositionalFormula a] -> PropositionalFormula a Source # lor :: [PropositionalFormula a] -> PropositionalFormula a Source # limplies :: PropositionalFormula a -> PropositionalFormula a -> PropositionalFormula a Source # lequals :: PropositionalFormula a -> PropositionalFormula a -> PropositionalFormula a Source # leval :: (PropositionalFormula a -> PropositionalFormula a) -> PropositionalFormula a -> PropositionalFormula a Source #

type Assignment a = a -> Bool Source #

An assignment for propositional formulas, assigns variables to boolean values.

eval :: Assignment a -> PropositionalFormula a -> Bool Source #

Evaluates a propositional formula with the given variable assignment.

liftBool :: Bool -> PropositionalFormula a Source #

Converts boolean values to their respective symbols in our definition of propositional logic.

isPTrue :: PropositionalFormula a -> Bool Source #

Returns true iff the given propositional formula is the value PTrue.

isPFalse :: PropositionalFormula a -> Bool Source #

Returns true iff the given propositional formula is the value PFalse.

isLiteral :: PropositionalFormula a -> Bool Source #

Returns true iff the given propositional formula is a literal.

isCNF :: PropositionalFormula a -> Bool Source #

Returns true iff the given propositional formula is in conjunctive normal form.

toCNF :: PropositionalFormula a -> PropositionalFormula a Source #

Converts the given propositional formula to conjunctive normal form.

lazyToCNF :: PropositionalFormula a -> PropositionalFormula a Source #

Converts the given propositional formula to conjunctive normal form if it is not already in that form.

toCNFClauseList :: PropositionalFormula a -> [PropositionalFormula a] Source #

Converts a PropositionalFormula in conjunctive normal form to a list of its clauses. The original formula can be reconstructed with PAnd (toClauseList x). Assumes that the given formula is in CNF.

toDNFClauseList :: PropositionalFormula a -> [PropositionalFormula a] Source #

Converts a PropositionalFormula in disjunctive normal form to a list of its clauses. Assumes that the given formula is in DNF.

toNNF :: PropositionalFormula a -> PropositionalFormula a Source #

Converts a PropositionalFormula to negation normal form.

cartesianOr :: [PropositionalFormula a] -> [PropositionalFormula a] -> [PropositionalFormula a] Source #

Returns a list of disjunctions such that all possible combinations of the formulas in the input lists are considered. Like the cartesian product but instead of pairs (x, y) we produce POr [x, y].

simplify :: PropositionalFormula a -> PropositionalFormula a Source #

Simplifies the given PropositionalFormula with some basic rules (e.g., PNot PTrue -> PFalse).

clausifyCNF :: Show a => (a -> a) -> (() -> a) -> PropositionalFormula a -> [[a]] Source #

Transforms a PropositionalFormula in CNF to a list of its clauses. Assumes that the given formula is in CNF.

The first argument is a functions resolving negation, i.e. it should take an a and give its negated version.
The second argument is a function creating the value of type a that should be associated with false (PFalse). For example, 0 could represent false in propositional formulas over numerals. (Note, if no such value exists, the false function is free to produce an error.)
The third argument is the function in CNF that should be clausified.

If still confused, try the following call and look at the result: show $ clausifyCNF (x -> "not "++x) "false" (toCNF p) where p is a propositional formula over strings.