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 v term, 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 v term, 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