Providing Hints, Next Steps and Feedback in a Tutoring System for Structural Induction

Josje Lodder
(Open University of the Netherlands)
Bastiaan Heeren
(Open University of the Netherlands)
Johan Jeuring
(Universiteit Utrecht, The Netherlands)

Structural induction is a proof technique that is widely used to prove statements about discrete structures. Students find it hard to construct inductive proofs, and when learning to construct such proofs, receiving feedback is important. In this paper we discuss the design of a tutoring system, LogInd, that helps students with constructing stepwise inductive proofs by providing hints, next steps and feedback. As far as we know, this is the first tutoring system for structural induction with this functionality. We explain how we use a strategy to construct proofs for a restricted class of problems. This strategy can also be used to complete partial student solutions, and hence to provide hints or next steps. We use constraints to provide feedback. A pilot evaluation with a small group of students shows that LogInd indeed can give hints and next steps in almost all cases.

In Pedro Quaresma, Walther Neuper and João Marcos: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software (ThEdu'19), Natal, Brazil, 25th August 2019, Electronic Proceedings in Theoretical Computer Science 313, pp. 17–34.
Published: 28th February 2020.

ArXived at: https://dx.doi.org/10.4204/EPTCS.313.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org