“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. The kept-alive notebooks from a Fall 2020 course and from a Fall 2023 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:***Providing On-Demand Feedback for Improved Learning of Logical Reasoning in Computer Science and Software Engineering**, in M. E. Auer, D. Centea (eds.):*Visions and Concepts for Education 4.0, ICBL 2020*, Advances in Intelligent Systems and Computing, vol 1314. Springer, Cham. 2021*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)*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:***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

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.