ECAI-2000 Conference Paper

[full paper]

Extensions of Constraint Solving for Proof Planning

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

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 have to be combined. This paper discusses the extensions, their conceptional realization, and the implementation in the constraint solver CoSIE.

Keywords: Theorem Proving, Constraint-Based Reasoning

Citation: Erica Melis, Jürgen Zimmer, Tobias Müller: Extensions of Constraint Solving for Proof Planning. In W.Horn (ed.): ECAI2000, Proceedings of the 14th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2000, pp.229-233.