×

Proving theorems by reuse. (English) Zbl 0939.68823

Summary: We investigate the improvement of theorem proving by reusing previously computed proofs. We have developed and implemented the Plagiator system which proves theorems by mathematical induction with the aid of a human advisor: If a base or step formula is submitted to the system, it tries to reuse a proof of a previously verified formula. If successful, labour is saved, because the number of required user interactions is decreased. Otherwise the human advisor is called for providing a hand crafted proof for such a formula, which subsequently – after some (automated) preparation steps – is stored in the system’s memory, to be in stock for future reasoning problems. Besides the potential savings of resources, the performance of the overall system is improved, because necessary lemmata might be speculated as the result of an attempt to reuse a proof. The success of the approach is based on our techniques for preparing given proofs as well as by our methods for retrieval and adaptation of reuse candidates which are promising for future proof reuses. We prove the soundness of our approach and illustrate its performance with several examples.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Aamodt, A.; Plaza, E., Case-based reasoning: foundational issues, methodological variations, and system approaches, AI communications, 7, 1, 39-59, (1994)
[2] Avenhaus, J.; Denzinger, J.; Fuchs, M., DISCOUNT: A system for distributed equational deduction, (), 397-402
[3] Bachmair, L.; Dershowitz, N.; Plaisted, D.A., Completion without failure, ()
[4] Bergmann, R.; Wilke, W., Learning abstract planning cases, (), 55-76
[5] Biundo, S.; Hummel, B.; Hutter, D.; Walther, C., The karlsruhe induction theorem proving system, (), 672-674
[6] Blumenthal, B.; Porter, B.W., Analysis and empirical studies of derivational analogy, Artificial intelligence, 67, 287-327, (1994)
[7] Börner, K.; Coulon, C.H.; Pippig, E.; Tammer, E.-C., Structural similarity and adaption, (), 58-75
[8] Bouhoula, A.; Kounalis, E.; Rusinowitch, M., {\scspike}: an automatic theorem prover, ()
[9] Boy de la Tour, T.; Caferra, R., Proof analogy in interactive theorem proving: A method to express and use it via second order pattern matching, (), 95-99
[10] Boy de la Tour, T.; Kreitz, C., Building proofs by analogy via the curry-howard isomorphism, (), 202-213 · Zbl 0925.68400
[11] Boyer, R.S.; Moore, J.S., A computational logic, ACM monograph series, (1979), Academic Press New York
[12] Boyer, R.S.; Moore, J.S., A computational logic handbook, Perspectives in computing, 23, (1988), Academic Press New York · Zbl 0678.68091
[13] Brauburger, J., {\scplagiator}—design and implementation of a learning theorem prover, diploma thesis (in German), (1994), TH Darmstadt
[14] Brock, B.; Cooper, S.; Pierce, W., Analogical reasoning and proof discovery, (), 454-468
[15] Bundy, A., The use of explicit plans to guide inductive proofs, (), 111-120
[16] Bundy, A.; Stevens, A.; van Harmelen, F.; Ireland, A.; Smaill, A., Rippling: A heuristic for guiding inductive proofs, Artificial intelligence, 62, 183-253, (1993) · Zbl 0789.68121
[17] Bundy, A.; van Harmelen, F.; Horn, C.; Smaill, A., The oyster-clam system, (), 647-648
[18] Carbonell, J.G., Derivational analogy: A theory of reconstructive problem solving and expertise acquisition, (), 371-392
[19] Curien, R., Second order E-matching as a tool for automated theorem proving, (), 242-257
[20] Defourneaux, G.; Bourely, C.; Peltier, N., Semantic generalizations for proving and disproving conjectures by analogy, J. automat. reason., 20, 27-45, (1998) · Zbl 0893.68134
[21] Defourneaux, G.; Peltier, N., Partial matching for analogy discovery in proofs and counter-examples, ()
[22] DeJong, G.; Mooney, R., Explanation-based learning: an alternative view, Machine learning, 1, 145-176, (1986)
[23] Denzinger, J.; Schulz, S., Learning domain knowledge to improve theorem proving, (), 62-76 · Zbl 1412.68217
[24] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (), 243-320 · Zbl 0900.68283
[25] Desimone, R.V., Learning control knowledge within an explanation-based learning framework, ph.D. thesis, (1989), Department of Artificial Intelligence, University of Edinburgh
[26] Dietzen, S.; Pfenning, F., Higher-order and modal logic as a framework for explanation-based generalization, Machine learning, 9, 23-55, (1992)
[27] Donat, M.R.; Wallen, L.A., Learning and applying generalised solutions using higher order resolution, (), 41-60 · Zbl 0644.68110
[28] Ellman, T., Explanation-based learning: A survey of programs and perspectives, ACM computing surveys, 21, 2, 163-221, (1989)
[29] Enderton, H.B., A mathematical introduction to logic, (1972), Academic Press San Diego, CA · Zbl 0298.02002
[30] Etzioni, O., A structural theory of explanation-based learning, Artificial intelligence, 60, 93-139, (1993)
[31] Felty, A.; Howe, D., Generalization and reuse of tactic proofs, (), 1-15
[32] Francis, A.G.; Ram, A., A domain-independent algorithm for multi-plan adaptation and merging in least-commitment planners, (), 19-25
[33] Fuchs, M., Learning proof heuristics by adapting parameters, ()
[34] Fuchs, M., Experiments in the heuristic use of past proof experience, (), 523-537 · Zbl 1412.68224
[35] Giesl, J., Termination analysis for functional programs using term orderings, (), 154-171
[36] Giunchiglia, F.; Walsh, T., A theory of abstraction, Artificial intelligence, 57, 323-389, (1992) · Zbl 0762.68054
[37] Goldfarb, W.D., The undecidability of the second-order unification problem, Theoret. comput. sci., 13, 225-230, (1981) · Zbl 0457.03006
[38] Greiner, R., Learning by understanding analogies, Artificial intelligence, 35, 81-125, (1988) · Zbl 0646.68095
[39] Hall, R.P., Computational approaches to analogical reasoning: A comparative analysis, Artificial intelligence, 39, 39-120, (1989) · Zbl 0668.68097
[40] Huet, G., A unification algorithm for typed λ-calculus, Theoret. comput. sci., 1, 27-57, (1975) · Zbl 0337.68027
[41] Huet, G.; Lang, B., Proving and applying program transformations expressed with second-order patterns, Acta informatica, 11, 11-31, (1978) · Zbl 0389.68008
[42] Hutter, D., Colouring terms to control equational reasoning, J. automat. reason., 18, 399-442, (1997) · Zbl 0881.68108
[43] Hutter, D.; Sengler, C., INKA: the next generation, (), 288-292 · Zbl 1412.68236
[44] Ireland, A.; Bundy, A., Productive use of failure in inductive proof, J. automat. reason. (special issue on automation of proofs by mathematical induction), 16, 1-2, (1996) · Zbl 0847.68103
[45] Kapur, D.; Subramaniam, M., Lemma discovery in automating induction, (), 538-552 · Zbl 1412.68239
[46] Kapur, D.; Zhang, H., RRL: A rewrite rule laboratory, (), 768-769
[47] Kedar-Cabelli, S.T.; McCarty, L.T., Explanation-based generalization as resolution theorem proving, (), 93-106
[48] Kling, R.E., A paradigm for reasoning by analogy, Artificial intelligence, 2, 147-178, (1971) · Zbl 0227.68041
[49] Knoblock, C.A., Automatically generating abstractions for planning, Artificial intelligence, 68, 243-302, (1994) · Zbl 0942.68712
[50] Kolbe, T., Optimizing proof search by machine learning techniques, doctoral dissertation, technische hochschule Darmstadt, (1997), Shaker Aachen
[51] Kolbe, T.; Brauburger, J., {\scplagiator}—A learning prover, (), 256-259
[52] Kolbe, T.; Glesner, S., Many-sorted logic in a learning theorem prover, (), 75-86
[53] Kolbe, T.; Walther, C., Patching proofs for reuse, (), 303-306
[54] Kolbe, T.; Walther, C., Proof management and retrieval, (), 16-20
[55] Kolbe, T.; Walther, C., Second-order matching modulo evaluation—A technique for reusing proofs, (), 190-195
[56] Kolbe, T.; Walther, C., Termination of theorem proving by reuse, (), 106-120 · Zbl 0939.68823
[57] Kolbe, T.; Walther, C., Proof analysis, generalization and reuse, (), 189-219 · Zbl 0970.68154
[58] Kolbe, T.; Walther, C., On terminating lemma speculations, J. inform. comput., (1999), to appear · Zbl 1045.68606
[59] Kolodner, J.L., Case-based reasoning, (1993), Morgan Kaufmann San Mateo, CA
[60] Lopez de Mantaras, R.; Plaza, E., Case-based reasoning, (1995), MLnet News
[61] Melis, E., A model of analogy-driven proof-plan construction, (), 182-188
[62] Melis, E.; Whittle, J., Analogy in inductive theorem proving, J. automat. reason., 22, 117-147, (1999) · Zbl 0929.03019
[63] Michalski, R.S.; Kodratoff, Y., Research in machine learning: recent progress, classification of methods and future directions, (), 3-30
[64] Minton, S., Quantitative results concerning the utility of explanation-based learning, Artificial intelligence, 42, 363-391, (1990)
[65] Mitchell, T.M.; Keller, R.M.; Kedar-Cabelli, S.T., Explanation-based generalization: A unifying view, Machine learning, 1, 47-80, (1986)
[66] Nakhaeizadeh, G.; Fuhr, N.; Morik, K.; Bartsch-Spörl, B.; Wess, S., Zur diskussion, Künstliche intelligenz, 1, 36-41, (1996), Themenheft Fallbasiertes Schließen
[67] Nie, X.; Plaisted, D.A., Application of explanation-based generalization in resolution theorem proving, (), 226-233
[68] Owen, S., Analogy for automated reasoning, (1990), Academic Press New York · Zbl 0823.68097
[69] Plaisted, D.A., Theorem proving with abstraction, Artificial intelligence, 16, 47-108, (1981) · Zbl 0454.68113
[70] Protzen, M., Lazy generation of induction hypotheses, ()
[71] Reif, W.; Stenzel, K., Reuse of proofs in software verification, () · Zbl 1058.68525
[72] Schrödl, S., Explanation-based generalization for negation as failure and multiple examples, (), 448-452
[73] Segre, A.; Elkan, C., A high-performance explanation-based learning algorithm, Artificial intelligence, 69, 1-50, (1994)
[74] Smyth, B.; Cunningham, P., Deja vu: A hierarchical case-based reasoning system for software design, ()
[75] van Harmelen, F.; Bundy, A., Explanation-based generalisation = partial evaluation, Artificial intelligence, 36, 401-412, (1988) · Zbl 0655.68106
[76] Veloso, M.M., {\scprodigy/analogy}: analogical reasoning in general problem solving, (), 33-50
[77] Veloso, M.M.; Carbonell, J.G., Derivational analogy in PRODIGY: automating case acquisition, storage, and utilization, Machine learning, 10, 249-278, (1993)
[78] Villafiorita, A.; Giunchiglia, F., Inductive theorem proving via abstraction, ()
[79] Walther, C., A many-sorted calculus based on resolution and paramodulation, research notes on artificial intelligence, (1987), Pitman, London/Morgan Kaufmann Los Altos, CA
[80] Walther, C., Computing induction axioms, () · Zbl 0925.03053
[81] Walther, C., Combining induction axioms by machine, ()
[82] Walther, C., Mathematical induction, (), 127-227
[83] Walther, C., On proving the termination of algorithms by machine, Artificial intelligence, 71, 1, 101-157, (1994) · Zbl 0938.68819
[84] Walther, C.; Kolbe, T., Report on proving theorems by reuse, technical report, (1998), Technische Universität Darmstadt · Zbl 0939.68823
[85] Watson, I.D., An introduction to case-based reasoning, (), 3-16
[86] Whittle, J., Analogy in CLAM, Master’s thesis, (1995), Department of Artificial Intelligence, University of Edinburgh
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.