Meta Reasoning in Multiple-Strategy Proof Planning

Andreas Meier, Erica Melis

In: Susanne Biundo , Thom Frühwirth , Günther Palm (Hrsg.). Poster Proceedings of 27th Annual German Conference on Artificial Intelligence (KI 2004). German Conference on Artificial Intelligence (KI) September 20-24 Ulm Germany Seiten 84-98 Lecture Notes in Computer Science (LNCS) 3238 2004-03 ISBN 3-540-23166-8 Springer Berlin 9/2004.


Monitoring a solution process and applying the right action at the right moment are at the heart of intelligent problem solving by humans. This includes the analysis of failure events and the development of "recommendations" to overcome typical failures. We present how meta-reasoning on failures can be used in multiple-strategy proof planning. This reasoning can exploit failures to guide subsequent proof plan manipulations and refinements. In the automated proof construction with the proof planner MULTI such failure reasoning cannot only ease the derivation of a solution proof plan but is required for some problems to find a solution at all.


Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence