External analogy in inductive theorem proving

Erica Metis, Jon Whittle

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

Abstract

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
PublisherSpringer
Pages112-122
Number of pages11
ISBN (Print)9783540634935
Publication statusPublished - 1 Jan 1997
Externally publishedYes
EventGerman Conference on Artificial Intelligence 1997 - Freiburg, Germany
Duration: 9 Sep 199712 Sep 1997
Conference number: 21st

Publication series

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

Conference

ConferenceGerman Conference on Artificial Intelligence 1997
Country/TerritoryGermany
CityFreiburg
Period9/09/9712/09/97

Cite this