   |
Integrating Constraint Solving into Proof Planning
Author: Erica Melis and Jürgen Zimmer and Tobias MüllerEditor: H'el`ene Kirchner and Christophe Ringeissen
In proof planning mathematical objects with
theory-specific properties have to be
constructed. More often than not, mere
unification offers little support for this task.
However, the integration of constraint solvers
into proof planning can sometimes help solving
this problem. We present such an integration and
discover certain requirements to be met in order
to integrate the constraint solver's efficient
activities in a way that is correct and sufficient
for proof planning. We explain how the
requirements can be met by an extension of the
constraint solving technology and describe their
implementation in the constraint solver CoSIE.
|