Skip to main content
SpringerLink
Log in

Optimizing proof search in model elimination

  • Session 5A
  • Conference paper
  • First Online:
Book cover Automated Deduction — Cade-13 (CADE 1996)

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

Included in the following conference series:

Abstract

Many implementations of model elimination perform proof search by iteratively increasing a bound on the total size of the proof. We propose an optimized version of this search mode using a simple divide-and-conquer refinement. Optimized and unoptimized modes are compared, together with depth-bounded and best-first search, over the entire TPTP problem library. The optimized size-bounded mode seems to be the overall winner, but for each strategy there are problems on which it performs best. Some attempt is made to analyze why. We emphasize that our optimization, and other implementation techniques like caching, are rather general: they are not dependent on the details of model elimination, or even that the search is concerned with theorem proving. As such, we believe that this study is a useful complement to research on extending the model elimination calculus.

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. O. L. Astrachan and M. E. Stickel. Caching and lemmaizing in model elimination theorem provers. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Computer Science, pages 224–238, 1992. Springer-Verlag.

    Google Scholar 

  2. P. Baumgartner and U. Furbach. Model elimination without contrapositives and its application to PTTP. Research report 12-93, Institute for Computer Science, University of Koblenz, 1993.

    Google Scholar 

  3. B. Beckert and J. Posegga. leanT A P: Lean, tableau-based deduction. Journal of Automated Reasoning, 15:339–358, 1995.

    Article  Google Scholar 

  4. M. J. C. Gordon and T. F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993.

    Google Scholar 

  5. R. E. Korf. Depth-first iterative-deepening: An optimal admissible tree search. Artificial Intelligence, 27:97–109, 1985.

    MathSciNet  Google Scholar 

  6. R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A high-performance theorem proven. Journal of Automated Reasoning, 8:183–212, 1992.

    MathSciNet  Google Scholar 

  7. R. Letz, K. Mayr, and C. Goller. Controlled integrations of the cut rule into connection tableau calculi. Technical Report AR-94-01, TU München, 1994.

    Google Scholar 

  8. V. Lifschitz. Mechanical Theorem Proving in the USSR: the Leningrad School. Monograph Series on Soviet Union. Delphic Associates, 1986. See also ‘What is the inverse method?’ in the Journal of Automated Reasoning, vol. 5, pp. 1–23, 1989.

    Google Scholar 

  9. D. W. Loveland. Mechanical theorem-proving by model elimination. Journal of the ACM, 15:236–251, 1968.

    Article  Google Scholar 

  10. D. Michie. “Memo” functions and machine learning. Nature, 218:19–22, 1968.

    Google Scholar 

  11. L. C. Paulson. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994. With contributions by Tobias Nipkow.

    Google Scholar 

  12. D. A. Plaisted. A sequent-style model elimination strategy and a positive refinement. Journal of Automated Reasoning, 6:389–402, 1990.

    Article  Google Scholar 

  13. P. Rudnicki. Obvious inferences. Journal of Automated Reasoning, 3:383–393, 1987.

    Article  Google Scholar 

  14. M. E. Stickel. A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4:353–380, 1988.

    Article  Google Scholar 

  15. C. B. Suttner and G. Sutcliffe. The TPTP problem library. Technical Report AR-95-03, TU München, 1995.

    Google Scholar 

  16. M. Tarver. An examination of the Prolog Technology Theorem-Prover. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 322–335, 1990. Springer-Verlag.

    Google Scholar 

  17. P. Weis and X. Leroy. Le langage Caml. InterEditions, 1993. See also the CAML Web page: http://pauillac.inria.fr/caml/.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Åbo Akademi University, Lemminkäisenkatu 14a, 20520, Turku, Finland

    John Harrison

Authors
  1. John Harrison
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

M. A. McRobbie J. K. Slaney

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Harrison, J. (1996). Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_97

Download citation

  • DOI: https://doi.org/10.1007/3-540-61511-3_97

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61511-8

  • Online ISBN: 978-3-540-68687-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation