C_(ALC)C_（HECK）: A Proof Checker for Teaching the 'Logical Approach to Discrete Math'

摘要

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 C_(ALC)C_（HECK） 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 C_(ALC)C_（HECK）_(web) 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. C_(ALC)C_（HECK）_(web) 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. C_(ALC)C_（HECK） also performed the grading, with very limited human overriding necessary.