Carsten Ullrich
In this talk I describe TOPAL, an approach for the analogical transfer of mathematical proofs. The transfer is performed at the level of proof plans, therefore the application of methods, is replayed in the new problem rather than the application of single calculus steps. In order to cope with the complexity of proofs at plan level, I had to extent existing analogy frameworks in several ways: Firstly, as in proof planning a standard higher order matcher can no longer compare source and target terms, I propose extensions to higher order matching that make these comparisions possible again. Secondly, the underlying assumption of most analogy systems, namely that the differences in term structure expressed via the matching can be used to guide the transfer and adaption of the source plan, is not valid in proof planning. Therefore I show how planning mechanisms can be used to fulfil the same purpose of guiding transfer and adaptions. Thirdly, I propose how theorem proving by analogy can be realised as one of several problem solving strategies. I identify situations in which the use of analogy makes sense and present the corresponding strategic control knowledge. Finally, I have evaluated TOPAL. The evaluation shows that the use of planning mechanisms enhances the performance of the analogical transfer. By using these mechanisms a great number of complex problems can be solved.