Safe Haskell | None |
---|---|
Language | Haskell98 |
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 Failing (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 Source #
tab :: (IsFirstOrder formula, Unify Failing (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) Source #
testTableaux :: Test Source #