zbMATH — the first resource for mathematics

CalcCheck: a proof checker for teaching the “Logical approach to discrete math”. (English) Zbl 1462.68215
Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 324-341 (2018).
Summary: For calculational proofs as they are propagated by D. Gries and F. B. Schneider’s textbook classic [A logical approach to discrete math. New York, NY: Springer-Verlag (1993; Zbl 0861.03001)] (LADM), automated proof checking is feasible, and can provide useful feedback to students acquiring and practicing basic proof skills. We report on the CalcCheck system which implements a proof checker for a mathematical language that resembles the rigorous but informal mathematical style of LADM so closely that students very quickly recognise the system, which provides them immediate feed-back, as not an obstacle, but as an aid, and realise that the problem is finding proofs.
Students interact with this proof checker trough the “web application” front-end CalcCheck which provides some assistance for proof entry, but intentionally no assistance for proof finding. Upon request, the system displays, side-by-side with the student input, a version of that input annotated with the results of checking each step for correctness.
CalcCheck has now been used twice for teaching an LADM-based second-year discrete mathematics course, and students have been solving exercises and submitting assignments, midterms, and final exams on the system – for examinations, there is the option to disable proof checking and leave only syntax checking enabled. CalcCheck also performed the grading, with very limited human overriding necessary.
For the entire collection see [Zbl 1391.68001].

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
97U70 Technological tools, calculators (aspects of mathematics education)
CalcCheck; Fuzz; MathEdit
Full Text: DOI