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 language | English |
|---|---|
| Title of host publication | KI-1997 |
| Subtitle of host publication | Advances in Artificial Intelligence - 21st Annual German Conference on Artificial Intelligence, 1997, Proceedings |
| Editors | Bernhard Nebel, Gerhard Brewka, Christopher Habel |
| Publisher | Springer |
| Pages | 112-122 |
| Number of pages | 11 |
| ISBN (Print) | 9783540634935 |
| Publication status | Published - 1 Jan 1997 |
| Externally published | Yes |
| Event | German Conference on Artificial Intelligence 1997 - Freiburg, Germany Duration: 9 Sept 1997 → 12 Sept 1997 Conference number: 21st |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 1303 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | German Conference on Artificial Intelligence 1997 |
|---|---|
| Country/Territory | Germany |
| City | Freiburg |
| Period | 9/09/97 → 12/09/97 |