Towards an Intelligent Tutor for Mathematical Proofs

Serge Autexier
(German Research Center for Artificial Intelligence (DFKI), Bremen, Germany)
Dominik Dietrich
(German Research Center for Artificial Intelligence (DFKI), Bremen, Germany)
Marvin Schiller
(Brunel University, London, UK)

Computer-supported learning is an increasingly important form of study since it allows for independent learning and individualized instruction. In this paper, we discuss a novel approach to developing an intelligent tutoring system for teaching textbook-style mathematical proofs. We characterize the particularities of the domain and discuss common ITS design models. Our approach is motivated by phenomena found in a corpus of tutorial dialogs that were collected in a Wizard-of-Oz experiment. We show how an intelligent tutor for textbook-style mathematical proofs can be built on top of an adapted assertion-level proof assistant by reusing representations and proof search strategies originally developed for automated and interactive theorem proving. The resulting prototype was successfully evaluated on a corpus of tutorial dialogs and yields good results.

In Pedro Quaresma and Ralph-Johan Back: Proceedings First Workshop on CTP Components for Educational Software (THedu'11), Wrocław, Poland, 31th July 2011, Electronic Proceedings in Theoretical Computer Science 79, pp. 1–28.
Published: 21st February 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: