Carnegie Mellon University
Browse

Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic

Download (229.38 kB)
journal contribution
posted on 2002-04-01, 00:00 authored by Andreas Abel, Bor-Yuh Evan Chang, Frank Pfenning
A linear syntax for natural deduction proofs in first-order intuitionistic logic is presented, which has been an effective tool for teaching logic. The proof checking algorithm is also given, which is the core of the tutorial proof checker Tutch. This syntax is then extended to proofs on the assertion level which resemble single inferences one would make in a rigorous proof. The resulting language has only four constructs. Checking of these proofs is decidable, and an efficient algorithm is given.

History

Date

2002-04-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC