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