Abstract
The performance of problem solvers and theorem provers can be improved by means of mechanisms that enable the application of old solutions to new problems. One such (learning) mechanism consists of generalising an old solution to obtain a specification of the most general problem that it solves. The generalised solution can then be applied in the solution of new problems wherever instances of the general problem it solves can be identified.
We present a method based on higher order unification and resolution for the generalisation of solutions and the flexible application of such generalisations in the solution of new problems. Our use of higher order unification renders the generalisations useful in the solution of both sub- and superproblems of the original problem. The flexibility thus gained is controlled by means of filter expressions that restrict the unifiers considered.
In this way we show how the bulk of the problem solving, generalisation and application tasks of a (learning) problem solving system can be performed by the one algorithm. This work generalises ad hoc techniques developed in the field of Explanation Based Learning and presents the results in a formal setting.
This work was supported in part by SERC/Alvey grants GR/D/44874 and GR/D/44270 whilst both authors were with the Dept. of Artificial Intelligence, University of Edinburgh, Scotland.
Lincoln Wallen is supported by a grant from the British Petroleum Venture Research Unit.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
deGroote, P. How I spent my time in Cambridge with Isabelle, Technical Report RR 87-1, Université Catholique de Louvain, January 1987.
Donat, M.R. Construction and Application of Generalisations Using Higher Order Unification. Master's thesis, Department of Artificial Intelligence, University of Edinburgh, 1987.
Fikes, R.E., Hart, P.E., and Nilsson, N.J. Learning and executing generalized robot plans. Artificial Intelligence, 3:251–288, 1972.
Kedar-Cabelli, S. and McCarty, L.T. Explanation-based generalization as resolution theorem proving. In P. Langley, editor, Proceedings of the 4th International Machine Learning Workshop, pages 383–389, Morgan Kaufmann, 1987.
Miller, D.A. and Nadathur, G. “Higher-order logic programming,” Proceedings of the 3rd Int. Logic Programming Conference, London, June 1986, 448–462.
Mitchell, T.M., Utgoff, P. E., and Banerji, R. Learning by experimentation: acquiring and modifying problem-solving heuristics. In Machine Learning, pages 163–190, Tioga Press, 1983.
Mitchell, T.M., Keller, R.M., and Kedar-Cabelli, S.T. Explanation-based generalization: a unifying view. Machine Learning, 1(1):47–80, 1986.
Paulson, L. Natural deduction as higher order resolution. Journal of Logic Programming, 3:237–258, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Donat, M.R., Wallen, L.A. (1988). Learning and applying generalised solutions using higher order resolution. In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012822
Download citation
DOI: https://doi.org/10.1007/BFb0012822
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19343-2
Online ISBN: 978-3-540-39216-3
eBook Packages: Springer Book Archive