| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Logic.ATP.Resolution
Description
Resolution.
Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
Synopsis
- 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 Failing (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 Failing (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))
- resolution3 :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (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))
- presolution :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (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))
- davis_putnam_example_formula :: Formula
- testResolution :: Test
Documentation
match_atoms :: (JustApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> (atom, atom) -> Failing (Map v term) Source #
match_atoms_eq :: (HasEquate atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> (atom, atom) -> Failing (Map v term) Source #
resolution1 :: forall m fof atom term v function. (IsFirstOrder fof, Unify Failing (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)) Source #
resolution2 :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (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)) Source #
With deletion of tautologies and bi-subsumption with "unused".
resolution3 :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (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)) Source #
Introduce a set-of-support restriction.
presolution :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (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)) Source #
Positive (P1) resolution.
davis_putnam_example_formula :: Formula Source #
Simple example that works well.