CalcCheck: 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 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 …