Extensions of Constraint Solving for Proof Planning
Autor: Erica Melis and Jürgen Zimmer and Tobias Müller
Herausgeber: Werner Horn
The integration of constraint solvers into proof planning has pushed
the problem solving horizon. Proof planning benefits from the
general functionalities of a constraint solver such as consistency
checks, constraint inference, as well as the search for
instantiations. However, off-the-shelf constraint solvers need to
be extended in order to be be integrated appropriately: In
particular, for correctness, the context of constraints and
Eigenvariable-conditions have to be taken into account. Moreover,
symbolic and numeric constraint inference are combined. This
paper discusses the extensions to constraint solving for proof
planning, namely the combination of symbolic and numeric inference,
first-class constraints, and context trees. We also describe the
implementation of these extensions in the constraint solver $\mathcalcoSIE$.
|