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

Safe HaskellNone

Data.Logic.Harrison.Resolution

Documentation

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

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

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

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

matchAtomsEq :: forall v f atom p term. (AtomEq atom p term, Term term v f) => Map v term -> atom -> atom -> Failing (Map v term)Source