Data.Logic.ATP.Meson

Model elimination procedure (MESON version, based on Stickel's PTTP).

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

Documentation

meson1 :: forall m fof atom predicate term function v. (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))

meson2 :: forall m fof atom term function v. (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 ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))

meson :: (IsFirstOrder fof, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))

testMeson :: Test