Proving a Heine-Borel Theorem by Analogy
Erica Melis⋆ · 1999
This paper addresses analogy-driven automated theorem proving that employs a source proof-plan to guide the search for a proof-plan of the target problem. The approach presented uses reformulations that go beyond symbol mappings and that incorporate frequently used re-representations and abstractions. Several realistic math examples were successfully processed by our analogy-driven proof-plan construction. One challenge example, a HeineBorel theorem, is discussed here. For this example the reformulaitons are shown step by step and the modifying actions are demonstrated. 1 Introduction Analogy in theorem proving has received little attention despite its importance in mathematics and the claims made for its usefulness in theorem proving [ Polya, 1957; Bledsoe, 1986; Wos, 1988 ] . Reasons for this situation are manifold: Firstly, different from simple AI domains, minor changes in theorems or proof assumptions may cause major changes in proofs. Hence, the retrieval of a source problem i...