CSE-433 Logic in Computer Science - Schedule

[ Home | Schedule | Assignments | Software | Resources | Students ] gla@postech Sungwoo Park


  • The schedule is subject to change throughout the semester.
  • CS = Course Notes. (The up-to-date version including all chapters [PS, PDF])
Date    Lecture   Reading    Assignment Due

Thu Sep 1   Overview of logic [PPT]    CS Chapter 1    

Tue Sep 6   Propositional logic     CS Chapter 2     W1
Thu Sep 8   Introduction to Coq     

Tue Sep 13   (Chusok)         
Thu Sep 15   Hypothetical judgments         P1

Tue Sep 20   Local soundness and completeness       
Thu Sep 22   Proof terms    CS Chapter 3     P2, W2

Tue Sep 27   First-order logic (I)     CS Chapter 5    
Thu Sep 29   First-order logic (II)          P3, W3

Tue Oct 4   Inductive datatypes     
Thu Oct 6   First-order logic withd datatypes   CS Chapter 6    

Tue Oct 11   Induction on terms     
Thu Oct 13   Induction on predicates      P4

Tue Oct 18   Definitional equality       
Thu Oct 19   Examples      

Midterm (Oct 20 - Oct 26)

Thu Oct 27   Midterm (In class, 9:00am - 10:30am)     P5,6

Tue Nov 1   Normal proofs      
Thu Nov 3   Normalization       

Tue Nov 8   Sequents CS Chapter 4     
Thu Nov 10   Sequent calculus       P7

Tue Nov 15   Cut elimination       Quiz [PDF]
Thu Nov 17   Application of cut elimination   

Tue Nov 22   Classical logic CS Chapter 7    P8
Thu Nov 24   Double-negation translation and CPS translation      

Tue Nov 29   Inversion in proof search Pfenning, Chapter 4.1   P9
Thu Dec 1   Backward search     

Tue Dec 6   Forward search    Penning, Chapter 5  
Tue Dec 8   Naming subformulas   

Thu Dec 13   Review       P10

Wed Dec 27   Final (7:00pm - 10:00pm)    


[ Home | Schedule | Assignments | Software | Resources | Students ] gla@postech Sungwoo Park