# 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 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.

## Publications

*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:*
**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.

*Wolfram Kahl*