Abstract
“prove ((E, F), A, B, C, D) : - !, prove (E, [F ∣ A], B, C, D).
prove ((E; F), A, B, C, D) : - !, prove (E, A, B, C, D), prove (F, A, B, C, D).
prove (all(H, I), A, B, C, D) : - !, ∖+ length (C, D), copy_term ((H, I, C), (G, F, C)), append (A, [all (H, I)], E), prove(F, E, B, [G ∣ C], D).
prove (A,_, [C ∣ D] ,_, _) :-((A= − (B); − (A) = B)) -> (unify(B, C); prove (A, [], D,_,_)).
prove (A, [E ∣ F], B, C, D): - prove (E, F, [A∣B], C,D).”
implements a first-order theorem prover based on free-variable semantic tableaux. It is complete, sound, and efficient.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Basin, D., Fronhöfer, B., Hähnle, R., Posegga, J., and Schwind, C.: 2nd Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Techical Report 213, Max-Planck-Institut für Informatik, Saarbrücken, Germany, May 1993.
Heckert, B. and Hähnle, R.: An improved method for adding equality to free variable semantic tableaux, in D. Kapur (ed.),11th Int. Conf. on Automated Deduction (CADE), Lecture Notes in Computer Science, Springer-Verlag, Albany, NY, 1992, pp. 507–521.
Beckert, B., Gerberding, S., Hähnle, R., and Kernig, W.: The tableau-based theorem prover3 T A P for multiple-valued logics, in11th Int. Conf. on Automated Deducation (CADE), Lecture Notes in Computer Science, Springer-Verlag, Albany, NY, 1992, pp. 758–760.
Beckert, B., Hähnle, R., and Schmitt, P. H.: The even more liberalized δ-rule in free variable semantic tableaux, in G. Gottlob, A. Leitsch, and D. Mundici (eds),3rd Kurt Gödel Colloquium (KGC), Lecture Notes in Computer Science, Springer-Verlag, Brno, Czech Republic, 1993, pp. 108–119.
Broda, K., D'Agostino, M., Goré, R., Johnson, R., and Reeves, S.: 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Technical Report TR-94/5, Imperial College London, Department of Computing, London, England, April 1994.
Eder, E.:Relative Complexities of First-Order Calculi. Artificial Intelligence. Vieweg-Verlag, 1992.
Fitting, M. C.:First-Order Logic and Automated Theorem Proving, Springer-Verlag, 1990.
Fronhöfer, B., Hähnle, R., and Käufl, T.: Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Technical Report 8/92, Universität Karlsruhe, Fakultät für Informatik, Karlsruhe, Germany, March 1992.
Hilbert, D. and Bernays, P.:Grundlagen der Mathematik II, Vol. 50 of Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, Springer-Verlag, 1939.
Käufl, T. and Zabel, N.: Cooperation of decision procedures in a tableau-based theorem prover,Revude d'Intelligence Artificielle 4(3) (1990).
Letz, R., Schumann, J., Bayerl, S., and Bibel, W.: SETHEO: A high-performance theorem prover,J. Automated Reasoning 8(2) (1992), 183–212.
Manthey, R. and Bry, F.: SATCHMO: A theorem power implemented in Prolog, in E. Lusk and R. Overbeek (eds),9th Int. Conf. on Automated Deducation (CADE), Lecture Notes in Computer Science, Springer-Verlag, Argonne, IL, 1988, pp. 415–434.
McCune, W. W.: Otter 2.0 Users Guide, Technical Report ANL-90/9, Argonne National Laboratory, Mathematics and Computer Science Division, Argonne, IL, March 1990.
O'Keefe, R. A.:The Craft of Prolog, MIT Press, 1990.
Oppacher, F. and Suen, E.: HARP: A tableau-based theorem prover,J. Automated Reasoning 4 (1988), 69–100.
Pelletier, F. J.: Seventy-five problems for testing automatic theorem provers,J. Automated Reasoning 2 (1986), 191–216.
Posegga, J.: Compiling proof search in semantic tableaux, in7th Int. Symp. on Methodologies for Intelligent Systems (ISMIS), Lecture Notes in Computer Science, Springer-Verlag, Trondheim, Norway, 1993, pp. 67–77.
Posegga, J.:Deduktion mit Shannongraphen für Prädikatenlogik erster Stufe, Infix-Verlag, St. Augustin, Germany, 1993.
Prawitz, D., Prawitz, H., and Voghera, N.: A mechanical proof procedure and its realization in an electronic computer,ACM 7(1–2) (1960) 102–128.
Schmitt, P. H.: The THOT Theorem Prover, Technical Report 87.9.7, IBM Germany, Scientific Center, Heidelberg, Germany, 1987.
Schönfeld, W.: Prolog extensions based on tableau calculus, in9th Int. Joint Conf. on Artificial Intelligence, Los Angeles, Vol. 2, 1985, pp. 730–733.
Stickel, M. E.: A Prolog technology theorem prover, in E. Lusk and R. Overbeek (eds),9th Int. Conf. on Automated Deducation (CADE), Lecture Notes in Computer Science, Springer-Verlag, Argonne, IL, 1988, pp. 752–753.
Wang, H.: Toward mechanical mathematics,IBM J. Research and Development 4(1) (1960).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Beckert, B., Posegga, J. leanTAP: Lean tableau-based deduction. J Autom Reasoning 15, 339–358 (1995). https://doi.org/10.1007/BF00881804
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00881804