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.
Cite
CITATION STYLE
Kahl, W. (2018). Calculational relation-algebraic proofs in the teaching tool CALCCHECK. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11194 LNCS, pp. 366–384). Springer Verlag. https://doi.org/10.1007/978-3-030-02149-8_22
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
