Mechanizing Proof Step Evaluation for Mathematics Tutoring - The Case of Granularity
Marvin R. G. Schiller · 2007
The motif of this thesis is the application of deduction techniques to tutorial dialogs in mathematics. The aim is to characterize different degrees of “granularity” of proof steps, which designates their argumentative size. This aspect of mathematical proof steps, also referred to as grain size, is still under-investigated in the theorem proving community. However, the ability to reflect on the granularity of proof steps is important for teaching mathematics. We propose an approach towards the automatization of the granularity assessment for a given proof fragment, and perform a first analysis on an empirically collected sample of mathematical dialogs from a Wizard-of-Oz study that is also part of this thesis. We show how such an analysis is performed with a first manifest hypothesis on how a granularity measure is obtained. This hypothesis relates the granularity level of a mathematical statement to the number of inference steps required for its justification, which is tested for justifications in two different natural deduction calculi. The outcome does not provide sufficient evidence for this first hypothesis. However, it clarifies its deficiencies.