Internal analogy in theorem proving

Erica Melis, Jon Whittle

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

5 Citations (Scopus)

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 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
PublisherSpringer
Pages92-105
Number of pages14
ISBN (Print)3540615113, 9783540615118
DOIs
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)
Volume1104
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Automated Deduction 1996
Abbreviated titleCADE 1996
CountryUnited States of America
CityNew Brunswick
Period30/07/963/08/96

Cite this