Calculational relation-algebraic proofs in the teaching tool CalcCheck. (English) Zbl 1462.68217

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 writeable machine-checked proofs of interesting relation-algebraic developments.


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


Zbl 0861.03001
Full Text: DOI


[1] Aarts, C.; Backhouse, R. C.; Hoogendijk, P.; Voermans, E.; van der Woude, J., A relational theory of datatypes (1992), Working document, 387 pp., available at
[2] Back, R.-J., Structured derivations: A unified proof style for teaching mathematics, Form. Asp. Comput., 22, 5, 629-661 (2010) · Zbl 1217.03043
[3] Back, R.-J.; Bos, V.; Eriksson, J., MathEdit: Tool support for structured calculational proofs (2007), Turku Centre for Comp. Sci., TUCS Tech. Rep. 854
[4] Berghammer, R.; Schmidt, G.; Zierer, H., Symmetric quotients and domain constructions, Inf. Process. Lett., 33, 3, 163-168 (1989) · Zbl 0689.68095
[5] Bertot, Y.; Castéran, P., Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science (2004), Springer · Zbl 1069.68095
[6] Bird, R. S.; de Moor, O., Algebra of Programming, International Series in Computer Science, vol. 100 (1997), Prentice Hall
[7] Boole, G., The Mathematical Analysis of Logic, Being an Essay Toward a Calculus of Deductive Reasoning (1847), Macmillan: Macmillan Cambridge
[8] Buchberger, B.; Jebelean, T.; Kutsia, T.; Maletzky, A.; Windsteiger, W., Theorema 2.0: Computer-assisted natural-style mathematics, J. Formaliz. Reason., 9, 1, 149-185 (2016) · Zbl 1451.68319
[9] Carter, N. C.; Monks, K. G., A web-based toolkit for mathematical word processing applications with semantics, (Geuvers, H.; etal., CICM 2017 (2017), Springer Intl.: Springer Intl. Cham), 272-291 · Zbl 1367.68332
[10] Contejean, E., A certified AC matching algorithm, (van Oostrom, V., RTA 2004. RTA 2004, LNCS, vol. 3091 (2004), Springer), 70-84 · Zbl 1187.68524
[11] Cuoq, P.; Kirchner, F.; Kosmatov, N.; Prevosto, V.; Signoles, J.; Yakobowski, B., Frama-c: a software analysis perspective, (Proceedings of the 10th International Conference on Software Engineering and Formal Methods. Proceedings of the 10th International Conference on Software Engineering and Formal Methods, SEFM’12 (2012), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 233-247
[12] De Morgan, A., On the syllogism: IV, and on the logic of relations, Trans. Cambridge Philos. Soc., 10, 331-358 (1864), (read April 23, 1860) Reprinted in [13]
[13] De Morgan, A., On the Syllogism, and Other Logical Writings (1966), Yale Univ. Press: Yale Univ. Press New Haven · Zbl 0168.00106
[14] de Moura, L.; Kong, S.; Avigad, J.; van Doorn, F.; von Raumer, J., The Lean theorem prover (system description), (Felty, A. P.; Middeldorp, A., CADE 2015 (2015), Springer International Publishing: Springer International Publishing Cham), 378-388 · Zbl 1465.68279
[15] Freyd, P. J.; Scedrov, A., Categories, Allegories, North-Holland Mathematical Library, vol. 39 (1990), North-Holland: North-Holland Amsterdam · Zbl 0698.18002
[16] Grabowski, A.; Korniłowicz, A.; Naumowicz, A., Mizar in a nutshell, J. Formaliz. Reason., 3, 2, 153-245 (2010) · Zbl 1211.68369
[17] Gries, D., Foundations for calculational logic, (Broy, M.; Schieder, B., Mathematical Methods in Program Development (1997), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 83-126 · Zbl 0929.03037
[18] Gries, D.; Schneider, F. B., A Logical Approach to, Discrete Math. Monographs in Computer Science (1993), Springer · Zbl 0861.03001
[19] Gruber Markdown, J. (2004)
[20] Kahl, W., Calculational relation-algebraic proofs in Isabelle/Isar, (Berghammer, R.; Möller, B.; Struth, G., RelMiCS/AKA 2003. RelMiCS/AKA 2003, LNCS, vol. 3051 (2003), Springer), 178-190 · Zbl 1088.68772
[21] Kahl, W., Refactoring heterogeneous relation algebras around ordered categories and converse, J. Relat. Methods Comp. Sci., 1, 277-313 (2004)
[22] Kahl, W., Dependently-typed formalisation of relation-algebraic abstractions, (de Swart, H., RAMiCS 2011. RAMiCS 2011, LNCS, vol. 6663 (2011), Springer), 230-247 · Zbl 1329.68063
[23] Kahl, W., The teaching tool CalcCheck: A proof-checker for Gries and Schneider’s “Logical Approach to Discrete Math”, (Jouannaud, J.-P.; Shao, Z., CPP 2011. CPP 2011, LNCS, vol. 7086 (2011), Springer), 216-230 · Zbl 1350.68238
[24] Kahl, W., CalcCheck: A proof checker for teaching the “logical approach to discrete math”, (Avigad, J.; Mahboubi, A., ITP 2018. ITP 2018, LNCS, vol. 10895 (2018), Springer: Springer Cham), 324-341 · Zbl 1462.68215
[25] Kahl, W., Calculational relation-algebraic proofs in the teaching tool CalcCheck, (Desharnais, J.; Guttmann, W.; Joosten, S., RAMiCS 2018. RAMiCS 2018, LNCS, vol. 11194 (2018), Springer: Springer Cham), 366-384 · Zbl 1462.68216
[26] S. Leonard, The text/markdown Media Type, RFC 7763. Internet Engineering Task Force (IETF), 2016.
[27] S. Leonard, Guidance on Markdown: Design Philosophies, Stability Strategies, and Select Registrations, RFC 7764. Internet Engineering Task Force (IETF), 2016.
[28] Pandoc, J. MacFarlane (2006)
[29] Maddux, R. D., Relation Algebras, Studies in Logic and the Foundations of Mathematics, vol. 150 (2006), Elsevier Science: Elsevier Science Oxford
[30] Mayrhofer, G.; Saminger, S.; Windsteiger, W., CreaComp: Experimental Formal Mathematics for the Classroom, (Li, S.; Wang, D.; Zhang, J.-Z., Symbolic Computation and Education (2007), World Scientific Publishing Co.: World Scientific Publishing Co. Singapore, New Jersey), 94-114
[31] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL — A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283 (2002), Springer · Zbl 0994.68131
[32] Norell, U., Towards a Practical Programming Language Based on Dependent Type Theory (2007), Dept. Comp. Sci. and Eng., Chalmers Univ. of Technology, See also
[33] Owre, S.; Shankar, N.; Rushby, J. M.; Stringer-Calvert, D. W.J., PVS Language Reference, Version 2.3 (1999), SRI International
[34] Peirce, C. S., Description of a notation for the logic of relatives, resulting from an amplification of the conceptions of Boole’s calculus of logic, Mem. Am. Acad. Arts Sci., 9, 317-378 (1870), Reprint by Welch, Bigelow and Co., Cambridge, MA, 1870, pp. 1-62. Also reprinted in [35] and [36]
[35] Peirce, C. S., (Hartshorne, C.; Weiss, P., C. S. Peirce Collected Papers (1933), Harvard Univ. Press: Harvard Univ. Press Cambridge)
[36] Peirce, C. S., (Moore, Edward C.; Fisch, Max H.; Kloesel, Christian J. W.; Roberts, Don D.; Ziegler, Lynn A., Writings of Charles S. Peirce, A Chronological Edition (1984), Indiana Univ. Press: Indiana Univ. Press Bloomington)
[37] Schmidt, G.; Ströhlein, T., Relations and Graphs, Discrete Mathematics for Computer Scientists, EATCS-Monographs on Theoret. Comput. Sci. (1993), Springer · Zbl 0900.68328
[38] Schröder, E., Vorlesungen über die Algebra der Logik (exacte Logik), (Algebra und Logik der Relative, part I, vol. 3 (1895), Teubner: Teubner Leipzig), published by Chelsea, 1966 · JFM 26.0074.01
[39] Sommer, R.; Nuckols, G., A proof environment for teaching mathematics, J. Autom. Reason., 32, 227-258 (2004)
[40] Spivey, J. M., The Z Notation: A Reference Manual (1989), Prentice Hall, Prentice Hall International Series in Computer Science · Zbl 0777.68003
[41] Tarski, A., On the calculus of relations, J. Symb. Log., 6, 3, 73-89 (1941) · JFM 67.0973.02
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.