posted on 2002-04-01, 00:00authored byAndreas 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.