Princeton University |
Computer Science 496 |
|
| Date | Topic | |
|---|---|---|
| 2/6-2/9 | Propositional logic, natural deduction, predicate logic | Huth 1.1-1.4, 2.1-2.3 |
| 2/12-2/16 | Automated proof checking, Twelf logical framework | Twelf Users Guide, |
| 2/19-2/23 | Higher-order logic | Hints ... in Twelf |
| 2/26-2/28 | Arithmetic | Hints ... in Twelf |
| 3/2-3/7 | Mathematical abstraction | |
| 3/9-3/16 | Temporal logic | Huth 3.1-3.5; CTL in Twelf |
| 3/26-3/30 | Model checking, SMV | Huth 3.6-3.10 |
Huth & Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2000.
Pfenning & Schuermann, Twelf User's Guide (also in PDF), Carnegie-Mellon University, 1998.
Appel, Hints on proving theorems in Twelf, Princeton University, 2000.