\input zb-basic
\input zb-matheduc
\iteman{ZMATH 2009e.00709}
\itemau{Schiller, Marvin; Dietrich, Dominik; Benzm\"{u}ller, Christoph}
\itemti{Proof step analysis for proof tutoring -- a learning approach to granularity.}
\itemso{Teach. Math. Comput. Sci. 6, No. 2, 325-343 (2008).}
\itemab
Summary: We present a proof step diagnosis module based on the mathematical assistant system OMEGA. The task of this module is to evaluate proof steps as typically uttered by students in tutoring sessions on mathematical proofs. In particular, we categorise the step size of proof steps performed by the student, in order to recognise if they are appropriate with respect to the student model. We propose an approach which builds on reconstructions of the proof in question via automated proof search using a cognitively motivated proof calculus. Our approach employs learning techniques and incorporates a student model, and our diagnosis module can be adjusted to different domains and users. We present a first evaluation based on empirical data.
\itemrv{~}
\itemcc{R45 E35 E55 U55 R25}
\itemut{proof tutoring; automated reasoning; machine learning}
\itemli{}
\end