Resources -- Winter 2009

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

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:

• Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic , Andreas Abel, Bor-Yuh Evan Chang and Frank Pfenning, Proof Transformation, Proof Presentation and Complexity of Proofs (PTP-01). Workshop Proceedings, 2001.

Twelf

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")


Twelf Resources

Twelf Project

Standard ML