iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/BFB0054274
On generating small clause normal forms | SpringerLink
Skip to main content
Springer Nature Link
Log in

On generating small clause normal forms

  • Conference paper
  • First Online:
Automated Deduction — CADE-15 (CADE 1998)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1421))

Included in the following conference series:

Abstract

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.

This work was supported by the German science foundation program Deduktion.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Thierry Boy de la Tour. An Optimality Result for Clause Form Translation. Journal of Symbolic Computation, 14:283–301, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. 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. Elmar Eder. Relative Complexities of First Order Calculi. Artificial Intelligence. Vieweg, 1992.

    Google Scholar 

  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. Uwe Egly and Thomas Rath. The Halting Problem: An Automatically Generated Proof. AAR Newsletter, 30:10–16, 1995.

    Google Scholar 

  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. Georg Gottlob and Alexander Leitsch. On the Efficiency of Subsumption Algorithms. Journal of the ACM, 32(2):280–295, 1985.

    Article  MathSciNet  MATH  Google Scholar 

  10. Donald W. Loveland. Automated Theorem Proving: A Logical Basis, volume 6 of Fundamental Studies in Computer Science. North-Holland, 1978.

    Google Scholar 

  11. William McCune and Larry Wos. Otter. Journal of Automated Reasoning,18(2):211–220, 1997.

    Article  Google Scholar 

  12. Andreas Nonnengart. Strong Skolemization. Technical Report MPI-I-96-2-010, Max-Planck-Institut für Informatik, Saarbrücken, Germany, 1996.http://www.mpi-sb.mpg.de/~nonnenga/publications/, submitted.

    Google Scholar 

  13. Hans Jürgen Ohlbach and Christoph Weidenbach. A Note on Assumptions about Skolem Functions. Journal of Automated Reasoning, 15(2):267–275, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  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.

    MATH  MathSciNet  Google Scholar 

  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. David A. Plaisted and Steven Greenbaum. A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation, 2:293–304, 1986.

    Article  MathSciNet  MATH  Google Scholar 

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

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Institut für Informatik, Im Stadtwald, 66123, Saarbrücken, Germany

    Andreas Nonnengart & Christoph Weidenbach

  2. German Research Center for Artificial Intelligence GmbH, Stuhlsatzenhausweg 3, 66123, Saarbrücken, Germany

    Georg Rock

Authors
  1. Andreas Nonnengart
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Georg Rock
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christoph Weidenbach
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Claude Kirchner Hélène Kirchner

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nonnengart, A., Rock, G., Weidenbach, C. (1998). On generating small clause normal forms. In: Kirchner, C., Kirchner, H. (eds) Automated Deduction — CADE-15. CADE 1998. Lecture Notes in Computer Science, vol 1421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054274

Download citation

  • DOI: https://doi.org/10.1007/BFb0054274

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64675-4

  • Online ISBN: 978-3-540-69110-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation