COMP 426: Automated Reasoning
Home : Course Information : Schedule : Assignments : Handouts : Resources

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 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:

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: