OMEGA is a mixed-initiative system with the ultimate goal of
supporting theorem proving in mathematical research practice and
mathematics education, i.e., it is a mathematical assistant system
that supports the user in the various tasks related to mathematical
theorem proving. The current system consists of a proof planner and a
distributed collection of tools for formulating problems, proving
subproblems, and for proof presentation. The distributed graphical
user interface, LOUI, provides advanced communication facilities; the
MBase tool is an active mathematical database; the constraint solver
LINEQ helps to construct mathematical objects; several traditional
automated theorem proving systems such as OTTER and SPASS and an
induction prover, INKA, may tackle simple subproblems; diverse
computer algebra systems can be used to simplify expressions and to
oracle the instantiations of variables.
The system is to be used in mathematical research and maths education.
The application of OMEGA in mainstream mathematics research rests upon
the specialized tools for finding a proof and checking it for its
correctness, whereas for mathematical tutor systems it seems to be
more important to explicitely represent knowlwedge about mathematical
problem solving strategies, methods, and control.
Our current research is concerned with the resource-dependent use of
problem solving strategies, the generation of proposals for the
mathematician on how to prove a theorem, the efficient organization
and use of the large amount of mathematical knowledge stored in the
mathematical database, MBase, and a cognitively adequate presentation
of proofs and proof attempts.
|