Anzeige
Erschienen in:
2018 | OriginalPaper | Buchkapitel
CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math”
verfasst von : Wolfram Kahl
Erschienen in: Interactive Theorem Proving
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
Abstract
For calculational proofs as they are propagated by Gries and Schneider’s textbook classic “A Logical Approach to Discrete Math” (LADM), automated proof checking is feasible, and can provide useful feedback to students acquiring and practicing basic proof skills. We report on the
system which implements a proof checker for a mathematical language that resembles the rigorous but informal mathematical style of LADM so closely that students very quickly recognise the system, which provides them immediate feed-back, as not an obstacle, but as an aid, and realise that the problem is finding proofs.
system which implements a proof checker for a mathematical language that resembles the rigorous but informal mathematical style of LADM so closely that students very quickly recognise the system, which provides them immediate feed-back, as not an obstacle, but as an aid, and realise that the problem is finding proofs.Students interact with this proof checker trough the “web application” front-end
which provides some assistance for proof entry, but intentionally no assistance for proof finding. Upon request, the system displays, side-by-side with the student input, a version of that input annotated with the results of checking each step for correctness.
which provides some assistance for proof entry, but intentionally no assistance for proof finding. Upon request, the system displays, side-by-side with the student input, a version of that input annotated with the results of checking each step for correctness.
has now been used twice for teaching an LADM-based second-year discrete mathematics course, and students have been solving exercises and submitting assignments, midterms, and final exams on the system — for examinations, there is the option to disable proof checking and leave only syntax checking enabled.
also performed the grading, with very limited human overriding necessary.
