Personal tools
You are here: Home › Courses › CS402 Intro. to Logic, Fall 07

CS402 Intro. to Logic, Fall 07

Announcement

  1. Academic honesty should be highly honored.   Dishonest activities such as plagiarism in your HW or cheating in quiz/exam will be handled with severe penalty.
  2. Late HW is accepted with 20% penalty in 1 day, 40% penalty in 3 days.  HW will not be accepted after that. 
  3. Errata for the textbook
  4. Final exam: Dec 19th 11:00 AM - 1:00 PM
  5. No class on Dec 14th

Administrative Information

Office: 2434 (located at the east wing)

Phone:042-869-3543

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

Office hour: Mon, Wed 5:30 - 7:00 PM

(reservation e-mail would be preferred)

  • Teaching assistants: Shin Hong and Yunho Kim

Office: 2438 (located at the east wing)

E-mail: hongshin@gmail.com, kimyunho@kaist.ac.kr

Phone: 042-869-3583

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:  2112 (2nd lecture room)
  • Lecture hours: 11:00-12:00 Mon/Wed/Fri
  • Grading: attendance & quiz: 20%, HW: 30%, midterm exam.: 25 %,final exam.: 25 %  
  • 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:
    •  "Mathematical Logic for Computer Science" by M.Ben-Ari, Springer, 2nd Edition
      • Ch 1-3, 5
    • "Logic in Computer Science" by M.Huth and M.Ryan, Cambridge university press, 2nd edition
      • Ch 2-3
  • 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

- Sep 3rd: Administrative Introduction

- Sep 5th:  “Intro. to logic (1/2)”

- Sep 7th:  “Intro. to logic (2/2)”

- Sep 10th: Propositional logic - semantics (1/3)

- Sep 12th: Propositional logic - semantics (2/3)

- Sep 14th: Propositional logic - semantics (3/3)

- Sep 17th: A SAT solver-based model checking a C program

                 : Propositional normal forms

- Sep 29th, Oct 1st: Propositional logic -deductive Systems (1/3)

- Oct 3rd, Oct 8th: Propositional logic -deductive Systems (2/3)

- Oct 12th: Propositional logic - natural deduction

- Oct 15th: Propositional logic- soundness and completeness of H

- Oct 17th: Propositional logic - resolution (1/2)

Wk 8: Midterm exam

- Oct 29th,31st: Predicate logic - semantics (1/3)

- Nov 5th: Predicate logic - semantics (2/3)

- Nov 7th: Predicate logic - semantics (3/3)

- Nov 9th: Predicate logic - semantic tableau (1/2)

- Nov 12nd: Predicate logic - semantic tableau (2/2)

- Nov 16th,19th: Predicate logic - undecidability

- Nov 21th: Predicate logic - natural deduction (1/2)

- Nov 23rd: Predicate logic - natural deduction (2/2)

- Nov 26th: Temporal logic (1/2)

- Nov 28th: Temporal logic (2/2)

- Nov 30th: Temporal logic- model checking

-Dec 3rd: Temporal logic -NuSMV example

-Dec 5th: Temporal logic - alternating bit protocol

-Dec 7th: Temporal logic - branching time logic (1/2)

-Dec 10th: Temporal logic - branching time logic (2/2)

-Dec 12th: Temporal logic - LTL, CTL, and CTL*

Resources

Document Actions