Constraint Solving for Proof Planning |
| |
Authors: | Email author" target="_blank">Jürgen?ZimmerEmail author Erica?Melis |
| |
Affiliation: | (1) Arbeitsgruppe Siekmann (AGS), Fachbereich Informatik (FB 14), Universität des Saarlandes, D-66041 Saarbrücken, Germany;(2) Competence Centre for eLearning, German Research Center for Artificial Intelligence (DFKI), D-66123 Saarbrücken, Germany |
| |
Abstract: | Proof planning is an application of AI planning to theorem proving that employs plan operators that encapsulate mathematical proof techniques. Many proofs require the instantiation of variables; that is, mathematical objects with certain properties have to be constructed. This is particularly difficult for automated theorem provers if the instantiations have to satisfy requirements specific for a mathematical theory, for example, for finite sets or for real numbers, because in this case unification is insufficient for finding a proper instantiation. Often, constraint solving can be employed for this task. We describe a framework for the integration of constraint solving into proof planning that combines proof planners and stand-alone constraint solvers. Proof planning has some peculiar requirements that are not met by any off-the-shelf constraint-solving system. Therefore, we extended an existing propagation-based constraint solver in a generic way. This approach generalizes previous work on tackling the problem. It provides a more principled way and employs existing AI technology. |
| |
Keywords: | automated reasoning proof plans constraint satisfaction |
本文献已被 SpringerLink 等数据库收录! |
|