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

CS402 Intro. to Logic, Spring 12

Announcement

Administrative Information

Office: 2434 (located at the east wing)

Phone:042-350-3543

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

Office hour: 3:00-4:30 Mon, 10:30 - 12:00 Tues

  • Teaching assistants:   Shin Hong and YoungJoo Kim
  • Lecture room:  Rm#3445 (a.k.a. Lecture room #6)
  • 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

- Feb 7: Administrative Introduction

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

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

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

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

- Feb 28:  Propositional logic - semantics (3/3)

- Mar 6: Propositional normal forms

- Mar 8: Prop. logic application 1: How to solve Sudoku?

- Mar 13: Prop. logic application 2: How to Test/Verify my C program?

- Mar 15: Propositional logic - deductive systems (natural deduction),

Propositional logic -deductive Systems (Gentzen system g)

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

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

Wk 8: Midterm exam

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

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

- Apr 10: Predicate logic - semantics (3/3),

- Apr 12: First order theories, Examples of First Order Theories

- Apr 17: Pred. logic application 1: SMT lib

Pred. logic application 2: Concolic testing

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

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

- May 2: Undecidability of Predicate Logic

- May 3: Temporal logic (1/2),Temporal logic (2/2)

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

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

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

- May 15:, Temporal logic - LTL, CTL, and CTL*

 

Homeworks

  • HW#1 : due Mar 15 23:59
  • HW#2: due Mar 27 23:59
  • HW#3: due April 19 23:59
  • HW#4: due May 6 23:59
  • HW#5: due May 29 23:59

Resources

Document Actions