CS402 Introduction to Logic for Computer Science (Spring 2017)
Lecturer
Shin Yoo shin.yoo@kaist.ac.kr
Syllabus
This course is about basics of logic used in computer programming. Topics covered in this course are: propositional and predicate logic, as well as basic temporal logic. We will also try to incorporate practical application of logic systems using various tools.
Evaluation
- Coursework: 30%
- Midterm Exam: 30%
- Final Exam: 30%
- Class Participation: 10%
Teaching Assistant
- Seongmin Lee, Jeongju Sohn
- email: nim.gnoes.eel@gmail.com, kasio555@kaist.ac.kr
- Office Hour: Every wednesday 16:00 ~ 17:30, 18:30 ~ 20:00, N1 Room #403
References
The majority of the course follows the outline of Ben-Ari, but we will also use Huth and Ryan as the reference for natural deduction.
- “Mathematical Logic for Computer Science” by M.Ben-Ari, 3rd Edition, Springer
- “Logic in Computer Science” by M.Huth and M.Ryan, Cambridge university press (Chapter 2-3)
Lectures
- 28 Feb: Administrative Introduction
- 02 Mar: Introduction to Logic
- 07 Mar: Propositional Logic - Semantics Part 1
- 09 Mar: Propositional Logic - Semantics Part 2
- 14 Mar: No Lecture (ICST 2017)
- 16 Mar: No Lecture (ICST 2017)
- 21 Mar: Propositional Logic - Semantics Part 3
- 23 Mar: Propositional Logic - Normal Forms
- 28 Mar: MiniSAT and SAT Encoding, Coursework 2, Propositional Logic - Deductive Proofs and Natural Deduction Part 1
- 30 Mar: Propositional Logic - Deductive Proofs and Natural Deduction Part 2
- 04 Apr: Propositional Logic - Gentzen System
- 06 Apr: Propositional Logic - Hilbert System
- 11 Apr: Soundness and Completeness of Hilbert System
- 13 Apr: Predicate Logic - Semantics Part 1
- 18 Apr: Midterm Exam
- 25 Apr: Predicate Logic - Semantics Part 2
- 27 Apr: Applications of Logic in Software Engineering, Z3 Tutorial, Coursework 3
- 02 May: Predicate Logic - Semantic Tableaux
- 04 May:
- 09 May: No Lecture (Election Day)
- 11 May: Predicate Logic - Natural Deduction
- 16 May: Predicate Logic - Undecidability
- 18 May: Temporal Logic - Semantics and Tableux Part 1
- 23 May: No Lecture (ICSE 2017)
- 25 May: No Lecture (ICSE 2017)
- 30 May: Temporal Logic - Semantics and Tableux Part 2
- 01 Jun: Linear Temporal Logic - Deductive System
- 06 Jun: Memorial Day
- 08 Jun: Linear Temporal Logic - Completeness and Soundness
- 13 Jun: Final Exam
Coursework
- Coursework 1: The Warming Up, due 2nd March
- Coursework 2: CNF and Nonogram, due 11th April
- Coursework 3: SMT Solver, due 25th May. Use the public test cases to test your implementation.