Advertisement

A Generalized Factorization Rule Based on the Introduction of Skolem Terms

  • Uwe Egly
Conference paper
Part of the Informatik-Fachberichte book series (INFORMATIK, volume 287)

Abstract

In this paper, we describe a factorization rule which is based on the introduction of Skolem terms. This rule generalizes non-unifiable terms to a new term not occurring elsewhere in the clause set. Clauses of the form p(x,t 1) ˅ p(y,t 2) are factorized to p(x,m) where t 1 t 2 are ground terms and m is a new constant not occurring in the Herbrand universe of the original clause set. A refutation of p(x,m) implies a refutation of p(x,t 1) ˅ p(y,t 2) but not vice versa. We extend this factorization rule in several ways and show that the application of such rules may increase the performance of automated theorem provers. A linear resolution proof of exponential length may collapse into a linear resolution proof of linear length.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Baaz and Leitsch, 1985]
    M. Baaz and A. Leitsch. Die Anwendung starker Reduktionsregeln in automatischen Beweisen. Proc. of the Austrian Acad, of Science II, 194:287–307, 1985. In German.MathSciNetzbMATHGoogle Scholar
  2. [Baaz and Leitsch, 1989]
    M. Baaz and A. Leitsch. A Strong Reduction Method for Clause Logic. Technical Report 8901, Technische Universität Wien, Institut für Computersprachen, Abteilung für Anwendungen der Formalen Logik, Getreidemarkt 9, A-1060 WIEN, Austria, 1989.Google Scholar
  3. [Baaz and Leitsch, 1990]
    M. Baaz and A. Leitsch. A Strong Problem Reduction Method Based on Function Introduction. In ISSAC 90, pages 30–37. ACM-Press, 1990.CrossRefGoogle Scholar
  4. [Baaz and Leitsch, 1991]
    M. Baaz and A. Leitsch. Complexity of Resolution Proofs and Function Introduction. Technical Report TR-9101, Technische Universität Wien, Institut für Computersprachen, Abteilung für Anwendungen der Formalen Logik, Getreidemarkt 9, A- 1060 WIEN, Austria, 1991.Google Scholar
  5. [Bibel, 1987]
    W. Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, second edition, 1987.Google Scholar
  6. [Bledsoe, 1971]
    W. W. Bledsoe. Splitting and Reduction Heuristics in Automatic Theorem Proving. Artificial Intelligence, 2:57–78, 1971.CrossRefGoogle Scholar
  7. [Chang and Lee, 1973]
    C. L. Chang and R. C. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.Google Scholar
  8. [Egly, 1990]
    U. Egly. Problem-Reduction Methods and Clause Splitting in Automated Theorem Proving. Master#x0027;s thesis, Technische Universität Wien, Institut für Computersprachen, Abteilung für Anwendungen der Formalen Logik, Getreidemarkt 9, A-1060 WIEN, 1990.Google Scholar
  9. [Letz et al., 1991]
    R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETIIEO — A high-performance theorem prover for first-order logic. Journal of Automated Reasoning, 1991.Google Scholar
  10. [Neugebauer and Schaub, 1991]
    G. Neugebauer and T. Schaub. A pool-based connection calculus. Technical Report AIDA-91–2, FG Intellektik, FB Informatik, TH Darmstadt, Alexanderstraße 10, D-6100 Darmstadt, January 1991.Google Scholar
  11. [Pelletier, 1986]
    F. J. Pelletier. Seventy-Five Problems for Testing Automatic Theorem Provers. Journal of Automated Reasoning, 2:191–216., 1986.MathSciNetzbMATHCrossRefGoogle Scholar
  12. [Schumann et al, 1989]
    J. Schumann, N. Trapp, and M. van der Koelen. SETHEO/PARTHEO Users Manual. Report FKI-121–89, Institut für Informatik, Technische Universität München, Arcisstr. 21, D-8000 München 2, Germany, December 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Uwe Egly
    • 1
  1. 1.FG Intellektik / FB InformatikTH DarmstadtDarmstadtDeutschland

Personalised recommendations