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].