Publication details
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
@INPROCEEDINGS{MelisMuellerZimmer:0,
title = {Integrating Constraint Solving into Proof Planning},
author = {Erica Melis and Jürgen Zimmer and Tobias Müller},
year = {2000},
month = {mar},
editor = {{H\'elène Kirchner and Christophe Ringeissen}},
publisher = {springer},
booktitle = {Frontiers of Combining Systems -- Third International Workshop, FroCos 2000},
series = {lnai},
volume = {1794},
pages = {{32--46}},
address = {"Nancy, France"},
}
Login to edit
Legal notice, Privacy policy
