CS 4860 
Applied Logic 
Fall 2010 
Schedule and Lecture NotesHere is a list of the lectures planned for the course. Note that topics are subject to change. 

Date  Topic  Lecture Notes and Readings 
Aug 26  Story of Logic  Lecture 1: pdf Readings: Begriffsschrift and Writing Programs 
Aug 31  Story of Logic and Foreward on Trees (See lecture 1 and lecture 3) 
Lecture 2: pdf Readings: First Order Logic 
Sept 2  Trees and Formulas  Lecture 3: pdf 
Sept 7 

Lecture 4: pdf 
Sept 9  Formulas and Boolean Valuations  Lecture 5: pdf 
Sept 14  Consistency of Tableau  Lecture 6: pdf 
Sept 16  Completeness of Tableau  Lecture 7: pdf Readings Completeness: 2003 Lec 6 
Sept 21  Compactness and SAT Solvers  Lecture 8: pdf

Sept 23  Decidability, SAT, and NP Problems  Lecture 9: pdf 
Sept 28  Lecture 10: pdf 

Sept 30  Introduction to FirstOrder Logic  Lecture 11: pdf Quiz 1 
Oct 5  Syntax of FirstOrder Logic  Lecture 12: pdf 
Oct 7  Semantics of FirstOrder Logic (models, satisfiability, validity) and Tableau Proofs  Lecture 13: pdf 
Oct 12  *FALL BREAK*  
Oct 14  Completeness of FirstOrder Logic  Lecture 14: pdf 
Oct 19  FirstOrder Completeness, Model Checking 
Lecture 15: pdf 
Oct 21  Nonstandard Models, Open Problem on Tableau Search  Lecture 16: pdf 
Oct 26  Block Tableau, Gentzen Systems  Lecture 17: pdf Handout Lecture 18: pdf 
Oct 28  Gentzen Systems  Lecture 18: pdf Handout Lecture 19: pdf 
Nov 2  Refinement Logic for Integers and Lists 
Lecture 19: pdf 
Nov 4  Verification examples, primitive recursive functions, Hoare while rule and iterative proofs, reallife verification  Lecture 20: pdf 
Nov 9  Verification examples, primitive recursive functions, Hoare while rule and iterative proofs, reallife verification examples continued 
Lecture 21: pdf 
Nov 11  Partial recursive functions, lambda terms, unsolvable problems, and Godel's incompleteness theorem, Quiz 2 on induction 
Lecture 22: pdf 
Nov 16  Lecture 23: pdf  
Nov 18  Lecture 24: pdf  
Nov 23  Guest lecture on interactive proof assistants if requested. Thanksgiving break starts Nov. 24. 
Lecture 25: 
Nov 25  *THANKSGIVING BREAK*  
Nov 30  Event Logic and reasoning about protocols. Quiz 4 (final quiz) on proof terms  Lecture 26: Semantics of Evidence 
Dec 2  Summary of course, more of the Story of Logic and review of major concepts 
Lecture 27: Godel's Incompleteness Theorem 
Dec 7  
Dec 9 