"De l'audace, encore de l'audace, et toujours de l'audace!" - Danton
It is perhaps as difficult to induce a computer to 'reason logically' as it is to induce a human to do so. The Tau theorem prover and knowledge base (a formal theory repository), is aiming to be the first interactive, easy-to-use, and comprehensive prover of its kind on the Internet. Tau is sound and theoretically complete for the First Order Predicate Calculus with Identity -- a phrase which can cover a multitude of sins, due to the undecidabilability of FOPC. Tau's syntax is full FOPC with sentential constants, relation symbols, function symbols, complex terms, and identity.
Tau accepts both a prefix version of FOL, called KIF (Knowledge Interchange Format), and an infix form of FOL.
Tau KIF is a Lisp-like, S-Expression prefix syntax based on the KIF 3 standard. Details of KIF 3 are available at the Knowledge Interchange Format home page. An HTML conversion of the TeX original from the preceding page is here: KIF Manual.
The other concrete syntax is the Tau infix version of KIF, which is consistent with typical conventions used in ASCII computer settings. Both of these concrete syntaxes are intended for situations where no special logic symbols are available. Our architecture admits unlimited additional concrete syntaxes, including those which include proper mathematical and logical symbology such as TeX or MathML; we intend to incorporate graphical notations and I/O into Tau.
(<=>
(exists ?Y
(and
(forall ?X
(<=>
(f ?X)
(= ?X ?Y)))
(g ?Y)))
(and
(exists ?Y
(forall ?X
(<=>
(f ?X)
(= ?X ?Y))))
(forall ?X
(=>
(f ?X)
(g ?X)))))
You can run a Tau proof of this theorem by clicking 'Prove' at TheoremSample1
Variables in KIF are preceded by a '?'; individual constants, predicates, relations, and functions may be a single alpha character or a string of such. Computer generated individual constants appearing in proofs are preceded by a '$'.
You can also see the trace of Tau's proof of this theorem at T324-PP.html. That page shows a verbose trace of Tau's actions in proving this theorem. The proof trace shows how the theorem was broken down into sub-proofs and how the formulas were rewritten and normalized to facilitate the proof. More concise proof display options are available.
Tau proofs are based upon proof-by-contradiction using a resolution (model elimination) strategy, and the proof displays are not informative in the way a natural deduction style of presentation is, e.g. We intend later to expose more of the proof structure which is currently hidden.
Other examples with which to try Tau:
We've been using theorems from Kalish and Montague, Logic [1964], (through the chapter on identity) for many of our basic tests. The test directory is at: samples.
Tau is written in the Java programming language and uses the Tomcat server. The logic employed by Tau is based upon finding proofs by contradiction, using a variant of the Model Elimination methodolgy of Loveland, which is augmented by rewriting strategies. Identity is implemented in Tau by a variant of Brand transformations.
Tau is intended for experimentation and educational use. It can be used as a proof assistant and teaching aid.
KIF (Knowledge Interchange Format) is essentially a (parenthesized) prefix version of common first-order logical notation. Being of prefix form, it is efficient for many computer applications and for that reason we adopted KIF as Tau's first internal language. Tau also has an infix version. For further details, please see:
The Tau prover is a hybrid which is indirect, at its core, and operates by saturation of the quantified formulas in the proof, and unification/resolution. Overlaid upon this methodology lies an extensible sequent-style strategizer
Tau is based on:
Compare the remarks of Bachmair and Ganzinger in the Handbook of Automated Reasoning, "Resolution Theorem Proving":
"It has been pointed out that a weakness of resolution is its lack of goal orientation. Simplification and clause elimination based on redundancy helps ameliorate the problem, but one might also consider possible combinations of resolution with such goal-oriented methods as the sequent calculus or semantic tableux. Semantic tableux and variants thereof, including the Davis-Putnam method, model elimination and SL-resolution can be viewed as tree-like theorem proving process in which the limits of the individual branches are saturated under (ordered) resolution with selection. This view may serve as a basis for further investigations of the combination problem." P. 94, Vol. 1, Handbook of Automated Reasoning, emphasis added.
Tau's use of Model Elimination in conjunction with selection heuristics and proof strategizing helps overcome some of the difficulties resulting from a lack of goal-directedness.
Our primary emphasis is on the logical soundness of the proof method and the integrity of the software design. We have a good deal of control/flexibility in choosing proof strategies, and over the presentations and annotations.
Tau is an ongoing project and its authors plan to follow several paths, including:
- Updating the documentation, much of which reflects our earliest work on Tau. (Documentation always lags:).
- Implementation of HOL and the use of theorem schemata
- Implementation of sequent style proofs (work now underway)
- TPTP testing
- Graphical notations
- KB persistence across sessions
Bachmair, Leo and Harald Ganzinger. "Equational reasoning in saturation based theorem proving". In Wolfgang Bibel and Peter H. Schmidt, editors, Automated Deduction: A Basis for Applications. Volume I, Foundations: Calculi and Methods, pages 353–398. Kluwer Academic Publishers, Dordrecht, 1998.
Brand, Daniel. "Proving theorems with the modification method". SIAM Journal on Computing, 4(4):412–430, 1975.
BundyAlan. "The Automation of Proof by Mathematical Induction". Handbook of Automated Reasoning 2001: 845-911
Chang, C.L., and R. C. T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973.
Degtyarev, Anatoli and Andrei Voronkov. "Equality reasoning in sequent-based calculi". In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 1999.
Hooker, J.N. "Solving the incremental satisfiability problem", Journal of Logic Programming 15 (1993) 177-186.
Hooker, J.N. "New methods for computing inferences in first order logic", Annals of Operations Research (1993) 479-492.
Inoue, K. "Linear resolution for consequence finding". Artificial Intelligence, 56:301--353, 1992.
Loveland, D.W.“A simplified format for the model elimination procedure,” Journal of the Association for Computing Machinery, Vol. 15, No. 2, 1969, pp. 349-363.
Loveland, D.W. "Mechanical theorem-proving by model elimination," Journal of the ACM, 15(2):236-251, April 1968.
Loveland, D.W. Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, 1978.
Martelli, Alberto and Ugo Montanari: An Efficient Unification Algorithm. ACM Trans. Program. Lang. Syst. 4(2): 258-282 (1982)
Martelli, A., and Montanari, U. "Theorem proving with structure sharing and efficient unification". Internal Rep. S-77-7, Ist. di Scienze della Informazione, University of Pisa, Pisa, Italy; also in Proceedings of the 5th International Joint Conference on Artificial Intelligence, Boston, 1977, p. 543.
Robinson, J.A. "A machine-oriented logic based on the resolution principle". Jour. Assoc. for Comput. Mach., 1965, 23-41.
Robinson, J.A. "Computational logic: The unification computation". In Machine Intelligence, vol. 6, B. Meltzer and D. Michie (Eds.). Edinburgh Univ. Press, Edinburgh, Scotland, 1971, pp. 63-72.
Stickel, M.E. "A Prolog technology theorem prover". New Generation Computing, 1984, 371-383.
Enjoy,