Adaptive access to a proof planner

Abstract

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. © Springer-Verlag Berlin Heidelberg 2004.