## Some Aspects of Analogy in Mathematical Reasoning

- An important research problem is the incorporation of "declarative" knowledge into an automated theorem prover that can be utilized in the search for a proof. An interesting pro-posal in this direction is Alan Bundy's approach of using explicit proof plans that encapsulatethe general form of a proof and is instantiated into a particular proof for the case at hand. Wegive some examples that show how a "declarative" highlevel description of a proof can be usedto find proofs of apparently "similiar" theorems by analogy. This "analogical" information isused to select the appropriate axioms from the database so that the theorem can be proved.This information is also used to adjust some options of a resolution theorem prover. In orderto get a powerful tool it is necessary to develop an epistemologically appropriate language todescribe proofs, for which a large set of examples should be used as a testbed. We presentsome ideas in this direction.

Author: | Manfred Kerber |
---|---|

URN (permanent link): | urn:nbn:de:hbz:386-kluedo-3249 |

Serie (Series number): | SEKI Report (89,12) |

Document Type: | Article |

Language of publication: | English |

Year of Completion: | 1999 |

Year of Publication: | 1999 |

Publishing Institute: | Technische Universität Kaiserslautern |

Date of the Publication (Server): | 2000/04/03 |

Tag: | abstract description; analogy ; proof plans ; theorem proving |

Faculties / Organisational entities: | Fachbereich Informatik |

DDC-Cassification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |

Licence (German): | Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011 |