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

Safe HaskellNone
LanguageHaskell98

Data.Logic.Harrison.Prop

Documentation

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

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

onAllValuations Source

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]) Source

type TruthTableRow = ([Bool], Bool) Source

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

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

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

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

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

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) -> pf Source

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

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

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

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

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 -> Bool Source

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

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

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

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

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

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

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

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

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

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 -> formula Source

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

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