Tableau-based Theorem Prover
is a many-valued tableau-based
theorem prover developed at the University of Karlsruhe. It can be
instantiated for arbitrary finitely-valued first-order logics, and it
can handle equality (two-valued), sorts, and non-clausal input.
A 190 page handbook (PDF) is available. It provides a user's manual, describes 's implementation, and documents the
history and development of .
A system abstract has been published at CADE 1992:
The Many-Valued Tableau-Based Theorem Prover 3TAP (System Abstract)
Bernhard Beckert, Stefan Gerberding, Reiner Hähnle,
& Werner Kernig
Proceedings, 11th International Conference on Automated Deduction
(CADE), Albany/NY, USA.
PDF
- BibTeX
A lot of papers, reports, and other publications have been written in
connection with , describing its
various features and theoritical advances that have been made during its
development. Most of these publications are available via the WWW.
Please refer to the author's web pages:
can handle full
two-valued first-order logic with equality and sorted
terms and many-valued first-order logic with
quasi-classical quantifiers. The prover is adaptable to any
finitely-valued logic involving arbitrary connectives within a few
hours, provided the truth tables of the connectives are given. Sorted
terms and two-valued equality are still available with many-valued
logics.
Various strategies that may shorten proofs such as
lemma generation are implemented and may optionally be switched on in
all versions.
For equality handling in the two-valued version, uses a completion-based method to
solve mixed universal and rigid E-unification problems, that are
extracted from tableau branches. (The implementation of this method for
equality handling can be used stand-alone.)
In the two-valued version a restricted version of the
dissolution inference rule of Murray & Rosenthal is
implemented and may optionally be switched on.
The implementation language of is Prolog (there are versions for Quintus Prolog and for
SICStus Prolog) with a
small amount of portable C. Parts of 's compiler module and of the utilities for visualizing
proofs are written using the Unix tools Lex and Yacc (resp. Flex and
Bison). The design of is as modular as possible. Thus, it should be easy
to port it to other architectures and to add new features.
The user interface of is the Prolog shell enriched with certain predicates for
proving theorems, loading databases etc. This has the advantage that the
user can quickly write his own predicates on top of these to accomplish
specialized tasks. Moreover, it is very easy to integrate into any existing system via its
interface predicates. An X-Windows based interface is currently under
development.
The syntax of databases is based on that of first-order
predicate logic in a very natural notation. No normal form is
required. In particular, equalities may occur in arbitrary places within
a formula.
A format
file is available for converting problems taken from the TPTP
library into syntax
(using the program tptp2x, which is part of the TPTP distribution).
The source code of Version
3.0 is availble as a compressed
TAR-file (315K).
Once you have uploaded and uncompressed the TAR-file
threetap.tar.gz on your local disk, use the shell command
for unpacking. A directory
threetap containing the source code will be
generated. Follow the instructions in the file README to install .
Do not hesitate to contact us if you are looking for any information you
cannot find on these pages, or should you have any further questions,
suggestions, or comments.
Finally, if should you do something interesting with , please inform us. This could
be modifying or extending the program, applying it to some domain, or
whatever. We appreciate feedback.
Reiner Hähnle
Chalmers University of Technology
Email: reiner@cs.chalmers.se
Maintainer: Bernhard Beckert