In this course we will use a proof tutor "Tutch" and explore logic programming using the Twelf system. Below you can find some more information related to Tutch and Twelf.
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
We will be using the Twelf system, which is an implementation of a logical framework (LF), a constraint logic programming language (Elf), and a meta-theorem prover. In this course, we mostly will concentrate on logic programming. As you will notice, when you browse some of the information regarding Twelf, logic programming is not its primary focus. Below is a quick introduction. For more information see the Twelf home page and the User's Guide for Version 1.3. You may also find the Twelf Wiki useful.
To run Twelf in the SOCS-domain, you need to add the following to your .emacs or .xemacs/init.el file:
;; ============================
;; Twelf
;; ============================
(setq load-path (cons "/usr/share/twelf/emacs/" load-path))
(setq twelf-root "/usr/share/twelf/")
;;; own version of twelf-init
(load "/usr/share/twelf/emacs/twelf-init.el")