CoSIE is special purpose constraint solver for arithmetical
constraints over the field of real numbers. It is integrated into the proof planning
system of OMEGA as an external reasoning
system. CoSIE combines propagation-based numeric constraint solving techniques with
term-rewriting and symbolic constraint inference mechanisms.
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.
This package can be installed by following the usual
configure, build, install procedure, i.e. by executing a the
shell:
./configure
make install
By default, all files of the package are
installed in the user's ~/.oz directory tree. In
particular, all modules are installed in the user's private cache.
functor
import
Application(exit)
System(showInfo: ShowInfo)
XApplication
at 'x-ozlib://mathweb/share/XApplication.ozf'
CosieClass('class': Cosie)
at 'x-ozlib://mathweb/cs/cosie/CosieClass.ozf'
define
local
Cos = {New Cosie init({New XApplication.manager init} 'Failure Test')}
S
in
{Cos reset('Failure Test' _)}
{Cos tellConstraint('L1' nil '<'('X'#var 'Y'#var) _)}
{Cos tellConstraint('L2' nil '<'('Y'#var 'Z'#var) _)}
{Cos tellConstraint('L3' nil '<'('Z'#var 'X'#var) _)}
{Cos reflect(S)}
{ShowInfo S}
%{Cos showConstraints(_)}
{Application.exit 0}
end
end