Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math”
verfasst von : Wolfram Kahl
Erschienen in: Certified Programs and Proofs
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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?”
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
${\rm L\kern-.36em\raise.3ex\hbox{\sc a}\kern-.15em T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}$
-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.