Adaptive Access to a Proof Planner

Erica Melis, Andreas Meier, Martin Pollet

In: A. Asperti , G. Bancerek , A. Trybulec (Hrsg.). Proceedings of Third International Conference on Mathematical Knowledge Management (MKM2004). International Conference on Mathematical Knowledge Management (MKM) Bialowieza Seiten 251-264 LNCS 3119 Springer 9/2004.


Mathematical tools such as computer algebra systems and interactive and automated theorem provers are complex systems and can perform difficult computations. Typically, such tools are used by a (small) group of particularly trained and skilled users to assist in mathematical problem solving. They can also be used as back-engines for interactive exercises in learning environments. This, however, suggests the adaptation of the choice of functionalities of the tool to the learner. This paper addresses the adaptive usage of the proof planner MULTI for the learning environment ActiveMath. The proof planner is a back-engine for interactive proof exercises. We identify different dimensions in which the usage of such a service system can be adapted and investigate the architecture realizing the adaptive access to MULTI.


Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence