English

Towards an Intelligent Tutor for Mathematical Proofs

Artificial Intelligence 2012-02-23 v1 Logic in Computer Science Mathematical Software Symbolic Computation

Abstract

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.

Keywords

Cite

@article{arxiv.1202.4828,
  title  = {Towards an Intelligent Tutor for Mathematical Proofs},
  author = {Serge Autexier and Dominik Dietrich and Marvin Schiller},
  journal= {arXiv preprint arXiv:1202.4828},
  year   = {2012}
}

Comments

In Proceedings THedu'11, arXiv:1202.4535

R2 v1 2026-06-21T20:23:15.059Z