Sciweavers

MKM
2005
Springer

Impasse-Driven Reasoning in Proof Planning

13 years 9 months ago
Impasse-Driven Reasoning in Proof Planning
Abstract. In a problem solving process, a step may not result in the expected progress or may not be applicable as expected. Hence, knowledge how to overcome and react to impasses and other failures is an important ingredient of successful mathematical problem solving. To employ such knowledge in a proving system requires a variety of behaviors and a flexible control. Multi-strategy proof planning is a knowledge-based theorem proving approach that provides a variety of strategies and knowledgebased guidance for search at different levels. This paper introduces reasoning about impasses as a natural ingredient of meta-reasoning at a strategic level and illustrates the use of knowledge about failure handling in the proof planner Multi.
Andreas Meier, Erica Melis
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where MKM
Authors Andreas Meier, Erica Melis
Comments (0)