Internal analogy in theorem proving

Erica Melis, Jon Whittle

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

4 Citations (Scopus)


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 was found that internal analogy can reduce the time taken to construct proof plans for some theorems.

Original languageEnglish
Title of host publicationAutomated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings
EditorsJohn K. Slaney, Michael A. McRobbie
Number of pages14
ISBN (Print)3540615113, 9783540615118
Publication statusPublished - 1 Jan 1996
Externally publishedYes
EventInternational Conference on Automated Deduction 1996 - New Brunswick, United States of America
Duration: 30 Jul 19963 Aug 1996
Conference number: 13th

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Automated Deduction 1996
Abbreviated titleCADE 1996
Country/TerritoryUnited States of America
CityNew Brunswick

Cite this