Skip to main content
SpringerLink
Log in

Incremental Closure of Free Variable Tableaux

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2001)

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

Included in the following conference series:

Abstract

This paper presents a technique for automated theorem proving with free variable tableaux that does not require backtracking. Most existing automated proof procedures using free variable tableaux require iterative deepening and backtracking over applied instantiations to guarantee completeness. If the correct instantiation is hard to find, this can lead to a significant amount of duplicated work. Incremental Closure is a way of organizing the search for closing instantiations that avoids this inefficiency.

Acknowledgments

I thank Wolfgang Ahrendt, Elmar Habermalz, Reiner Hähnle and the anonymous referees for their numerous and helpful comments on drafts of this paper.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Peter Baumgartner. Hyper Tableaux — The Next Generation. In Harrie de Swart, editor, Proc. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands, number 1397 in LNCS, pages 60–76. Springer-Verlag, 1998.

    Google Scholar 

  2. Bernhard Beckert. A completion-based method for mixed universal and rigid E-unification. In Alan Bundy, editor, Proc. 12th Conf. on Automated Deduction CADE, Nancy/France, LNAI 814, pages 678–692. Springer, 1994.

    Google Scholar 

  3. Bernhard Beckert. Depth-first proof search without backtracking for free variable clausal tableaux. In P. Baumgartner and H. Zhang, editors, 3rd Int. Workshop on First-Order Theorem Proving (FTP), St. Andrews, Scotland, TR 5/2000 Univ. of Koblenz, pages 44–55, 2000.

    Google Scholar 

  4. Peter Baumgartner, Norbert Eisinger, and Ulrich Furbach. A confluent connection calculus. In Harald Ganzinger, editor, Proc. 16th International Conference on Automated Deduction, CADE-16, Trento, Italy, volume 1632 of LNCS, pages 329–343. Springer-Verlag, 1999.

    Google Scholar 

  5. Peter Baumgartner, Ulrich Furbach, and Ilkka Niemelä. Hyper tableaux. In José Júlio Alferes, Luís Moniz Pereira, and Ewa Orlowska, editors, Proc. European Workshop: Logics in Artificial Intelligence, JELIA, volume 1126 of LNCS, pages 1–17. Springer-Verlag, 1996.

    Chapter  Google Scholar 

  6. Bernhard Beckert and Reiner Hähnle. Analytic tableaux. In W. Bibel and P. Schmitt, editors, Automated Deduction: A Basis for Applications, volume I, chapter 1, pages 11–41. Kluwer, 1998.

    Google Scholar 

  7. Jean-Paul Billon. The disconnection method: a confluent integration of unification in the analytic framework. In P. Miglioli et al., editor, Theorem Proving with Tableaux and Related Methods, TABLEAUX’96, Terrasini, Italy, volume 1071 of LNCS, pages 110–126. Springer-Verlag, 1996.

    Google Scholar 

  8. Bernhard Beckert and Joachim Posegga. leanTAP: Lean tableau-based theorem proving. extended abstract. In Alan Bundy, editor, Proceedings, 12th International Conference on Automated Deduction (CADE), Nancy, France, volume 814 of LNCS 814, pages 793–797. Springer-Verlag, 1994.

    Google Scholar 

  9. Hubert Comon. Disunification: a survey. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, chapter 9, pages 322–359. MIT Press, Cambridge, MA, USA, 1991.

    Google Scholar 

  10. Martin Giese. A first-order simplification rule with constraints. In Peter Baumgartner and Hantao Zhang, editors, 3rd Int. Workshop on First-Order Theorem Proving (FTP), St. Andrews, Scotland, TR 5/2000 Univ. of Koblenz, pages 113–121, 2000.

    Google Scholar 

  11. Martin Giese. Proof search without backtracking using instance streams, position paper. In Peter Baumgartner and Hantao Zhang, editors, 3rd Int. Workshop on First-Order Theorem Proving (FTP), St. Andrews, Scotland, TR 5/2000 Univ. of Koblenz, pages 227–228, 2000.

    Google Scholar 

  12. Boris Konev and Tudor Jebelean. Using meta-variables for natural deductionin theorema. In M. Kohlhase and M. Kerber, editors, Proceedings of Calculemus-2000 Conference. Electronic Notes in Computer Science, 2000.

    Google Scholar 

  13. Reinhold Letz and Gernot Stenz. Model elimination and connection tableau procedures. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science, 2001. to appear.

    Google Scholar 

  14. Robert Nieuwenhuis and Albert Rubio. Paramodulation-based theorem proving. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science, 2001. to appear.

    Google Scholar 

  15. M. S. Paterson and M. N. Wegman. Linear unification. Journal of Computer and System Sciences, 16(2):158–167, April 1978.

    Article  MathSciNet  MATH  Google Scholar 

  16. Raymond M. Smullyan. First-Order Logic, volume 43 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, New York, 1968.

    Book  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, Germany

    Martin Giese

Authors
  1. Martin Giese
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Automated Reasoning Project and Department of Computer Science, Australian National University, Canberra, ACT, 0200, Australia

    Rajeev Goré

  2. AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Favoritenstr. 9, E185-2, 1040, Wien, Austria

    Alexander Leitsch

  3. Institut für Informatik, Technische Universität München, 80290, München, Germany

    Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Giese, M. (2001). Incremental Closure of Free Variable Tableaux. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_46

Download citation

  • DOI: https://doi.org/10.1007/3-540-45744-5_46

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42254-9

  • Online ISBN: 978-3-540-45744-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation