×

Termination of theorem proving by reuse. (English) Zbl 1412.68241

McRobbie, M. A. (ed.) et al., Automated deduction – CADE-13. 13th international conference on automated deduction, New Brunswick, NJ, USA, July/August 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1104, 106-120 (1996).
Summary: 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.
For the entire collection see [Zbl 1102.68317].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

SPIKE; PLAGIATOR
PDFBibTeX XMLCite
Full Text: DOI

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.
[2] R. S. Boyer and J. S. Moore. A Computational Logic. ACM Monograph Series. Academic Press, 1979. · Zbl 0448.68020
[3] J. Brauburger. Plagiator — Design and Implementation of a Learning Theorem Prover. Diploma Thesis, TH Darmstadt, 1994. (in German).
[4] N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 3(1,2):69-115, 1987. · Zbl 0637.68035
[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.).
[6] N. Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. Communications of the ACM, 22(8):465-476, 1979. · Zbl 0431.68016 · doi:10.1145/359138.359142
[7] T. Ellman. Explanation-Based Learning: A Survey of Programs and Perspectives. ACM Computing Surveys, 21(2):163-221, 1989. · doi:10.1145/66443.66445
[8] F. Giunchiglia and T. Walsh. A Theory of Abstraction. Artificial Intelligence, 57:323-389, 1992. · Zbl 0762.68054 · doi:10.1016/0004-3702(92)90021-O
[9] R. P. Hall. Computational Approaches to Analogical Reasoning: A Comparative Analysis. Artificial Intelligence, 39:39-120, 1989. · Zbl 0668.68097
[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. · Zbl 0847.68103
[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.
[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.
[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.
[14] T. Kolbe and C. Walther. Patching Proofs for Reuse. Technical Report IBN 95/27, Technische Hochschule Darmstadt, 1995.
[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.
[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.
[17] T. Kolbe and C. Walther. On the Benefits of Reusing Past Problem Solutions. Technical Report IBN 96/35, Technische Hochschule Darmstadt, 1996. · Zbl 1412.68241
[18] N. J. Nilsson. Problem Solving Methods in Artificial Intelligence. McGraw Hill, New York, 1971.
[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.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.