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.3   Propositional logic     CS Chapter 2    
9.5   Hypothetical judgments        

9.10   Local soundness and completeness         
9.12   Proof terms    CS Chapter 3   

9.17   First-order logic (I)     CS Chapter 5    

10.1   First-order logic (II)       
10.3   Inductive datatypes   CS Chapter 6

10.8   First-order logic withd datatypes      
10.10   Induction on terms and predicates    

10.15   Definitional equality       
10.17   Normal proofs  CS Chapter 2   

10.22   Normalization       
10.24   Sequent calculus   CS Chapter 4     

10.29   Cut elimination    
10.31   Application of cut elimination     

11.5   Classical logic CS Chapter 7   
11.7   Proof terms for classical logic    

11.12   Sequent calculus for classical logic
11.14   Double-negation translation and CPS translation    

11.19   Inversion in proof search   Pfenning, Chapter 4.1  
11.21   Forward search   Penning, Chapter 5  

11.26   Naming subformulas  
11.28   Review    


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