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

Safe HaskellNone
LanguageHaskell98

Data.Logic.Harrison.DefCNF

Documentation

data Atom a Source

Constructors

P a 

Instances

class NumAtom atom where Source

Methods

ma :: N -> atom Source

ai :: atom -> N Source

Instances

mkprop :: forall pf atom. (PropositionalFormula pf atom, NumAtom atom) => N -> (pf, N) Source

maincnf :: (NumAtom atom, PropositionalFormula pf atom) => (pf, Map pf pf, Int) -> (pf, Map pf pf, Int) Source

defstep :: (PropositionalFormula pf atom, NumAtom atom, Ord pf) => (pf -> pf -> pf) -> (pf, pf) -> (pf, Map pf pf, Int) -> (pf, Map pf pf, Int) Source

max_varindex :: NumAtom atom => atom -> Int -> Int Source

mk_defcnf :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => ((pf, Map pf pf, Int) -> (pf, Map pf pf, Int)) -> pf -> Set (Set lit) Source

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

subcnf :: (PropositionalFormula pf atom, NumAtom atom) => ((pf, Map pf pf, Int) -> (pf, Map pf pf, Int)) -> (pf -> pf -> pf) -> pf -> pf -> (pf, Map pf pf, Int) -> (pf, Map pf pf, Int) Source

orcnf :: (NumAtom atom, PropositionalFormula pf atom) => (pf, Map pf pf, Int) -> (pf, Map pf pf, Int) Source

andcnf :: (PropositionalFormula pf atom, NumAtom atom, Ord pf) => (pf, Map pf pf, Int) -> (pf, Map pf pf, Int) Source

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

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

andcnf3 :: (PropositionalFormula pf atom, NumAtom atom, Ord pf) => (pf, Map pf pf, Int) -> (pf, Map pf pf, Int) Source

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