### Resources -- Fall 2007

In this course we will use a proof tutor "Tutch" and implement our own small theorem provers using SML. Below you can find some more information related to Tutch and SML.

### Tutch

**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. A detailed description on how to download and use it can be found at the TUTCH webpage.

Follow these instructions to run tutch:

- Check that the SML version is at least 110.45
- Download from the site:
```
http://www.tcs.informatik.uni-muenchen.de/~abel/tutch/
```

the tar file:
```
http://www.tcs.informatik.uni-muenchen.de/~abel/tutch/tutch-0.52-for-sml-110.45.tar.gz
```

- Run:
`gunzip tutch-0.52-for-sml-110.45.tar.gz`

- Run:
`tar -xvf tutch-0.52-for-sml-110.45.tar`

- Run:
`cd tutch-0.52`

- Type:
`make`

- Type:

```
cd ..
```

ln -s tutch-0.52 tutch

- Now you can run tutch by typing
`tutch/bin/tutch`

You can also check which shell is running by typing "echo %shell" and
then change the .bashrc or .cshrc file by adding in "alias tutch
your_path_to_tutch/bin/tutch"
and then restart the shell and tutch can be run anywhere by just typing "tutch".
For a paper about Tutch and some of the ideas related to it see: