15-317 Constructive Logic


To explore bottom-up logic programming we'll be using Lollibot, a linear logic programming language which is a custom fragment of Ollibot

Lollibot is installed on Andrew machines in the course directory. You can run it on a file filename.lob by running

  $ /afs/andrew/course/15/317/bin/lollibot filename.lob
For a quick primer on Lollibot, see Appendix A of the Assignment 10 handout from 2009. Examples from lecture will be available from the course software directory

If you encounter any problems or strange errors while running Lollibot, you should email one of the instructors so they can attempt to correct them as promptly as possible.


For this course we are using GNU Prolog.

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.


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 distribution is available 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 User's Guide for further information on running Tutch.

See the 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.

[ Home | Schedule | Assignments | Handouts | Software ]

annpenny at Andrew