zbMATH — the first resource for mathematics

The teaching tool CalcCheck: a proof-checker for Gries and Schneider’s “Logical approach to discrete math”. (English) Zbl 1350.68238
Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 216-230 (2011).
Summary: Students following a first-year course based on D. Gries and F. B. Schneider’s LADM textbook [A logical approach to discrete math. New York, NY: Springer-Verlag (1993; Zbl 0861.03001)] had frequently been asking: “how can I know whether my solution is good?”
We now report on the development of a proof-checker designed to answer exactly that question, while intentionally not helping to find the solutions in the first place. CalcCheck provides detailed feedback to LaTeX-formatted calculational proofs, and thus helps students to develop confidence in their own skills in “rigorous mathematical writing”.
Gries and Schneider’s book emphasises rigorous development of mathematical results, while striking one particular compromise between full formality and customary, more informal, mathematical practises, and thus teaches aspects of both. This is one source of several unusual requirements for a mechanised proof-checker; other interesting aspects arise from details of their notational conventions.
For the entire collection see [Zbl 1226.68005].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Andrews, P.B., et al.: ETPS: A system to help students write formal proofs. Journal of Automated Reasoning 32, 75–92 (2004), doi:10.1023/B:JARS.0000021871.18776.94 · Zbl 02081545
[2] Abel, A., Chang, B.-Y.E., Pfenning, F.: Human-readable machine-verifiable proofs for teaching constructive logic. In: Proceedings of Workshop on Proof Transformation, Proof Presentation and Complexity of Proofs (PTP 2001). Università degli Studi Siena, Dipartimento di Ingegneria dell’Informazione, Tech. Report 13/0 (2001), http://www2.tcs.ifi.lmu.de/ abel/tutch/
[3] Allen, C., Hand, M.: Logic Primer, 2nd edn. MIT Press (2001), http://logic.tamu.edu/ · Zbl 0988.03001
[4] Aldrich, J., Simmons, R.J., Shin, K.: SASyLF: An educational proof assistant for language theory. In: Huch, F., Parkin, A. (eds.) Proceedings of the 2008 International Workshop on Functional and Declarative Programming in Education, FDPE 2008, pp. 31–40. ACM (2008)
[5] Borak, E., Zalewska, A.: Mizar Course in Logic and Set Theory. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 191–204. Springer, Heidelberg (2007) · Zbl 1202.68373
[6] Contejean, E.: A Certified AC Matching Algorithm. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 70–84. Springer, Heidelberg (2004) · Zbl 1187.68524
[7] Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reasoning 3(2), 153–245 (2010) · Zbl 1211.68369
[8] Goldson, D., Reeves, S., Bornat, R.: A review of several programs for the teaching of logic. The Computer Journal 36, 373–386 (1993)
[9] Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Monographs in Computer Science. Springer, Heidelberg (1993) · Zbl 0861.03001
[10] Heeren, B.: Top Quality Type Error Messages. PhD thesis, Universiteit Utrecht, The Netherlands (September 2005)
[11] Hudak, P., Hughes, J., Jones, S.P., Wadler, P.: A history of Haskell: Being lazy with class. In: Third ACM SIGPLAN History of Programming Languages Conference (HOPL-III), pp. 12–1–12–55. ACM (2007)
[12] James Hoover, H., Rudnicki, P.: Teaching freshman logic with mizar-mse. Mathesis Universalis, 3 (1996), http://www.calculemus.org/MathUniversalis/3/ ; ISSN 1426-3513
[13] Knuth, D.E.: Literate programming. The Computer Journal 27(2), 97–111 (1984) · Zbl 0533.68005
[14] Knuth, D.E.: Literate Programming. CSLI Lecture Notes, vol. 27. Center for the Study of Language and Information (1992) · Zbl 1109.68387
[15] Leijen, D., Meijer, E.: Parsec: Direct style monadic parser combinators for the real world. Technical Report UU-CS-2001-27, Department of Computer Science, Universiteit Utrecht (2001), http://www.cs.uu.nl/ daan/parsec.html
[16] Nipkow, T.: Structured Proofs in Isar/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 259–278. Springer, Heidelberg (2003) · Zbl 1023.68657
[17] Naumowicz, A., Korniłowicz, A.: A Brief Overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67–72. Springer, Heidelberg (2009) · Zbl 1252.68262
[18] Norell, U.: Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology (September 2007)
[19] Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science. Prentice Hall (1989), Out of print; available via http://spivey.oriel.ox.ac.uk/mike/zrm/
[20] Spivey, M.: The fuzz type-checker for Z, Version 3.4.1, and The fuzz Manual, 2 edn. (2008), http://spivey.oriel.ox.ac.uk/mike/fuzz/ (last accessed June 17, 2011)
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.