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
Many logic tutors are out there already, most of them interactive and
rule-based. Although they often come with beautiful graphical interfaces,
we find proof development in these interactive systems disadvantageous for the
We tried an alternative way and followed the Curry-Howard
Isomorphism: proving = programming. We offer a small
language in which proofs can be "programmed", and a compiler-like
tool that verifies steps in the proof file. This has the
- Either one has to learn many command names or click around
- Forgotten proof step usually cannot be inserted easily.
- The result is usually a proof script, incomprehensible for
the human reader.
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
Pfenning, CMU) with great success.
- One can use one's favorite text editor to type the proof.
- Missing steps can be inserted easily.
- Proofs can be reused via cut-and-paste.
- The resulting proof is human-readable like the source code
of a structured programming language.
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 =
[ A & B; % assumption
B & A ]; % conclusion
A & B => B & A
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 Curry-Howard Isomorphism can be studied naturally.
In detail, tutch handles the following theories and concepts:
External features are an easy to use interface and an electronic
homework submission system.
- 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
The tutch documentation is available in different formats:
tutch 0.52 beta is available for Unix platforms. It requires Standard ML of New Jersey, Version 110.
tutch is in an early stage of development. Bug reports and
suggestions for improvements are very welcome. These bugs wait to
Send bug report!
Last modified: Mon Mar 14 15:32:00 CET 2005