Analogy in CLAM

  • CL A M is a proof planner, developed by the Dream group in Edinburgh,that mainly operates for inductive proofs. This paper addresses the questionhow an analogy model that I developed independently of CL A M can beapplied to CL A M and it presents analogy-driven proof plan construction as acontrol strategy of CL A M . This strategy is realized as a derivational analogythat includes the reformulation of proof plans. The analogical replay checkswhether the reformulated justifications of the source plan methods hold inthe target as a permission to transfer the method to the target plan. SinceCL A M has very efficient heuristic search strategies, the main purpose ofthe analogy is to suggest lemmas, to replay not commonly loaded methods,to suggest induction variables and induction terms, and to override controlrather than to construct a target proof plan that can be built by CL A Mitself more efficiently.

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Verfasserangaben:Erica Melis
URN (Permalink):urn:nbn:de:hbz:386-kluedo-2640
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:1999
Jahr der Veröffentlichung:1999
Veröffentlichende Institution:Technische Universität Kaiserslautern
Datum der Publikation (Server):03.04.2000
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581 $