eds.activemath.org

The Main Idea

The Omega Mathematical Assistant System offers a module dubbed the "OmegaTutor". It is basically an automated proof construction/proof checking framework based on Omega's Assertion Application Mechanism, which allows to build a proof interactively and semi-automatically, such that intermediate steps in the proof construction can be supplied by the user, and the proof is automatically updated (and possible gaps are filled in automatically). This allows to check the correctness of the proof steps suggested by the user within a particular proof exercise, similar to the work of a human tutor who is checking a student's proof. Furthermore, a granularity analysis module can be employed which additionally judges whether the step size of the student's steps is appropriate (from a cognitive/didactic point of view).

The OmegaTutor currently has no convenient user interface, and its student model is not integrated into any larger learning environment. Moreover, the (didactically appropriate) presentation of learning material is not in the focus of Omega. The integration of the OmegaTutor with ActiveMath will enable the user to call the OmegaTutor from within ActiveMath to work on proof exercises. In particular, this will connect student modeling across the two platforms, such that the exercises performed with the help of the OmegaTutor are put in the broader learning context of the student.

Prototype

A first prototype version connects the Exercise Subsystem in ActiveMath with the OmegaTutor via XML-RPC. The exercise file omegatutor_console.omdoc (in omdoc1/exercises_test/omdoc) allows the user to enter in a dialog with the OmegaTutor about a concrete proof exercise. For the moment, this is always the same exercise (however, a choice will be included at a later stage). The user is supposed to work on the proof by indicating the next proof step, on which she receives immediate feedback from the OmegaTutor. Currently, the feedback is quite sparse (correct/incorrect), but can be extended at a later point to granularity judgments and hints. This way, the user engages in a dialog with the OmegaTutor. For each formula, its status has to be indicated, whether it represents a hypothesis, a conclusion, a goal reduction or a conjecture.

Technically, OmegaTutor acts as an XML-RPC server. Connections are initiated by instances of the OmegaTutorService class (org.activemath.exercises.openmath.services.OmegaTutorService). The exercise generator OmegaTutorGenerator (org.activemath.exercises.generators.OmegaTutorGenerator) passes each input from the student on the ActiveMath web interface via the OmegaTutorService to OmegaTutor and extends the dialog by a simple display of the answer together with a new input field. This is similar to the cas_console exercise, for example.

Further Development

At a later stage, the student models of ActiveMath and OmegaTutor will be synchronized via XML-RPC. This is important, since the granularity analysis in OmegaTutor heavily relies on data from the student model. This will allow some more targeted feedback than only correct/incorrect. Another mid-term goal is to embed the OmegaTutor exercises into the ActiveMath content, such that lessons are linked with appropriate OmegaTutor exercises.