tutch Home Page
 

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 rule-based. 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 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 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 cut-and-paste.
  • The resulting proof is human-readable 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.

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 Curry-Howard Isomorphism can be studied naturally. In detail, tutch handles the following theories and concepts:
  1. Natural Deduction (ND) proofs in Intuitonistic Predicate Logic
  2. ND proofs annotated with proof terms
  3. Proving with proof terms alone
  4. Primitve Recursion over booleans, natural numbers and lists
  5. 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!

Date Version Download Instructions
13.06.2004 0.52 for SML 110 working versions (≥ 110.45) tutch-0.52-for-sml-110.45.tar.gz tutch-0.52-for-sml-110.45-INSTALL
24.10.2002 0.52 beta (for SML 110 official release) tutch-0.52.tar.gz tutch-0.52-INSTALL
10.07.2001 0.51 beta tutch-0.51.tar.gz tutch-0.51-INSTALL

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