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).