Personal tools
You are here: Home › Courses › CS402 Intro. to Logic, Spring 2013

CS402 Intro. to Logic, Spring 2013

Announcement

  • No class on Mar 19 and 21 due to ICST 2013 at Luxembourg
  • Make-up class on April 1 (Mon) 8:00 PM at Rm#114
  • Help desk for HW #1 on April 9 (Tuesday) 7:00 - 9:00 PM at Rm# 2438, CS building (E3-1)
  • The midterm on April 30th 09:00 - 10:20 AM @Rm 113, N1 (김병호 IT)
  • No class on May 23 for ICSE 2013
  • Make-up class on May 30 (Thursday) 08:00 - 10:30 PM @Rm 113, N1 (김병호 IT)
  • The final exam on June 21st (Friday) 7:00 - 9:00 PM  @Rm 113, N1 (김병호 IT)

Administrative Information

Office: 2434 (located at the east wing)

Phone:042-350-3543

E-mail: moonzoo@cs.kaist.ac.kr

Office hour: Tues/Thurs 5:00-7:00 PM (e-mail reservation preferred)

  • Teaching assistants:   Shin Hong and Seokhyun Moon ( seokhyeon.mun@gmail.com )
  • Lecture room:  N1 (김병호IT) Rm#113
  • Lecture hours: 9:00-10:30 Tues/Thur
  • Grading: attendance, quiz, class participation: 20%, HW: 30%, midterm exam.: 25 %,final exam.: 25 %  
    • Late HW is accepted with 20% penalty in 1 day, 40% penalty in 3 days.  HW will not be accepted after that. 
    • You should submit both hadcopy and softcopy. Missing either format will receive 10% penalty.
    • More than 8 absences of class will get F grade
      • Late attendance is considered as 1/3 absence, so to start class on time. 
  • Note: The official language in the class is English. All students should submit homework and exam in English.
  • Pre-requisite:
    • CS204 Discrete mathematics
    • basic understanding of Unix/Linux shell and utilities and C programming (this course does NOT provide support for tool installation and error handling during tool usage)
  • CS 402 BBS at NOAH : All class attendants are encouraged to write questions or comments on the class at the BBS. 

 

Course Material

  • Main text:
  • Recommended reading list:
    • "A Mathematical Introduction to Logic" by H.B.Enderton, Academic Press, 2nd edition
    • "Logic and Structure" by D.V.Dalen, Springer, 4th edition

Course Schedule

Wk 1: Introduction

Mar 5: Administrative Introduction

Mar 7:  “Intro. to logic (1/2)”

Mar 12 :  “Intro. to logic (2/2)”

Mar 14: Propositional logic - semantics (1/3)

Mar 26, 28 : Propositional logic - semantics (2/3)

Apr 1:  Propositional logic - semantics (3/3)

Apr 2:  Propositional normal forms

Apr 4 : Prop. logic application 1: How to solve Sudoku?

Apr 9 : Prop. logic application 2: How to Test/Verify my C program?

Apr 11: Propositional logic - deductive systems (natural deduction),

Apr 16: Propositional logic -deductive Systems (Gentzen system g)

Apr 18 : Propositional logic -deductive Systems (Hilbert system H))

Apr 23 : Propositional logic- soundness and completeness of H

Apr 30 : Midterm exam

May 2 : Predicate logic - semantics (1/3)

May 7 : Predicate logic - semantics (2/3)

May 9 : Predicate logic - semantics (3/3), 

May 14 : First order theories, Examples of First Order Theories

May 16 : Pred. logic application 1: SMT lib

               Pred. logic application 2: Concolic testing

May 21 :  Predicate logic - semantic tableau (1/2)

May 28:    Predicate logic - natural deduction (1/2), Predicate logic - natural deduction (2/2),  

May *:  Predicate logic - semantic tableau (2/2),   Undecidability of Predicate Logic

May 30 : Temporal logic (1/2),Temporal logic (2/2)

June 4 :  Temporal logic application: model checking

               Temporal logic for concurrent system req. spec.,  NuSMV 

June 11 :   Temporal logic - branching time logic (1/2)

               :Temporal logic - branching time logic (2/2)  

June 13 :, Temporal logic - LTL, CTL, and CTL*

 

Homeworks

  • HW1: due Apr 11th 23:59
  • HW2: due Apr 25th 23:59
  • HW3: due May 2nd 23:59
  • HW4: due May 23rd 23:59
  • HW5: due June 6th 23:59 (hw5.pptx)
  • HW6: due June 21st 23:59 

Resources

Document Actions