A Tutorial Proof Checker, Reloaded

Background

Natural deduction is a formal calculus to write proofs step-by-step, where each proposition must follow from previously proven propositions by a single inference rule. Natural deduction is typically part of a course on logic at the undergraduate or graduate level. However, many students struggle writing correct natural deduction proofs, especially when it comes to the correct handling of assumptions. There are many proof tutors on the web, which allow the construction of natural deduction by a structure editor.

Tutch is a proof tutor for natural deduction targeting especially computer science students. The student writes a proof in a block-structured syntax not unlike to familiar programming languages like C, JAVA, or PASCAL. Since the proof is just program text, it can be edited in any order and way, including cut-paste-modify. (This is seldom supported by structure editors.) When run by the user, the Tutch batch program checks the proof not unlike the type-checker in a compiler. Errors are reported by source location. In verbose mode, Tutch prints the proof back to the user, with reconstructed justifications for each step (which rule was applied, which premises were used). Tutch is used in several logic courses around the world, but has been written in SML and is a bit hard to install. Also, the interaction is on the command line and could be more comfortable.

Project description

Here, we propose a reimplementation and refurbishing of Tutch. It shall be equipped with an IDE that gives the user constant feedback on her proof. Error messages should be intuitive, even for parse errors. Time permitting, Tutch will be made parametric in the logic it supports, reading a logic-definition file that can be constructed by the course instructor.

Suggested reading

Target group

Prerequisites

Proposal author

Andreas Abel