Extensions of Constraint Solving for Proof Planning

11 years 4 months ago
Extensions of Constraint Solving for Proof Planning
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 check, 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 CoSIE.
Erica Melis, Jürgen Zimmer, Tobias Mülle
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2000
Where ECAI
Authors Erica Melis, Jürgen Zimmer, Tobias Müller
Comments (0)