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:
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
gunzip tutch-0.52-for-sml-110.45.tar.gz
tar -xvf tutch-0.52-for-sml-110.45.tar
cd tutch-0.52
make
cd ..
ln -s tutch-0.52 tutch
tutch/bin/tutch