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 39 articles , 2 standard articles )
Showing results 1 to 20 of 39.
Sorted by year (- Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
- Klimek, Radosław: Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models (2019)
- Diallo, Nafi; Ghardallou, Wided; Desharnais, Jules; Mili, Ali: Convergence: integrating termination and abort-freedom (2018)
- Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2018)
- Kahl, Wolfram: CalcCheck: a proof checker for teaching the “Logical approach to discrete math” (2018)
- 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)
- Dyba, Martin; El-Zekey, Moataz; Novák, Vilém: Non-commutative first-order EQ-logics (2016)
- Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra: Well-founded coalgebras, revisited (2015)
- Rocha, Camilo: The formal system of Dijkstra and Scholten (2015)
- Klimek, Radosław: A system for deduction-based formal verification of workflow-oriented software models (2014)
- 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)