1. Introduction

Nomen est omen: Tutch is an abbreviation of Tutorial proof checker. Tutch is a checker for the validity of formal proofs in constructive logic. It is still under development, but it is aimed towards handling first-order predicate logic with a few built-in inductive data types and recursive functions over these data types. The strength of the system will be the same as of Heyting Arithmetic (HA).

Tutch is meant to be a tool to assist teaching of logic. It should help students to learn how to formally prove propositions. We believe this is easier if they are allowed to write down the proof like the code of a program and let it be checked afterwards in a compiler-like tool, instead of trying to assemble it with "hands tied" in an interactive system, where they have to search for the appropriate tactics and apply them in the right order.

We try to develop user-friendly error messages. Any feedback on cryptic messages or suggestion of better messages is highly valuable for us. Please sent feedback to abel@informatik.uni-muenchen.de.

Tutch is not:

1. A professional tool for verification
2. An automated theorem prover
3. A logical framework
4. A point-and-click program

About this document

This document is meant as a user's guide. It's neither a reference, where Tutch input is defined formally and all options are listed in alphabetical order, nor a "First Steps Tutch Tour for Dummies", where every keystroke is explained. Instead it tries to be a quick and reasonable introduction along examples, which I believe communicate the basic ideas most quickly and intuitively.

Have fun!