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.
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
”.
Publications
- 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
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