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 23 articles )
Showing results 1 to 20 of 23.
Sorted by year (- 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)
- 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)
- Höfner, Peter: Semiring neighbours: An algebraic embedding and extension of neighbourhood logic. (2007)
- Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter: Specification and verification challenges for sequential object-oriented programs (2007)
- Jones, Cliff B.: Reasoning about partial functions in the formal development of programs. (2006)
- Hehner, Eric C.: From Boolean algebra to unified algebra (2004)
- 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)
- Backhouse, Roland; Fokkinga, Maarten: The associativity of equivalence and the Towers of Hanoi problem (2001)
- Diaconescu, Razvan; Futatsugi, Kokichi: An overview of cafeobj. (1998)
- Westmoreland, Michael; Krone, Joan; Schumacher, Benjamin: Analysis of billiard ball computation using phase space logics (1998)
- Simons, Martin; Weber, Matthias: An approach to literate and structured formal developments (1996)