What's new?
Introduction
tutch is a tool for checking constructive proofs.
It is aimed at teaching intuitionistic logic and "how to
prove". Its name is short for tutorial proof
checker.
Many logic tutors are out there already, most of them interactive and
rulebased. Although they often come with beautiful graphical interfaces,
we find proof development in these interactive systems disadvantageous for the
following reasons:
 Either one has to learn many command names or click around
much.
 Forgotten proof step usually cannot be inserted easily.
 The result is usually a proof script, incomprehensible for
the human reader.
We tried an alternative way and followed the CurryHoward
Isomorphism: proving = programming. We offer a small
language in which proofs can be "programmed", and a compilerlike
tool that verifies steps in the proof file. This has the
following advantages:
 One can use one's favorite text editor to type the proof.
 Missing steps can be inserted easily.
 Proofs can be reused via cutandpaste.
 The resulting proof is humanreadable like the source code
of a structured programming language.
We believe that with tutch, students learn to write a proof rather
than just how to use a specific proof system. In Fall 2000
tutch was used in the course Constructive
Logic (Frank
Pfenning, CMU) with great success.
Courses using Tutch
Example
Here a short glimpse at how proofs in tutch look like. Everything
from "%" to the end of a line is considered a comment. A
frame construct "[...]" introduces a hypothesis in the
first line which is available within the frame. Each step follows
from the previous by a single natural deduction inference step.
proof andComm: A & B => B & A =
begin
[ A & B; % assumption
A;
B;
B & A ]; % conclusion
A & B => B & A
end;

Features
tutch supports certain constructive theories from propositional
logic to Heyting Arithmetic, which allows to do a little "software
verification". Since it uses the same syntax for proof terms and
programs, the CurryHoward Isomorphism can be studied naturally.
In detail, tutch handles the following theories and concepts:
 Natural Deduction (ND) proofs in Intuitonistic Predicate Logic
 ND proofs annotated with proof terms
 Proving with proof terms alone
 Primitve Recursion over booleans, natural numbers and lists
 Heyting Arithmetic: induction, equality, inequality
External features are an easy to use interface and an electronic
homework submission system.
Documentation
The tutch documentation is available in different formats:
Download
tutch 0.52 beta is available for Unix platforms. It requires Standard ML of New Jersey, Version 110.
Have fun!
Known bugs
tutch is in an early stage of development. Bug reports and
suggestions for improvements are very welcome. These bugs wait to
be fixed:
Send bug report!
Andreas Abel
Last modified: Mon Mar 14 15:32:00 CET 2005
