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.
Cite
CITATION STYLE
Metis, E., & Whittle, J. (1997). External analogy in inductive theorem proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1303, pp. 112–122). Springer Verlag. https://doi.org/10.1007/3540634932_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
