Princeton University
Computer Science Department

Computer Science 598A
Automated Theorem Proving

Andrew Appel

Schedule
Spring 2003

General Information | Schedule | Assignments | Announcements

Schedule (very tentative, subject to rearrangement)

DateTopic
Feb. 3 Propositional logic, natural deduction Huth 1.1-1.4
Feb 10 Predicate logic; Twelf logical framework Huth 2.1-2.3; Twelf Users Guide (v1.4),
Feb 17Higher-order logicHints ... in Twelf
Feb 24ArithmeticHints ... in Twelf
March 3Mathematical abstraction
March 10Temporal logicHuth 3.1-3.5
March 24Model checking, SMVHuth 3.6-3.10; Examples
March 31Prolog-style programming in Twelf Twelf Users Guide
April 7Hoare logicHuth 4
April 14Semantic models of logic programsWu et al.; Conjunct provers
April 21Semantic models of type systems; dependently typed provers
April 28Union-find; Tactical-style proversAppel & Felty

Readings

Huth & Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2000.

Pfenning & Schuermann, Twelf User's Guide, Carnegie-Mellon University, 1998-2002.

Appel, Hints on proving theorems in Twelf, Princeton University, 2000.

Foundational Proof Checkers with Small Witnesses, by Dinghao Wu, Andrew W. Appel, and Aaron Stump.

Dependent Types Ensure Partial Correctness of Theorem Provers, by Andrew W. Appel and Amy P. Felty. Accepted for publication, Journal of Functional Programming, 2002.