Week 1 
Tu 04/01 
 Introduction
 Slides: [ ppt
 pdf ]

Th 04/03 
 Discussion of papers (please read before class):
 Logics: standard logics
 Slides: [ ppt
 pdf ]

Week 2 
Tu 04/08 
 Logics: encoding computation in firstorder logic
 Discussion of papers (read and write reviews before
class):
 Flanagan, Leino, Lillibridge, Nelson, Saxe,
State, Extended
Static Checking for Java, PLDI 02
 Lerner, Millstein, Rice, Chambers, Automated
Soundness Proofs for Dataflow Analyses and Transformations via Local
Rules, POPL 05 (sections 1, 2, and 3)
 Also, don't worry if you don't understand all the
details in what you read... We will go through the details in class.
 Slides: [ ppt
 pdf ]

Th 04/10 
 Applications (Part I)
 Slides: [ ppt 
pdf ]

Week 3 
Tu 04/15 
 Applications (Part II)
 Slides: [ ppt
 pdf ]

Th 04/17 
 Finish ESC/Java
 Overview of search in the semantic domain
 Slides: [ ppt
 pdf ]

Week 4 
Tu 04/22 
 Search in the semantic domain
 DPLL
 using SAT solvers incrementally
 Martin Davis and Hilary Putnam, A
Computing Procedure for Quantification Theory, JACM, 1960.
 P. C. Gilmore, A
Proof Method for Quantification Theory: Its Justification and
Realization, IBM Journal of Research and Development, 1960
 Cormac Flanagan, Rajeev Goshi, Xinming Ou,
and James B. Saxe, Theorem
Proving using Lazy Proof Explication, CAV 03
 Slides: [ ppt 
pdf ]

Th 04/24 
 Equality (Part I)
 Congruence closure/Egraph
 Quantifiers
 Skolemization
 Unification
 Matching
 Slides: [ ppt 
pdf ]

Week 5 
Tu 04/29 
 Decision procedures
 Communication between decision procedures
 Slides: [ ppt 
pdf ]

Th 05/01 
 Decision Procedures
 Communication between the heuristic prover and
decision procedures
 Search in the proof domain (Part I)
 Hilbertstyle systems
 natural decuction
 Slides: [ ppt 
pdf ]

Week 6 
Tu 05/06 
 Search in the proof domain (Part II)
 sequent calculus
 tactics and tacticals
 Slides: [ ppt 
pdf ]

Th 05/08 
 Search in the proof domain (Part III)
 Slides: [ ppt 
pdf ]

Week 7 
Tu 05/13 
 Applications (Part III)
 Slides: [ ppt 
pdf ]

Th 05/15 
 Constructive logic, and CurryHoward isomorphism
 Slides: [ ppt 
pdf ]

Week 8 
Tu 05/20 
 Equality (Part II)
 rewrite rules
 inductionless induction
 Slides: [ ppt 
pdf ]

Th 05/22 
 Induction
 induction based on recursive structure
 Boyer and Moore, A
computational logic, Academic Press, 1979, chapter XIV
 Matt Kaufmann, Panagiotis Manolios, and J
Strother Moore, ComputerAided Reasoning: An Approach,
Kluwer Academic Publishers, June, 2000.
 Slides: [ ppt 
pdf ]

Week 9/10 
Tu 05/27 to Th 06/05 
 Final Project Presentations
