Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Session IV: Proving

Impasse-Driven Reasoning in Proof Planning

Andreas MeierContact Information and Erica MelisContact Information

(1)  German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany
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 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 MediaObjects/InlineFigure1.png.

Contact Information Andreas Meier
Email: ameier@dfki.de

Contact Information Erica Melis
Email: melis@dfki.de
Fulltext Preview (Small, Large)
Image of the first page of the fulltext


Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.114 • Server: mpweb19
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)