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

Video   전산논리학 소개 (I)     Video (52:12s, 954MB) [mp4]
Video (22:42s, 415MB) [mp4]
   
Video   전산논리학 소개 (II)     Video (50:53s, 906MB) [mp4]
Video (27:38s, 442MB) [mp4]
   

9.2   Introduction to computational logic    CS Chapter 2 [PDF]   
9.4   Propositional logic     CS Chapter 2    

9.11   Hypothetical judgments        

9.16   Local soundness and completeness         
9.18   Proof terms    CS Chapter 3 [PDF]   

9.23   First-order logic (I)     CS Chapter 5 [PDF]   
9.25   First-order logic (II)       

9.30   Inductive datatypes   CS Chapter 6
10.2   First-order logic withd datatypes      

10.7   Induction on terms and predicates    

10.14   Definitional equality       
10.16   Normal proofs  CS Chapter 2   

Midterm

10.28   Normalization       
10.30   Sequent calculus   CS Chapter 4     

11.4   Cut elimination    
11.6   Application of cut elimination     

11.11   Classical logic CS Chapter 7   
11.13   Proof terms for classical logic    

11.25   Sequent calculus for classical logic
11.27   Double-negation translation and CPS translation    

12.2   Inversion in proof search   Pfenning, Chapter 4.1  
12.4   Forward search   Penning, Chapter 5  

12.9   Naming subformulas  
12.11   Review    

Final


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