Skip to main content
SpringerLink
Log in

Termination of theorem proving by reuse

  • Session 2A
  • Conference paper
  • First Online:
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

We investigate the improvement of theorem provers by reusing previously computed proofs. We formulate our method for reusing proofs as an instance of the problem reduction paradigm and then develop a termination requirement for our reuse procedure. We prove the soundness of our proposal and show that reusability of proofs is not spoiled by the termination requirement imposed on the reuse procedure. We also give evidence for the general usefulness of our termination requirement for lemma speculation in induction theorem proving.

This work was supported under grants no. Wa652/4-1,2,3 by the Deutsche Forschungsgemeinschaft as part of the focus 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. A. Bouhoula, E. Kounalis, and M. Rusinowitch. Spike: An Automatic Theorem Prover. In Proceedings of the Conference on Logic Programming and Automated Reasoning (LPAR-92), St. Petersburg, Russia. Springer, 1992.

    Google Scholar 

  2. R. S. Boyer and J. S. Moore. A Computational Logic. ACM Monograph Series. Academic Press, 1979.

    Google Scholar 

  3. J. Brauburger. Plagiator — Design and Implementation of a Learning Theorem Prover. Diploma Thesis, TH Darmstadt, 1994. (in German).

    Google Scholar 

  4. N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 3(1,2):69–115, 1987.

    Google Scholar 

  5. N. Dershowitz and J.-P. Jouannaud. Rewrite Systems, volume B of the Handbook of Theoretical Computer Science: Formal Models and Semantics, chapter 6, pages 243–320. Elsevier Science Publishers B.V., 1990. Jan van Leeuwen (Ed.).

    Google Scholar 

  6. N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. Communications of the ACM, 22(8):465–476, 1979.

    Article  Google Scholar 

  7. T. Ellman. Explanation-Based Learning: A Survey of Programs and Perspectives. ACM Computing Surveys, 21(2):163–221, 1989.

    Article  Google Scholar 

  8. F. Giunchiglia and T. Walsh. A Theory of Abstraction. Artificial Intelligence, 57:323–389, 1992.

    Article  Google Scholar 

  9. R. P. Hall. Computational Approaches to Analogical Reasoning: A Comparative Analysis. Artificial Intelligence, 39:39–120, 1989.

    MathSciNet  Google Scholar 

  10. A. Ireland and A. Bundy. Productive Use of Failure in Inductive Proof. Special Issue of the Journal of Automated Reasoning on Automation of Proofs by Mathematical Induction, 1996.

    Google Scholar 

  11. D. Kapur and H. Zhang. RRL: A Rewrite Rule Laborarory. In E. Lusk and R. Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction (CADE-88), Argonne, pages 768–769. Springer LNCS 310, 1988.

    Google Scholar 

  12. T. Kolbe and C. Walther. Reusing Proofs. In A. Cohn, editor, Proceedings of the 11th European Conference on Artificial Intelligence (ECAI-94), Amsterdam, The Netherlands, pages 80–84. John Wiley & Sons, Ltd., 1994.

    Google Scholar 

  13. T. Kolbe and C. Walther. Patching Proofs for Reuse. In N. Lavrac and S. Wrobel, editors, Proceedings of the European Conference on Machine Learning (ECML-95), Heraklion, Greece, pages 303–306. Springer LNAI 912, 1995.

    Google Scholar 

  14. T. Kolbe and C. Walther. Patching Proofs for Reuse. Technical Report IBN 95/27, Technische Hochschule Darmstadt, 1995.

    Google Scholar 

  15. T. Kolbe and C. Walther. Proof Management and Retrieval. In Proceedings of the IJCAI'95 Workshop on Formal Approaches to the Reuse of Plans, Proofs, and Programs, pages 16–20, 1995.

    Google Scholar 

  16. T. Kolbe and C. Walther. Second-Order Matching modulo Evaluation — A Technique for Reusing Proofs. In Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI-95), Montreal, Canada, pages 190–195, 1995.

    Google Scholar 

  17. T. Kolbe and C. Walther. On the Benefits of Reusing Past Problem Solutions. Technical Report IBN 96/35, Technische Hochschule Darmstadt, 1996.

    Google Scholar 

  18. N. J. Nilsson. Problem Solving Methods in Artificial Intelligence. McGraw Hill, New York, 1971.

    Google Scholar 

  19. C. Walther. Mathematical Induction. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, pages 127–227. Oxford University Press, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Technische Hochschule Darmstadt, Alexanderstr. 10, D-64283, Darmstadt, Germany

    Thomas Kolbe & Christoph Walther

Authors
  1. Thomas Kolbe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Walther
    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

Kolbe, T., Walther, C. (1996). Termination of theorem proving by reuse. 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_72

Download citation

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

  • 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