zbMATH — the first resource for mathematics

Calculational relation-algebraic proofs in the teaching tool CalcCheck. (English) Zbl 1462.68216
Desharnais, Jules (ed.) et al., Relational and algebraic methods in computer science. 17th international conference, RAMiCS 2018, Groningen, The Netherlands, October 29 – November 1, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11194, 366-384 (2018).
Summary: The proof checker CalcCheck has been developed for teaching calculational proofs in the style of D. Gries and F. B. Schneider’s textbook classic [A logical approach to discrete math. New York, NY: Springer-Verlag (1993; Zbl 0861.03001)]. 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 CalcCheck language including this and several other recent improvements supports readable and writable machine-checked proofs of interesting relation-algebraic developments.
For the entire collection see [Zbl 1398.68023].

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
97U70 Technological tools, calculators (aspects of mathematics education)
Full Text: DOI