Advertisement

Using matings for pruning connection tableaux

  • Reinhold Letz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)

Abstract

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.

Keywords

Reduction Step Automate Deduction Proof Search Connection Method Input Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    P. Andrews. Theorem Proving via General Matings. Journal of the Association for Computing Machinery, 28(2):193–214, 1981.zbMATHMathSciNetGoogle Scholar
  2. 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
  3. 3.
    W. Bibel. On Matrices withConnections. Journal of the ACM, 28:633–645, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    W. Bibel. Automated Theorem Proving. Vieweg, 2nd edition, 1987.Google Scholar
  5. 5.
    M. Fitting. First-Order Logic and Automated Theorem Proving, Springer, 2nd edition, 1996.Google Scholar
  6. 6.
    J. D. Horton and B. Spencer. Clause trees: a tool for understanding and implementing resolution in automated deduction. Artificial Intelligence, 92:25–89, 1997.CrossRefMathSciNetzbMATHGoogle Scholar
  7. 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
  8. 8.
    R. A. Kowalski and D. Kuehner. Linear Resolution with Selection Function. Artificial Intelligence, 2:227–260, 1970.CrossRefMathSciNetGoogle Scholar
  9. 9.
    R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8(2):183–212, 1992.CrossRefMathSciNetzbMATHGoogle Scholar
  10. 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
  11. 11.
    R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableaux Calculi. Journal of Automated Reasoning, 13:297–337, 1994.CrossRefMathSciNetzbMATHGoogle Scholar
  12. 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. 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
  14. 14.
    D. W. Loveland. Mechanical Theorem Proving by Model Elimination. Journal of the ACM, 15(2):236–251, 1968.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    D. W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978.Google Scholar
  16. 16.
    M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, K. Mayr. SETHEO and E-SETHEO. Journal of Automated Reasoning, 18:237–246, 1997.CrossRefGoogle Scholar
  17. 17.
    D. Prawitz. An Improved Proof Procedure. Theoria, 26:102–139, 1960.zbMATHMathSciNetCrossRefGoogle Scholar
  18. 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. 19.
    R. M. Smullyan. First-Order Logic. Springer, 1968.Google Scholar
  20. 20.
    M. A. Stickel. A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning, 4:353–380, 1988.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Reinhold Letz
    • 1
  1. 1.Institut für InformatikTechnische UniversitÄt MünchenMünchenGermany

Personalised recommendations