Publication details

Saarland University Computer Science

Integrating Constraint Solving into Proof Planning

Erica Melis, Jürgen Zimmer, Tobias Müller

Frontiers of Combining Systems -- Third International Workshop, FroCos 2000, Vol. 1794 of lnai, pp. 32--46, springer, March 2000

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.

Download PDF        Show BibTeX               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009