External analogy in inductive theorem proving

Erica Metis, Jon Whittle

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


Tiffs paper investigates analogy-driven proof plan construction in inductive theorem proving. Given a proof plan of a source theorem, we identify constraints of second-order mappings that enable a replay of the source plan to produce a similar plan for the target theorem. In addition, the analogical replay is controlled by justifications that have to be satisfied in the target. Our analogy procedure, ABALONE, is implemented on top of the proof planner, CLAM. Employing analogy has extended the problem solving horizon of CLAM: with analogy, some theorems could be proved that CLAM could not prove automatically.

Original languageEnglish
Title of host publicationKI-1997
Subtitle of host publicationAdvances in Artificial Intelligence - 21st Annual German Conference on Artificial Intelligence, 1997, Proceedings
EditorsBernhard Nebel, Gerhard Brewka, Christopher Habel
Number of pages11
ISBN (Print)9783540634935
Publication statusPublished - 1 Jan 1997
Externally publishedYes
EventGerman Conference on Artificial Intelligence 1997 - Freiburg, Germany
Duration: 9 Sept 199712 Sept 1997
Conference number: 21st

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


ConferenceGerman Conference on Artificial Intelligence 1997

Cite this