Home
Schedule
Assignments
Software
 
Discussion board:
academic.cs.15-317
 
  

15-317 Constructive Logic
Software

Twelf

To represent and prove things about logics, we'll be using Twelf, an implementation of the logical framework LF. The Twelf Wiki linked above is a great source of information about Twelf.

Twelf is installed on Andrew machines in the course directory. You can interact with the Twelf server directly by running: 

  /afs/andrew/course/15/317/bin/twelf-server
For a quick tutorial on how to use the Twelf server, see the Twelf Wiki's article on using Twelf without Emacs.

To use the Twelf Emacs mode, add the following to your ~/.emacs file: 

  (setq twelf-root "/afs/andrew/course/15/317/twelf/")
  (load (concat twelf-root "emacs/twelf-init.el"))
For a quick tutorial on how to use the Emacs mode to develop Twelf code, see the Twelf Wiki's article on using Twelf with Emacs.

To get vim syntax highlighting, copy the contents of 

  /afs/andrew/course/15/317/twelf/vim
to your ~/.vim directory. Then Twelf syntax highlighting will automatically be enabled when editing .elf files.

You can also download Twelf as a source or binary distribution if you'd like to install it on your own machine.

Prolog

For this course we are using GNU Prolog, release 1.4.1.

You can run the Andrew installation of GNU Prolog either by running the script: 

  $ /afs/andrew/course/15/317/bin/runprolog
or by adding the directory /afs/andrew/course/15/317/bin to your path and running gprolog. You can also download a distribution from the GNU Prolog web site and install it on your own machine.

Most installations of vim and emacs have editing modes for Prolog code, but the default is to treat .pl files as Perl code. To switch to the Prolog mode in vim, use the command :setf prolog. To switch to the Prolog mode in emacs, use the command M-x prolog-mode.

Tutch

In the first part of this course you will be using a proof checker called Tutch (short for Tutorial Proof Checker). As the name indicates, it checks the validity of formal proofs that users provide.

The current version of course software Tutch is 0.52 beta, October 24, 2002. The distribution is available from the course software directory, or directly from the Tutch home page.

On Andrew, Tutch is installed in /afs/andrew/course/15/317/bin. The executable files are tutch, submit and status; they should work under linux.andrew.cmu.edu and directly on the machines in the cluster with Linux. The easiest way to run them is with 

  $ /afs/andrew/course/15/317/bin/tutch filename.tut

where filename.tut contains your proof or proofs. See the documentation for further information on running Tutch.

See Tutch Overview for an introduction to using the Tutch proof checker. The examples from the overview are available here.

The section on Requirements and Submission contains information on how to submit your homework.

Syntax Highlighting

For Vim, see Vim Syntax. For Emacs, Evan Cavallo has graciously written a Tutch mode.

[ Home | Schedule | Assignments | Software ]