Abstract
The proof checker has been developed for teaching calculational proofs in the style of Gries and Schneider’s textbook classic “A Logical Approach to Discrete Math”. While originally only AC-rewriting was supported, we now added also support for operators that are only associative, which is essential for convenience in reasoning about composition of (in particular) relations. We demonstrate how the
language including this and several other recent improvements supports readable and writable machine-checked proofs of interesting relation-algebraic developments.
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
Similar content being viewed by others
Notes
- 1.
In the font used in this paper to display
source listings, the “top” symbol \(\top \) comes out looking like a just slightly smaller version of the letter “T”, and “
” comes out looking almost like a conventional semicolon (which is however currently not used in
).
References
Aarts, C., Backhouse, R.C., Hoogendijk, P., Voermans, E., van der Woude, J.: A relational theory of datatypes. Working document, 387 pp. (1992). http://www.cs.nott.ac.uk/~rcb/papers/abstract.html#book
Bird, R.S., de Moor, O.: Algebra of Programming. International Series in Computer Science, vol. 100. Prentice Hall, Upper Saddle River (1997)
Contejean, E.: A certified AC matching algorithm. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 70–84. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-25979-4_5
Gries, D.: Foundations for calculational logic. In: Broy, M., Schieder, B. (eds.) Mathematical Methods in Program Development. NATO ASI Series (Series F: Computer and Systems Sciences), 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, Heidelberg (1993). https://doi.org/10.1007/978-1-4757-3837-7
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
Kahl, W.: CalcCheck: a proof checker for teaching the “logical approach to discrete math”. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 324–341. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94821-8_19
Schmidt, G., Ströhlein, T.: Relations and Graphs. EATCS Monographs on Theoretical Computer Science. Discrete Mathematics for Computer Scientists. Springer, Heidelberg (1993). https://doi.org/10.1007/978-3-642-77968-8
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River (1989)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Kahl, W. (2018). Calculational Relation-Algebraic Proofs in the Teaching Tool CalcCheck. In: Desharnais, J., Guttmann, W., Joosten, S. (eds) Relational and Algebraic Methods in Computer Science. RAMiCS 2018. Lecture Notes in Computer Science(), vol 11194. Springer, Cham. https://doi.org/10.1007/978-3-030-02149-8_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-02149-8_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02148-1
Online ISBN: 978-3-030-02149-8
eBook Packages: Computer ScienceComputer Science (R0)