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

CalcCheck is a proof checker for calculational proofs in the logics of the popular textbook A Logical Approach to Discrete Math (LADM) by David Gries and Fred Schneider.

The current version is still under development; its main use is as a web application implemented using Haste — initial documentation is here (see also some Syntax hints), and the kept-alive notebooks from the Fall 2020 course are now experimentally available here; there is also a “long theorem list” from the 2019 version of the course.

If you are interested in using CalcCheck for your course, please send an e-mail to kahl at cas dot mcmaster dot ca.


Predecessor System

The old LaTeX-based version from 2011–2013 should now only be of historic interest, but is still available as CalcCheck-0.2 and described in the following publication:

Wolfram Kahl