Calculational Relation-Algebraic Proofs in the Teaching Tool CalcCheck

摘要

The proof checker CalcCheck has been developed for teaching calculational proofs in the style of Cries 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 CalcCheck language including this and several other recent improvements supports readable and writable machine-checked proofs of interesting relation-algebraic developments.