# CS402 Intro. to Logic, Fall 07

**Announcement**

- 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.
- Late HW is accepted with 20% penalty in 1 day, 40% penalty in 3 days. HW will not be accepted after that.
**Errata for the textbook****Final exam: Dec 19th 11:00 AM - 1:00 PM****No class on Dec 14th**

**Administrative Information**

**Instructor**: Moonzoo Kim

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

- 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

- Wikipedia
- SAT competition 2007 (look at input format section)
- Minisat
- The Quest for Efficient Boolean Satisfiability Solvers
- Cygwin : a linux-like platform for Windows
- MikTek : the best typesetter for mathematical/logical formulas
- CBMC : A bound model checker based on SAT solver for C programs
- Table of mathematical symbols from Wikipedia
- NuSMV