| |
|
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:
- 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.53 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!
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
|
|