Extensions of constraint solving for proof planning
Erica Melis⋆, Jürgen Zimmer, Tobias Müller · 2000
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 are usually geared towards their typical applications. Since proof planning differs from other applications, we present extensions of constraint solving necessary for its use in proof planning. We think that these extensions can broaden the range applications of constraint solving even beyond proof planning. 1 Introduction In automated theorem proving and proof planning, difficulties can be caused by the need to construct mathematical objects with theory-specific properties. More often than not, unification offers little support for this task and logic proofs, say of linear inequalities, can be very long and infeasible for purely logical automated theorem proving. This situation...