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

CS402 Intro. to Logic, Spring 2011

Announcement

1. Class starts on Feb 8

2. No class on Feb 10 due to KCSE conf.

3. No class on Mar 1 (natl. holiday)

4. Mid term exam on Mar 29 9:00-11:59 AM (Tues) (closed book)

5. No class on Apr 12 (due to the KAIST policy for the recent tragedy)

6. Quiz on May 3rd (LTL semantics)

7. HW#4 due is extended to May 5th 23:59

8. No class on May 10 (natl. holiday)

9. Students interested in URP on software verification are welcome!

10. Final exam: May 31 (Tues) 7-10 PM

11. Please, evaluate the CS402 class in this semester before/on May 20.

Administrative Information

Office: 2434 (located at the east wing)

Phone:042-350-3543

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

Office hour: TBD 

(reservation e-mail would be preferred)

  • Teaching assistants: Shin Hong and Hak Yeol Choi

Office: 2438 (located at the east wing)

E-mail: hongshin@gmail.com ,  krhhyhy@gmail.com

Phone: 042-350-7743

Office hour:  Tues, 7:00 - 10:00 PM @ 1st floor PC room (a.k.a eve room)

(reservation e-mail would be preferred)

  • Lecture room:  3444 (5th lecture room)
  • Lecture hours: 9:00-10:30 Tues/Thur
  • Grading: attendance & quiz: 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. 
  • 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.
  • 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

- Feb 8: Administrative Introduction

- Feb 15:  “Intro. to logic (1/2)”

- Feb 17:  “Intro. to logic (2/2)”

- Feb 22: Propositional logic - semantics (1/3)

- Feb 24: Propositional logic - semantics (2/3)

- Sep 14th:  Propositional normal forms

- Mar 3: Prop. logic application: A SAT solver-based model checking a C program

- Mar 8: Propositional logic - semantics (3/3)

- Mar 10: Propositional logic - deductive systems (natural deduction)

- Mar 15: Propositional logic -deductive Systems (Gentzen system g)

- Mar 17: Propositional logic -deductive Systems (Hilbert system H))

- Mar 22: Propositional logic- soundness and completeness of H

- Mar 24: Predicate logic - semantics (1/3)

Wk 8: Midterm exam

- Apr 5: : Predicate logic - semantics (2/3),: Predicate logic - semantics (3/3)

Practical application: SMT solver and Concolic testing

-Apr 7:  Examples of First Order Theories, SMT lib

- Apr 11: Concolic testing, CREST manual

- Apr 14: Predicate logic - semantic tableau (1/2)

- Apr 19: Predicate logic - semantic tableau (2/2)

- Apr 21:Predicate logic - undecidability  

              Predicate logic - natural deduction (1/2) 

- Apr 26: Predicate logic - natural deduction (2/2)

- Apr 28: Temporal logic (1/2),Temporal logic (2/2)

- May 3:  Temporal logic- model checking,  Temporal logic -NuSMV example

- May 12: Temporal logic - alternating bit protocol,

- May 17: Temporal logic - branching time logic (1/2),Temporal logic - branching time logic (2/2)  

- May 19:, Temporal logic - LTL, CTL, and CTL*, LTL model checking algorithm basics

Homeworks

  1. HW#1: Due Mar 22 23:59
  2. HW#2: Due Apr 5 23:59
  3. HW#3: Due Apr 19 23:59
  4. HW#4: Due May 5 23:59
  5. HW#5: Due May 31 23:59

Resources

Document Actions