## Theorem Proving by Analogy - A Compelling Example ?

- This paper shows how a new approach to theorem provingby analogy is applicable to real maths problems. This approach worksat the level of proof-plans and employs reformulation that goes beyondsymbol mapping. The Heine-Borel theorem is a widely known result inmathematics. It is usually stated in R 1 and similar versions are also truein R 2 , in topology, and metric spaces. Its analogical transfer was proposedas a challenge example and could not be solved by previous approachesto theorem proving by analogy. We use a proof-plan of the Heine-Boreltheorem in R 1 as a guide in automatically producing a proof-plan of theHeine-Borel theorem in R 2 by analogy-driven proof-plan construction.

Author: | Erica Melis |
---|---|

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

Document Type: | Preprint |

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 |

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 |