Data.Logic.ATP.Tableaux

Tableaux, seen as an optimized version of a Prawitz-like procedure.

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

Documentation

prawitz :: forall formula atom term function v. (IsFirstOrder formula, Ord formula, Unify (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => formula -> Int

newtype K

Constructors

K Int

Instances

Enum K

Eq K

Ord K

Show K

Pretty K

tab :: (IsFirstOrder formula, Unify (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => Maybe Depth -> formula -> Failing ((K, Map v term), Depth)

testTableaux :: Test