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

Data.Logic.Harrison.Prop

# Documentation

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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