Learning and applying generalised solutions using higher order resolution

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.