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 knowledge-based 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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Meier, A., & Melis, E. (2006). Impasse-driven reasoning in proof planning. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3863 LNAI, pp. 143–158). https://doi.org/10.1007/11618027_10
Mendeley helps you to discover research relevant for your work.