The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math”

Students following a first-year course based on Gries and Schneider’s LADM textbook had frequently been asking: “How can I know whether my solution is good?”We now report on the development of a proof-checker designed to answer exactly that question, while intentionally not helping to find the solutions in the first place. CalcCheck provides detailed feedback to $${\rm L\kern-.36em\raise.3ex\hbox{\sc a}\kern-.15em …