Advertisement

Hyper Tableau — The Next Generation

  • Peter Baumgartner
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)

Abstract

“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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [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
  2. [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
  3. [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
  4. [BG94]
    Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [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
  6. [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
  7. [BP95]
    Bernhard Beckert and Joachim Posegga. leanT A P: Lean tableau-based deduction. Journal of Automated Reasoning, 15(3):339–358, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  8. [Bra76]
    D. Brand. Analytic Resolution in Theorem Proving. Artificial Intelligence, 7:285–318, 1976.zbMATHCrossRefMathSciNetGoogle Scholar
  9. [CL73]
    C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.Google Scholar
  10. [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
  11. [Fit90]
    M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.Google Scholar
  12. [Joy76]
    W.H. Joyner. Resolution Strategies as Decision Procedures. Journal of the ACM, 23(3):396–417, 1976.MathSciNetGoogle Scholar
  13. [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
  14. [Küh97]
    Michael Kühn. Rigid Hypertableaux. In Proc. of KI’ 97, Lecture Notes in Aritificial Intelligence. Springer, 1997.Google Scholar
  15. [Lei97]
    Alexander Leitsch. The Resolution Calculus. Springer, 1997.Google Scholar
  16. [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
  17. [LP92]
    S.-J. Lee and D. Plaisted. Eliminating Duplicates with the Hyper-Linking Strategy. Journal of Automated Reasoning, 9:25–42, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  18. [LRW95]
    D. Loveland, D. Reed, and D. Wilson. SATCHMORE: SATCHMO with RElevance. Journal of Automated Reasoning, 14:325–351, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  19. [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
  20. [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
  21. [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
  22. [OS88]
    F. Oppacher and E. Suen. HARP: A Tableau-Based Theorem Prover. Journal of Automated Reasoning, 4:69–100, 1988.CrossRefMathSciNetGoogle Scholar
  23. [Rob65]
    J. A. Robinson. Automated deduction with hyper-resolution. Internat. J. Comput. Math., 1:227–234, 1965.zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Peter Baumgartner
    • 1
  1. 1.Institut für InformatikUniversität KoblenzKoblenzGermany

Personalised recommendations