COMP 527: Logic and Computation
Home : Course Information : Schedule : Assignments : Handouts : Resources

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


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