CS402 Intro. to Logic, Spring 2012
- No class on Feb 8th (due to Korea Conference on Sofware Engineering (KCSE) 2012).
- Mid-term exam on March 27 (Tues) 9:00 - 11:00 AM
- We have a class on April 17, but no class on April 19 (due to IEEE Intl. Conf. on Software Testing, Verification and Validation (ICST)).
- Make-up class on May 2nd (Wed) 8:00 PM
- HW#5 deadline is delayed to May 29th (Tue) 11:59 PM.
- Final exam: May 22nd 9:00 - 12:00 AM
- Instructor: Moonzoo Kim
Office: 2434 (located at the east wing)
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.
- 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.
- Main text:
- "Mathematical Logic for Computer Science" by M.Ben-Ari, Springer, 2nd Edition
- "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
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?
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 17: Pred. logic application 1: SMT lib
Pred. logic application 2: Concolic testing
- May 2: Undecidability of Predicate Logic
- 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*
- 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
- SAT competition 2007 (look at input format section)
- 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