Masterarbeit,
Analogie im Beweisplanen
Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany, (2000)
Zusammenfassung
Analogical reasoning consists of transferring the solution of a previously solved
problem (called source) onto a new problem (called target). In this thesis 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 abstract planning
operators, called 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
comparisons 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.
