Data.Logic.Harrison.Prop

Documentation

eval :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Map atomic Bool -> Bool

atoms :: Ord atomic => PropositionalFormula formula atomic => formula -> Set atomic

onAllValuations

Arguments

:: Ord a

=> (r -> r -> r)

Combine function for result type

-> (Map a Bool -> r)

The substitution function

-> Map a Bool

The default valuation function for atoms not in ps

-> Set a

The variables to vary

-> r

type TruthTable a = ([a], [TruthTableRow])

type TruthTableRow = ([Bool], Bool)

truthTable :: forall formula atom. (PropositionalFormula formula atom, Eq atom, Ord atom) => formula -> TruthTable atom

tautology :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Bool

unsatisfiable :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Bool

satisfiable :: (PropositionalFormula formula atomic, Ord atomic) => formula -> Bool

rawdnf :: PropositionalFormula formula atomic => formula -> formula

purednf :: (PropositionalFormula pf atom, Literal lit atom, Ord lit) => pf -> Set (Set lit)

dnf :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, Ord lit) => Set (Set lit) -> pf

dnf' :: forall pf atom. (PropositionalFormula pf atom, Literal pf atom) => pf -> pf

trivial :: (Literal lit atom, Ord lit) => Set lit -> Bool

psimplify :: forall formula atomic. (PropositionalFormula formula atomic, Eq formula) => formula -> formula

nnf :: (PropositionalFormula formula atomic, Eq formula) => formula -> formula

simpdnf :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, Ord lit) => pf -> Set (Set lit)

simpcnf :: (PropositionalFormula pf atom, Literal lit atom, Ord lit) => pf -> Set (Set lit)

positive :: Literal lit atom => lit -> Bool

negative :: forall lit atom. Literal lit atom => lit -> Bool

negate :: PropositionalFormula formula atomic => formula -> formula

distrib :: PropositionalFormula formula atomic => formula -> formula

list_disj :: PropositionalFormula formula atomic => Set formula -> formula

list_conj :: (PropositionalFormula formula atomic, Ord formula) => Set formula -> formula

pSubst :: (PropositionalFormula formula atomic, Ord atomic) => Map atomic formula -> formula -> formula

dual :: forall formula atomic. PropositionalFormula formula atomic => formula -> formula

nenf :: (PropositionalFormula formula atomic, Eq formula) => formula -> formula

mkLits :: (PropositionalFormula formula atomic, Ord formula, Ord atomic) => Set formula -> Map atomic Bool -> formula

allSatValuations :: Ord a => (Map a Bool -> Bool) -> Map a Bool -> Set a -> [Map a Bool]

dnf0 :: forall formula atomic. (PropositionalFormula formula atomic, Ord atomic, Ord formula) => formula -> formula

cnf :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, Ord lit) => Set (Set lit) -> pf

cnf' :: forall pf atom. (PropositionalFormula pf atom, Literal pf atom) => pf -> pf