logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving
Data.Logic.Harrison.Normal
Description
Versions of the normal form functions in Prop for FirstOrderFormula.
trivial :: (Negatable lit, Ord lit) => Set lit -> BoolSource
simpdnf :: (FirstOrderFormula fof atom v, Eq fof, Ord fof) => fof -> Set (Set fof)Source
simpdnf' :: forall lit fof atom v. (FirstOrderFormula fof atom v, Literal lit atom, Formula lit atom, Ord lit) => fof -> Set (Set lit)Source
simpcnf :: forall fof atom v. (FirstOrderFormula fof atom v, Ord fof) => fof -> Set (Set fof)Source
simpcnf' :: forall lit fof atom v. (FirstOrderFormula fof atom v, Literal lit atom, Ord lit) => fof -> Set (Set lit)Source