Princeton University Computer Science Department

Computer Science 598A Automated Theorem Proving Andrew Appel

General Information Spring 2003

Course Summary. Logic, semiautomatic theorem proving, and automatic proof checking have applications in program verification, network and cryptographic protocols, computer security, mathematics, and computer architecture. This course covers principles, methods, and applications, with an emphasis on hands-on learning how to use the tools of the trade. Specific topics include higher-order logic, the Twelf logical framework, logic programming in (a higher-order) Prolog, representation of methamatics in logic, computation tree logic and model checking using the SMV system, Hoare-style program verification, and the implementation of tactical-style theorem provers.

Administrative Information

Lectures: MW 9:30-10:50, Room: TBD

Professor: Andrew Appel - 409 CS Building - 258-4627 appel@cs.princeton.edu

Software

Twelf

We will be using Twelf 1.4. This is installed on the CS department "shades" and "penguins" servers; just put the following two lines in your emacs profile, (~/.emacs):

(setq twelf-root "/cmnusr/local/sml/twelf/")
(load (concat twelf-root "emacs/twelf-init.el"))

Or you can install Twelf on your own machine:

• README-1-4
• twelf-1-4-0.i386.rpm binary distribution for Red Hat Linux 7.1 (2.9 MB) (README-1-4-rpm)
• twelf-1-4.exe binary for Windows (5.1 MB)

SMV

We will also be using the SMV model checker. It is installed on the CS cycle servers as /usr/local/smv, or you can get it from the SMV web site and install it on your own machine.