The MIPPA project investigates usage foundations of proof planning techniques in mathematical tutoring systems. It targets the integration of the proof planner MULTI as back-engine for proof exercises in the learning environment ActiveMath.
Empirical studies suggest that students have deficiencies in mathematical competences with respect to understanding and development of proofs. This is due to shortcomings of student's self-guided explorative learning opportunities and the lack of (self-)explanations during problem solving. Such an active and explorative learning can be supported by tools.
Proof planning is a knowledge-based proof technique. It constructs proofs at abstract level of mathematical steps guided by mathematically motivated heuristics. Although its main application has been for automated proof construction, it is also a promising technique for math education.
In an educational context, however, the original features of automated proof planning are not sufficient. Hence, MIPPA investigates and extends existing proof planning techniques, such as meta-reasoning and guidance by heuristics, as well as their useful exploitation in a learning context. Moreover, new proof planning features which support effective learning, will be developed. For instance:
- interactive and mixed-initiative proof sessions,
- adaptivity to the learner,
- generation of feedback on the learners activities,
- possibility to make mistakes,
- suitable presentation of proof states and proof information.
The development of a GUI supporting active and explorative learning is in the scope of the MIPPA project.
MULTI has been developed in the OMEGA project at the Saarland University. ActiveMath has been developed at the DFKI and the Saarland University.