Data.Logic.ATP.Resolution

Resolution.

Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

Documentation

match_atoms :: (JustApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> (atom, atom) -> Failing (Map v term)

match_atoms_eq :: (HasEquate atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> (atom, atom) -> Failing (Map v term)

resolution1 :: forall m fof atom term v function. (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))

resolution2 :: forall fof atom term v function m. (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))

With deletion of tautologies and bi-subsumption with "unused".

resolution3 :: forall fof atom term v function m. (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))

Introduce a set-of-support restriction.

presolution :: forall fof atom term v function m. (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool))

Positive (P1) resolution.

davis_putnam_example_formula :: Formula

Simple example that works well.

testResolution :: Test