On generating small clause normal forms

  • Andreas Nonnengart
  • Georg Rock
  • Christoph Weidenbach
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


In this paper we focus on two powerful techniques to obtain compact clause normal forms: Renaming of formulae and refined Skolemization methods. We illustrate their effect on various examples. By an exhaustive experiment of all first-order TPTP problems, it shows that our clause normal form transformation yields fewer clauses and fewer literals than the methods known and used so far. This often allows for exponentially shorter proofs and, in some cases, it makes it even possible for a theorem prover to find a proof where it was unable to do so with more standard clause normal form transformations.


Normal Form Automate Reasoning Automate Deduction Small Clause General Clause 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Thierry Boy de la Tour. An Optimality Result for Clause Form Translation. Journal of Symbolic Computation, 14:283–301, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Chin-Liang Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Computer Science and Applied Mathematics. Academic Press, 1973.Google Scholar
  3. 3.
    Li Dafa. The Formulation of the Halting Problem is Not Suitable for Describing the Halting Problem. Association for Automated Reasoning Newsletter, 27:1–7, 1994.Google Scholar
  4. 4.
    Ingo Dahn, J. Gehne, Thomas Honigmann, and Andreas Wolf. Integration of Automated and Interactive Theorem Proving in ILF. In Proceedings of the 14th International Conference on Automated Deduction, CADE-14, volume 1249 of LNAI,pages 57–60, Townsville, Australia, 1997. Springer.Google Scholar
  5. 5.
    Elmar Eder. Relative Complexities of First Order Calculi. Artificial Intelligence. Vieweg, 1992.Google Scholar
  6. 6.
    Uwe Egly. On the Value of Antiprenexing. In Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, volume 822 of LNAI, pages 69–83. Springer, July 1994.Google Scholar
  7. 7.
    Uwe Egly and Thomas Rath. The Halting Problem: An Automatically Generated Proof. AAR Newsletter, 30:10–16, 1995.Google Scholar
  8. 8.
    Uwe Egly and Thomas Rath. On the Practical Value of Different Definitional Translations to Normal Form. In M.A. McRobbie and J.K. Slaney, editors, 13th International Conference on Automated Deduction, CADE-13, volume 1104 of LNAI, pages 403–417. Springer, 1996.Google Scholar
  9. 9.
    Georg Gottlob and Alexander Leitsch. On the Efficiency of Subsumption Algorithms. Journal of the ACM, 32(2):280–295, 1985.CrossRefMathSciNetzbMATHGoogle Scholar
  10. 10.
    Donald W. Loveland. Automated Theorem Proving: A Logical Basis, volume 6 of Fundamental Studies in Computer Science. North-Holland, 1978.Google Scholar
  11. 11.
    William McCune and Larry Wos. Otter. Journal of Automated Reasoning,18(2):211–220, 1997.CrossRefGoogle Scholar
  12. 12.
    Andreas Nonnengart. Strong Skolemization. Technical Report MPI-I-96-2-010, Max-Planck-Institut für Informatik, Saarbrücken, Germany, 1996., submitted.Google Scholar
  13. 13.
    Hans Jürgen Ohlbach and Christoph Weidenbach. A Note on Assumptions about Skolem Functions. Journal of Automated Reasoning, 15(2):267–275, 1995.CrossRefMathSciNetzbMATHGoogle Scholar
  14. 14.
    Francis Jeffry Pelletier. Seventy-Five Problems for Testing Automatic Theorem Provers. Journal of Automated Reasoning, 2(2):191–216, 1986. Errata: Journal of Automated Reasoning, 4(2):235–236,1988.zbMATHMathSciNetGoogle Scholar
  15. 15.
    Francis Jeffry Pelletier and Geoff Sutcliffe. An Erratum for Some Errata to Automated Theorem Proving Problems. Association for Automated Reasoning Newsletter, 31:8–14, December 1995.Google Scholar
  16. 16.
    David A. Plaisted and Steven Greenbaum. A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation, 2:293–304, 1986.MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Georg Rock. Transformations of First-Order Formulae for Automated Reasoning.Diplomarbeit, Max-Planck-Institut für Informatik, Saarbrücken, Germany, April 1995. Supervisors: H.J. Ohlbach, C. Weidenbach.Google Scholar
  18. 18.
    Thoralf Skolem. Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer SÄtze nebst einem Theoreme über dichte Mengen. Skrifter utgit av Videnskappsellkapet i Kristiania, 4:4–36, 1920. Reprinted in: From Frege to Gödel, A Source Book in Mathematical Logic, 1879-1931, van Heijenoort, Jean, editor, pages 252–263, Harvard University Press, 1976.Google Scholar
  19. 19.
    Geoff Sutcliffe, Christian B. Suttner, and Theodor Yemenis. The TPTP Problem Library. In Alan Bundy, editor, Twelfth International Conference on Automated Deduction, CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, LNAI, pages 252–266, Nancy, France, June 1994. Springer.Google Scholar
  20. 20.
    G.S. Tseitin. On the complexity of derivations in propositional calculus. In A.O. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic.1968. Reprinted in: Automation of Reasoning: Classical Papers on Computational Logic, J. Siekmann and G. Wrightson, editors, pages 466–483, Springer, 1983.Google Scholar
  21. 21.
    Christoph Weidenbach, Bernd Gaede, and Georg Rock. SPASS & FLOTTER, Version 0.42. In M.A. McRobbie and J.K. Slaney, editors, 13th International Conference on Automated Deduction, CADE-13, volume 1104 of LNAI, pages 141–145.Springer, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Andreas Nonnengart
    • 1
  • Georg Rock
    • 2
  • Christoph Weidenbach
    • 1
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany
  2. 2.German Research Center for Artificial Intelligence GmbHSaarbrückenGermany

Personalised recommendations