Abstract
Internal analogy tries to reuse solutions of subproblems within the same problem solving process. In mathematical theorem proving several patterns are known where internal analogy suggests itself. Hence, we propose the use of internal analogy in automated theorem proving. This paper investigates the possibility of incorporating internal analogy into the inductive proof planner CL A M. It introduces internal analogy as a control strategy of CL A M that can reduce search. We concentrate on using internal analogy to avoid the repeated application of the induction revision critic. The implementation has been tested and it was found that internal analogy can reduce the time taken to construct proof plans for some theorems.
The first author was supported by the HC&M grant CHBICT930806 and the second author by an EPSRC studentship. Computing facilities were in part provided by EPSRC grant GR/J/80702.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303–324, 1991.
A. Bundy, Stevens A, F. Van Harmelen, A. Ireland, and A. Smaill. A heuristic for guiding inductive proofs. Artificial Intelligence, 63:185–253, 1993.
J.G. Carbonell. Derivational analogy: A theory of reconstructive problem solving and expertise acquisition. In R.S. Michalsky, J.G. Carbonell, and T.M. Mitchell, editors, Machine Learning: An Artificial Intelligence Approach, pages 371–392. Morgan Kaufmann Publ, Los Altos, 1986.
M. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. Lecture Notes in Computer Science 78. Springer, Berlin, 1979.
Angela K. Hickman and Jill H. Larkin. Internal analogy: A model of transfer within problems. In The 12th Annual Conference of The Cognitive Science Society, pages 53–60, Hillsdale, NJ, 1990. Lawrence Erlbaum Associates.
Angela K. Kennedy. Internal Analogy: A First Step Towards a Unified Theory of Analogical Problem Solving. Unpublished PhD thesis, Carnegie Mellon University, to appear 1995.
D. Hutter. Guiding inductive proofs. In M.E. Stickel, editor, Proc. of 10th International Conference on Automated Deduction (CADE), volume Lecture Notes in Artificial Intelligence 449. Springer, 1990.
A. Ireland and A. Bundy. Productive use of failure in inductive proof. Technical report, Department of AI Edinburgh, 1994. Available from Edinburgh as DAI Research Paper 716.
Th. Kolbe and Ch. Walther. Second-order matching modulo evaluation — a technique for reusing proofs. In Proceedings of the 14th International Joint Conference on Artificial Intelligence, Montreal, 1995. Morgan Kaufmann.
S. Owen. Analogy for automated reasoning. Academic Press, London, 1990.
W. Reif and K. Stenzel. Reuse of Proofs in Software Verification. In Proc. 13th Conference on Foundations of Software Technology and Theoretical Computer Science, 1993. pages 74–85. LNCS 761, Springer.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Melis, E., Whittle, J. (1996). Internal analogy in theorem proving. 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_71
Download citation
DOI: https://doi.org/10.1007/3-540-61511-3_71
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