@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Name: 3TAP
Keywords: free-variable semantic tableaux, first-order, many-valued,
automatic, equality, sorted terms
Description:
Semantics: Finitely-valued first-order logic with quasi-classical quantifiers,
sorted terms, and (in the two-valued version) equality.
The syntax is based on that of first-order logic in a very
natural notation. Translation tools from TPTP format exist.
No normal form is required. In particular,
equalities may occur everywhere within a formula.
The prover is easily adaptable to any finitely-valued logic
involving arbitrary connectives, provided the truth tables
of the connectives are given.
Deductive machinery: Free-variable semantic tableaux using the sets-as-
signs approach and various other strategies for
shortening proofs such as analytic cut, and a
liberalized delta-rule.
Dynamics: 3TAP's user interface is the Prolog shell enriched with certain
predicates for proving theorems, loading databases etc.
A graphical interface will be soon available.
The tableau proofs are built automatically.
Persistence: Proofs and traces of proof searches can be saved.
Contact persons: Reiner Haehnle, Bernhard Beckert
University of Karlsruhe
Institute for Logic, Complexity and Deduction Systems
Kaiserstrasse 12
D-76128 Karlsruhe, Germany
Email: {haehnle,beckert}@ira.uka.de
Phone: +49 721 6084324
Fax: +49 721 6084329
User group: There is no user group. Latest information can be obtained from
the 3TAP homepage: http://i12www.ira.uka.de/~threetap/
Pragmatics: To our best knowledge 3TAP is the first and only automated
theorem prover capable of dealing with arbitrary many-valued
logics. Moreover, experiments suggest that its twovalued version
(and therefore also the many-valued version) does perform not too
bad if compared to conventional theorem provers.
In addition, 3TAP is the first prover that handles reasonably well
first-order logic with unrestricted equality, where no normal
form is required and equalities can occur everywhere in a formula.
It can however not compete with completion-based systems or
resolution with paramodulation.
Documentation: A handbook [1] is available, that includes a user's manual
and a description of 3TAP's source code. It is distributed
together with 3TAP and is also available separately from
the contact persons or via WWW: http://i12www.ira.uka.de/~threetap/
See [2] for more information on tableau-based theorem proving
in many-valued logics.
[1] Reiner Haehnle, Bernhard Beckert, Stefan Gerberding.
The many-valued tableau-based theorem
prover 3TAP. Tech Report 30/94, Institute for Logic, Complexity
and Deduction Systems, University of Karlsruhe, Germany, 1994.
[2] Reiner Haehnle. Automated Proof Search in Multiple Valued
Logics. Oxford University Press, 1994.
Applications: Most applications of 3TAP have been of an experimental nature.
The two substantial efforts, to date, have been hardware
verification using a seven-valued logic [3] and experiments
with a three-valued axiomatization of interval arithmetic [4].
3TAP's equality module has been used as part of a proof
procedure for nonmonotonic reasoning [5]. Recently, (the
two-valued version of) 3TAP is used as part of the interactive
program verification system KIV to enhance the degree of automation.
[3] Reiner Haehnle and Werner Kernig. Verification of switch-
level designs with many-valued logics. In Proceedings,
LPAR '93, St. Petersburg, Springer, LNCS, 1993.
[4] Stefan Gerberding. Monomorphe Axiomatisierung von
Intervallarithmetik mit mehrwertigen Logiken. Master's
thesis, University of Karlsruhe, Department of Computer
Science, 1991.
[5] Sven Lorenz. A tableau prover for domain minimization.
In Proceedings, 2nd Workshop on Theorem Proving with
Analytic Tableaux and Related Methods, Marseille,
Max-Planck-Institut fuer Informatik, MPI-I-92-213,
Saarbruecken, March 1993.
Extensions/enhancements: 3TAP is still being improved as part of a project
at the University of Karlsruhe, that is funded by
the Deutsche Forschungsgemeinschaft.
Objective of this project is to refine proof
methods based on semantic tableaux, i.e., to add
new features and to increase their efficiency.
Resource requirements: The implementation language of 3TAP is Prolog
with a very small amount of portable C. It is easy to
install 3TAP on a Unix machines where Sicstus Prolog
Version 2.1.9 or Quintus Prolog 3.x and an
ANSI C compiler are available.
To achieve acceptable performance, at least 8MB main
memory and 20MB swap space should be configured.
Where-to-get-it: The 3TAP source code and handbook is available via WWW:
http://i12www.ira.uka.de/~threetap/
Bernhard Beckert
Reiner Haehnle
July 31, 1995
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%