Calculational Relation-Algebraic Proofs in the Teaching Tool CalcCheck

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.