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