“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`
”.

*Wolfram Kahl:***CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math”**, in J. Avigad, A. Mahboubi (eds.):*Interactive Theorem Proving, 9th International Conference, IITP 2018*, Springer-Verlag, 2018*Wolfram Kahl:***Calculational Relation-Algebraic Proofs in the Teaching Tool CalcCheck**, in J. Desharnais, W. Guttmann, S. Joosten (eds.):*Relational and Algebraic Methods in Computer Science, 17th International Conference, RAMiCS 2018*, Springer-Verlag, 2018

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:***The Teaching Tool CalcCheck: A Proof-Checker for Gries and Schneider's “Logical Approach to Discrete Math”**, in J.-P. Jouannaud, Z. Shao (eds.):*Certified Programs and Proofs, CPP 2011*, pp. 216–230, LNCS 7086, Springer-Verlag, 2011.