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

Safe HaskellNone
LanguageHaskell98

Data.Logic.Harrison.Meson

Documentation

contrapositives :: forall fof atom v. (FirstOrderFormula fof atom v, Ord fof) => Set fof -> Set (Set fof, fof) Source

mexpand :: forall fof atom term v f. (FirstOrderFormula fof atom v, Literal fof atom, Term term v f, Atom atom term v, Ord fof) => Set (Set fof, fof) -> Set fof -> fof -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int)) -> (Map v term, Int, Int) -> Failing (Map v term, Int, Int) Source

puremeson :: forall fof atom term v f. (FirstOrderFormula fof atom v, Literal fof atom, Term term v f, Atom atom term v, Ord fof) => Maybe Int -> fof -> Failing ((Map v term, Int, Int), Int) Source

meson :: forall m fof atom term f v. (FirstOrderFormula fof atom v, PropositionalFormula fof atom, Literal fof atom, Term term v f, Atom atom term v, Ord fof, Monad m) => Maybe Int -> fof -> SkolemT v term m (Set (Failing ((Map v term, Int, Int), Int))) Source