CALCCHECK

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 2018 course are now experimentally available here.

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

Publications


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