Hyper Tableau — The Next Generation
“Hyper tableau” is a sound and complete calculus for first-order clausal logic. The present paper introduces an improvement which removes the major weakness of the calculus, which is the need to (at least partially) blindly guess ground-instantiations for certain clauses. This guessing is now replaced by a unification-driven technique.
The calculus is presented in detail, which includes a completeness proof. Completeness is proven by using a novel approach to extract a model from an open branch. This enables semantical redundancy criteria which are not present in related approaches.
Unable to display preview. Download preview PDF.
- [AB97]Chandrabose Aravindan and Peter Baumgartner. A Rational and Efficient Algorithm for View Deletion in Databases. In Jan Maluszynski, editor, Logic Programming-Proceedings of the 1997 International Symposium, Port Jefferson, New York, 1997. The MIT Press.Google Scholar
- [BFFN97]Peter Baumgartner, Peter Fröhlich, Ulrich Furbach, and Wolfgang Nejdl. Semantically Guided Theorem Proving for Diagnosis Applications. In 15th International Joint Conference on Artificial Intelligence (IJCAI 97), pages 460–465, Nagoya, 1997. International Joint Conference on Artificial Intelligence.Google Scholar
- [BFN96]Peter Baumgartner, Ulrich Furbach, and Ilkka Niemelä. Hyper Tableaux. In Proc. JELIA 96, number 1126 in Lecture Notes in Aritificial Intelligence. European Workshop on Logic in AI, Springer, 1996.Google Scholar
- [BHOS96]Bernhard Beckert, Reiner Hähnle, Peter Oel, and Martin Sulzmann. The tableau-based theorem prover 3 T A P, version 4.0. In Proceedings, 13th International Conference on Automated Deduction (CADE), New Brunswick, NJ, USA, volume 1104 of Lecture Notes in Computer Science, pages 303–307. Springer, 1996.Google Scholar
- [Bil96]Jean-Paul Billon. The Disconnection Method. In U. Moscato, D. Mundici, and M. Ornaghi, editors. Theorem Proving with Analytic Tableaux and Related Methods, number 1071 in Lecture Notes in Artificial Intelligence. 1996 Miglioli et al. [MMMO96].Google Scholar
- [CL73]C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.Google Scholar
- [FH91]H. Fujita and R. Hasegawa. A Model Generation Theorem Prover in KL1 using a Ramified-Stack Algorithm. In Proc. of the Eigth International Conference on Logic Programming, pages 535–548, Paris, France, 1991.Google Scholar
- [Fit90]M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.Google Scholar
- [KH94]Stefan Klingenbeck and Reiner Hähnle. Semantic tableaux with ordering restrictions. In A. Bundy, editor, Proc. CADE-12, volume 814 of LNAI, pages 708–722. Springer, 1994.Google Scholar
- [Küh97]Michael Kühn. Rigid Hypertableaux. In Proc. of KI’ 97, Lecture Notes in Aritificial Intelligence. Springer, 1997.Google Scholar
- [Lei97]Alexander Leitsch. The Resolution Calculus. Springer, 1997.Google Scholar
- [LMG94]R. Letz, K. Mayr, and C. Goller. Controlled Integrations of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, 13, 1994.Google Scholar
- [MB88]Rainer Manthey and François Bry. SATCHMO: a theorem prover implemented in Prolog. In Ewing Lusk and Ross Overbeek, editors, Proceedings of the 9 th Conference on Automated Deduction, Argonne, Illinois, May 1988, volume 310 of Lecture Notes in Computer Science, pages 415–434. Springer, 1988.Google Scholar
- [MMMO96]P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors. Theorem Proving with Analytic Tableaux and Related Methods, number 1071 in Lecture Notes in Artificial Intelligence. Springer, 1996.Google Scholar
- [Nie96]Ilkka Niemelä. A Tableau Calculus for Minimal Model Reasoning. In U. Moscato, D. Mundici, and M. Ornaghi, editors. Theorem Proving with Analytic Tableaux and Related Methods, number 1071 in Lecture Notes in Artificial Intelligence. 1996 Miglioli et al. [MMMO96].Google Scholar