CoSIE: A Constraint Solver for Inqualities and
Equations over real numbers
About the use constraint solvers in proof planning
Many proofs require the construction of mathematical objects with
theory-specific properties (constraints). This specialized reasoning does not
work too well with traditional ATP systems. Theory-specific systems,
e.g. constraint solvers, can perform such services more efficiently because
they represent objects such as rational and real numbers by specialized data
types that can be efficiently handled and because they rely on efficient
special-purpose algorithms.
During proof planning a constraint solver
collects the constraints and propagates them. It checks for inconsistency in
order to restrict the search space in proof planning and finally searches for
witness terms for the existentially quantified variables.
The constraint solver CoSIE
CoSIE is special purpose constraint solver for arithmetical constraints over
the field of real numbers. CoSIE combines propagation-based numeric constraint
solving techniques with term-rewriting and symbolic constraint inference
mechanisms ( click here for a detailed description of
this symbiosis ).
During proof planning CoSIE collects all valid
constraints (wrt. its constraint language) from proof assumptions and planning
goals and tests for inconsistency of the constraint store. This helps the proof
planner to prune inconsistent paths in the search tree.
At the end of the
planning process (e.g. when no more constraints are told to the constraint
solver), CoSIE can search for solutions (i.e. instantiations) for the (meta-)
variables occuring in the planning problem. As a case study, we used CoSIE for
planning proofs of Limit Theorems .
Integration
CoSIE is integrated into the
Mathweb Software Bus as a mathematical service. Unfortunately, there's no
autonomous version available at the moment.
There is a description of the
main interface and the
constraint language of CoSIE available.
Implementation
follow the link to get more information about the implementation of CoSIE.
System requirements
Note, that CoSIE uses the Real Interval module of the Mozart Oz contribution.
So far, we only managed to run this module on SuSE 6.0 or RedHat 6.0 (or higher)
machines.
Bibliography
The most detailed description of CoSIE can be found in my diploma thesis:
If you want read more about the extensions of constraint solving necessary for proof
planning:
More about proof planning for limit theorems can be found here: