@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%