SFB 378 Home OMEGA staff OMEGA publications Deutsche Version OMEGA contact More about OMEGA OMEGA Flyer PS OMEGA Flyer PDF

B
READY
KnAc
PERFORM
OMEGA
NEP
CHORUS

OMEGA: A mathematical assistant

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.

SFB 378 Home OMEGA staff OMEGA publications Deutsche Version OMEGA contact More about OMEGA OMEGA Flyer PS OMEGA Flyer PDF