CalcCheck
The teaching tool CalcCheck: a proof-checker for Gries and Schneider’s “logical approach to discrete math”. Students following a first-year course based on Gries and Schneider’s LADM textbook had frequently been asking: “how can I know whether my solution is good?”par 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 {sc LaTeX}-formatted calculational proofs, and thus helps students to develop confidence in their own skills in “rigorous mathematical writing”.par 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.
Keywords for this software
References in zbMATH (referenced in 27 articles )
Showing results 1 to 20 of 27.
Sorted by year (- Alain, Mathieu; Desharnais, Jules: Relations as images (2017)
- Carter, Nathan C.; Monks, Kenneth G.: A web-based toolkit for mathematical word processing applications with semantics (2017)
- Boute, Raymond: Why mathematics needs engineering (2016)
- Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra: Well-founded coalgebras, revisited (2015)
- Rocha, Camilo: The formal system of Dijkstra and Scholten (2015)
- Solin, Kim: Dual choice and iteration in an abstract algebra of action (2012)
- Backhouse, Roland; Ferreira, João F.: On Euclid’s algorithm and elementary number theory (2011)
- Jouannaud, Jean-Pierre (ed.); Shao, Zhong (ed.): Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7--9, 2011. Proceedings (2011)
- Kahl, Wolfram: The teaching tool CalcCheck: a proof-checker for Gries and Schneider’s “Logical approach to discrete math” (2011)
- Bohórquez V, Jaime A.: An elementary and unified approach to program correctness (2010)
- Boute, Raymond: Pointfree expression and calculation: From quantification to temporal logic (2010)
- Bherer, Hans; Desharnais, Jules; St-Denis, Richard: Control of parameterized discrete event systems (2009)
- Colvin, Robert; Dongol, Brijesh: A general technique for proving lock-freedom (2009)
- Smith, S.; Yu, W.: A document driven methodology for developing a high quality parallel mesh generation toolbox (2009)
- Tourlakis, George: A new foundation of a complete Boolean equational logic (2009)
- Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter: Specification and verification challenges for sequential object-oriented programs (2007)
- Hehner, Eric C.: From Boolean algebra to unified algebra (2004) MathEduc
- Hehner, Eric C.R.: From Boolean algebra to unified algebra (2004)
- Doberkat, Ernst-Erich; Omodeo, Eugenio G.: Algebraic semantics of ER-models in the context of the calculus of relations. II: Dynamic view (2002)
- Lifschitz, Vladimir: On calculational proofs (2002)