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

*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*Wolfram Kahl:***Calculational Relation-Algebraic Proofs in the Teaching Tool CalcCheck**, Journal of Logical and Algebraic Methods in Programming, volume 117, Dec. 2020, 100581 (39 pages)

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.