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.
|URN (permanent link):||urn:nbn:de:hbz:386-kluedo-2617|
|Language of publication:||English|
|Year of Completion:||1999|
|Year of Publication:||1999|
|Publishing Institute:||Technische Universität Kaiserslautern|
|Faculties / Organisational entities:||Fachbereich Informatik|
|DDC-Cassification:||004 Datenverarbeitung; Informatik|