Abstract
For calculational proofs as they are propagated by Gries and Schneider’s textbook classic “A Logical Approach to Discrete Math” (LADM), automated proof checking is feasible, and can provide useful feedback to students acquiring and practicing basic proof skills. We report on the 
system which implements a proof checker for a mathematical language that resembles the rigorous but informal mathematical style of LADM so closely that students very quickly recognise the system, which provides them immediate feed-back, as not an obstacle, but as an aid, and realise that the problem is finding proofs.
Students interact with this proof checker trough the “web application” front-end 
which provides some assistance for proof entry, but intentionally no assistance for proof finding. Upon request, the system displays, side-by-side with the student input, a version of that input annotated with the results of checking each step for correctness.
has now been used twice for teaching an LADM-based second-year discrete mathematics course, and students have been solving exercises and submitting assignments, midterms, and final exams on the system — for examinations, there is the option to disable proof checking and leave only syntax checking enabled. 
also performed the grading, with very limited human overriding necessary.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Gries (1997) restricts metavariables to be named by single upper-case letters, (non-meta-)variables by single lower-case letters. Gries (1997) then distinguishes between “uniform substitution” written
for metavariables V, and “textual substitution” written \(E^v_G\) for variables v, where only the latter renames variable binders to avoid capture of free variables of G. However, the use of “
” in the statement and proof of (8.22) there is then unclear — it will have to be understood as “textual substitution” since otherwise y might be captured by binders in R.
for metavariables V, and “textual substitution” written 
” in the statement and proof of (8.22) there is then unclear — it will have to be understood as “textual substitution” since otherwise y might be captured by binders in R.References
Back, R.-J.: Structured derivations: A unified proof style for teaching mathematics. Formal Aspects Comput. 22(5), 629–661 (2010). https://doi.org/10.1007/s00165-009-0136-5
Back, R.-J., Bos, V., Eriksson, J.: MathEdit: Tool support for structured calculational proofs. TUCS Technical report 854, Turku Centre for Computer Science (2007)
Carter, N.C., Monks, K.G.: A web-based toolkit for mathematical word processing applications with semantics. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 272–291. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_19
Ekblad, A.: High-performance client-side web applications through Haskell EDSLs. In: Mainland, G., (ed) Proceedings 9th International Symposium on Haskell, Haskell 2016, pp. 62–73. ACM (2016). https://doi.org/10.1145/2976002.2976015
Gries, D.: Foundations for calculational logic. In: Broy, M., Schieder, B. (eds.) Mathematical Methods in Program Development, pp. 83–126. Springer, Heidelberg (1997). https://doi.org/10.1007/978-3-642-60858-2_16
Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Monographs in Computer Science. Springer, New York (1993). https://doi.org/10.1007/978-1-4757-3837-7
Gries, D., Schneider, F.B.: Equational propositional logic. Inform. Process. Lett. 53, 145–152 (1995). https://doi.org/10.1016/0020-0190(94)00198-8
Kahl, W.: The teaching tool CalcCheck a proof-checker for Gries and Schneider’s “Logical Approach to Discrete Math”. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 216–230. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25379-9_17
Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology (2007). http://wiki.portal.chalmers.se/agda/pmwiki.php
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science. Prentice Hall (1989)
Spivey, M.: The fuzz type-checker for Z, Version 3.4.1, and the fuzz Manual, 2nd edn. (2008). http://spivey.oriel.ox.ac.uk/corner/Fuzz. Accessed 15 April 2018
Talcott, C.L.: A theory of binding structures and applications to rewriting. Theoret. Comput. Sci. 112, 68–81 (1993). https://doi.org/10.1016/0304-3975(93)90240-T
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Kahl, W. (2018). CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math”. In: Avigad, J., Mahboubi, A. (eds) Interactive Theorem Proving. ITP 2018. Lecture Notes in Computer Science(), vol 10895. Springer, Cham. https://doi.org/10.1007/978-3-319-94821-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-94821-8_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94820-1
Online ISBN: 978-3-319-94821-8
eBook Packages: Computer ScienceComputer Science (R0)