576 Course Page

CS 576: Topics in Automated Deduction

The website for the page is an evolving entity. Please check back periodically.

Instructor: Prof. Elsa Gunter
Email: egunter@cs.uiuc.edu
Office: 2112 SC
Phone: 265-6118
Office hours: Wednesdays 11:00am - 12:15 am, Fridays 11:00am - 12:15 pm,

Here are some directories containing course material: doc

Lecture notes for the course (cs576)

Homework exercises (aka MPs)

Documentation for Isabelle (including textbook)

Downloads for installing Isabelle and ProofGeneral

Theory files for the demos given in class

The class newsgroup is found at: news://class.cs567

Here is a link to the main Isabelle website:

http://www.cl.cam.ac.uk/Research/HVG/Isabelle/

To use Isabelle/HOL on the csil-linux and csil-core machines, you need to make a couple of additions you environment on these machines. First, you want to add /home/class/sp08/cs576/bin to your path environment variable. If you are using either the csh or the tcsh shell, then you may do this by adding

set path=($path /home/class/sp08/cs576/bin)

to the end of your .cshrc file. Make a backup of this file, in case you need to restore it to its original form. Adding this directory to you path will enable the executables associated with Isabelle to be automatically found. The standard way to run Isabelle is through using the ProofGeneral interface in either Emacs or XEmacs. To enable this, you need to have emacs/xemacs load a file at startup. Assuming you have the standard .emacs file, which loads ~/.xemacs/init.el, you want to add to the end of your ~/.xemacs/init.el the following command:

(load-file "/home/class/sp08/cs576/public_html/ProofGeneral/generic/proof-site.el")

Once you have made these two additions, when you start editing a file ending in .thy, emacs should start up ProofGeneral and Isabelle and you should be able to use the buttons and pull down menus to interact with Isabelle, as you have seen in class. I have found the startup on the csil-core machines to be remarkably slow (taking minutes). Please be patient. If it takes more then ten minutes, then you probably have problem.