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.