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

Safe HaskellNone
LanguageHaskell98

Data.Logic.Harrison.Normal

Description

Versions of the normal form functions in Prop for FirstOrderFormula.

Documentation

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

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