ABSTRACT. For calculational proofs as they are propagated by Gries and Schneider's textbook classic “A Logical Approach to Discrete Math” (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 as not an obstacle, but as an aid, and realise that the problem is finding proofs.

Students interact with this trough the “web application” front-end CalcCheckWeb 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 annotated with the results of checking each step for correctness.

CalcCheckWeb has now been used twice for teaching this 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.