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.

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 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.53 beta is available for Unix platforms. It requires Standard ML of New Jersey, Version 110. Have fun!

Date Version Download Instructions
11.02.2009 0.53 for SML 110 working versions (≥ 110.45) tutch-0.53-for-sml-110.45.tar.gz tutch-0.53-for-sml-110.45-INSTALL
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!

Paper and related work

In essence, Tutch's linear proof notation with bracketed assumption is ASCII-fication of Fitch-style proofs, close to the ``boxes'' presentation of Huth and Ryan, with justifications (references to rule names and line numbers) inferred. Letting the system infer the justifications but not the sequence and bracketing of propositions was the original idea of Frank Pfenning. It liberates the student of the tedious work of line numbering and rule referencing, without diminishing the learning experience of what a valid natural deduction proof is and how it can be constructed.

Here is our publication and some comments on related work I found via Google.

  • Andreas Abel, Bor-Yuh Evan Chang, Frank Pfenning
    Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic
    In Proceedings of the Workshop on Proof Transformation and Presentation and Proof Complexities (PTP'01)

    2017-10-19: The error messages of Tutch's parser could be better (at least when it comes to the ``annotated proof'' syntax where one has to write proof terms).

  • Pandora: Proof Assistant for Natural Deduction using Organised Rectangular Areas (Java applet)
    Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai, and Alex Summers

    2017-10-19: Did not run (since Java applets are no longer supported in contemporary browsers).

  • Robert Stärk and Michel Lévy, teachinglogic.liglab.fr/DN (PHP/Ocaml, 2009/2010)

    2017-10-19: Just propositional logic. Very similar to Tutch, bracketing via assume ... therefore. Also constructs proofs automatically. (Not suitable for proof exercises.) The annotation feature is like the verbose Tutch output: reconstructs inference rules.

  • Fitch, Copyright © 2009–2017, Proofmood.

    2017-10-19: Clicking together a Fitch-style proof (formulas can be entered on the keyboard). Verifying the proof always failed with error ``Premises are missing''. Had to seriously read the help page to understand how to enter the ``premises'' (line numbers referred to by justifications): by right-clicking left of the beginning of a line I want to refer to.

  • Elin Björnsson, Fredrik Johansson, Jan Liu, Henry Ly, Jesper Olsson, and Andreas Widbom
    Proof Editor for Natural Deduction in First-order Logic
    The Evaluation of an Educational Aiding Tool for Students Learning Logic
    Bachelor’s thesis in Computer Science, Department of Computer Science and Engineering, Chalmers University of Technology and University of Gothenburg, 2017

    Conan (Java 8) Proof tutor for first-order predicate logic.

    2017-10-19: Interface: text input (single formulas), line insertion/deletion, clicking on rule names. Assumptions have to be put in boxes. Justifications in form of rule names and line numbers have to be given.
    Problems:

    • Cannot place subproof into a box retrospectively. Box has to be created first before its content.
    • Inserting lines does not update the referenced line numbers.
This list is not exhaustive. There seems to be a plethora of pedagogic proof assistants.

License

Tutch is unlicensed. The LICENSE file is reproduced here:

This is free and unencumbered software released into the public domain.

Anyone is free to copy, modify, publish, use, compile, sell, or distribute this software, either in source code form or as a compiled binary, for any purpose, commercial or non-commercial, and by any means.

In jurisdictions that recognize copyright laws, the author or authors of this software dedicate any and all copyright interest in the software to the public domain. We make this dedication for the benefit of the public at large and to the detriment of our heirs and successors. We intend this dedication to be an overt act of relinquishment in perpetuity of all present and future rights to this software under copyright law.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

For more information, please refer to http://unlicense.org


Andreas Abel
Last modified: 12 Sep 2017