Using matings for pruning connection tableaux
Tableau calculi and the connection method are generally considered as related paradigms in automated deduction. However, in their essence, the frameworks are based on different concepts, and there is a large potential for cross-fertilization which is by far not exploited. In this paper, we demonstrate how the matings concept, which is central to the connection method framework, can be used to identify significant redundancies in the search for connection tableau proofs. The redundancies we discuss arise from the fact that different tableaux may encode the same mating. We concentrate on certain permutations of connection tableaux that occur when so-called reduction steps are performed in the tableau construction. Those permutations can be avoided without having to store the corresponding matings, which would be expensive. Instead the input formula is augmented with a literal ordering which is used in the connection tableau calculus to prune certain reduction steps. With this technique a significant reduction of the search space for almost every non-Horn formula can be achieved. Furthermore, the method can be implemented very easily and has almost no run-time overhead.
KeywordsReduction Step Automate Deduction Proof Search Connection Method Input Formula
Unable to display preview. Download preview PDF.
- 2.O. W. Astrachan and M. E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. Proceedings of the 11th Conference on Automated Deduction (CADE-11), LNAI 607, pages 224–238, Springer, 1992.Google Scholar
- 4.W. Bibel. Automated Theorem Proving. Vieweg, 2nd edition, 1987.Google Scholar
- 5.M. Fitting. First-Order Logic and Automated Theorem Proving, Springer, 2nd edition, 1996.Google Scholar
- 7.O. Ibens and R. Letz. Subgoal Alternation in Model Elimination. In Proceedings of TABLEAUX'97, LNAI 1227, pages 201–215, Springer, 1997.Google Scholar
- 10.R. Letz. First-Order Calculi and Proof Procedures for Automated Deduction. PhD thesis, Technische Hochschule Darmstadt, 1993 (http://wwwjessen.informatik.tu-muenchen.de/personen/letz.html).Google Scholar
- 12.R. Letz. Clausal Tableaux. In W. Bibel, P. H. Schmitt, editors, Automated Deduction. A basis for applications, Vol. 1, pages 39–68, Kluwer, 1998.Google Scholar
- 13.R. Letz. First-order Tableau Methods. In M. D'Agostino, D. Gabbay, R. HÄhnle, J. Posegga, editors, Handbook of Tableau Methods, Kluwer, 1998.Google Scholar
- 15.D. W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978.Google Scholar
- 18.S. Reeves. Semantic tableaux as a framework for automated theorem-proving. In C. S. Mellish and J. Hallam, editors, Advances in Artificial Intelligence (Proceedings of AISB-87), pages 125–139, Wiley, 1987.Google Scholar
- 19.R. M. Smullyan. First-Order Logic. Springer, 1968.Google Scholar