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, and the kept-alive notebooks from the Fall 2017 course are now experimentally available here.

The old LaTeX-based version from 2011–2013 shuld now only be of historic interest, but is still available as CalcCheck-0.2.


Wolfram Kahl