The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #803

Title:Internal Analogy in Theorem Proving
Authors:Melis,E; Whittle,JN
Date:Apr 1996
Presented:Published in the Proceedings of CADE-13, 1996
Abstract:Internal analogy tries to reuse solutions of subproblems within the same problem solving process. In mathematical theorem proving several patterns are known where internal analogy suggests itself. Hence, we propose the use of internal analogy in automated theorem proving. This paper investigates the possibility of incorporating internal analogy into the inductive proof planner CLAM. It introduces internal analogy as a control strategy of CLAM that can reduce search. We concentrate on using internal analogy to avoid the repeated application of the induction revision critic. The implementation has been tested and it wasfound that internal analogy can reduce the time taken to construct proof plans for some theorems.

[Search These Pages] [DAI Home Page] [Comment]