CS402 Introduction to Logic for Computer Science (Spring 2018)
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 (bohrok@kaist.ac.kr)
- Office hour: Room 401 at N1, Tuesday & Thursday, 2:00-4:30PM
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)
Lecture Schedule
I have three trips that I am already committed to in Spring 2018. I was invited to speak at the 58th CREST Open Workshop on 27th February. I am the Program Co-chair for ICST 2018, which takes place from 9th to 13th of April. Finally, I am attending the biggest software engineering conference, ICSE 2018, in the last week of May to present papers and conduct meetings. I will try my best to keep the disruptions to the minimum; there may be one or two guest lectures where appropriate.
The following schedule is tentative and we have have new topics for 2018. Stay tuned.
- 27 Feb: No Lecture (CREST Open Workshop)
- 01 Mar: No Lecture (Independence Day)
- 06 Mar: Introduction to Logic
- 08 Mar: Propositional Logic - Semantics Part 1, Part 2
- 13 Mar: Propositional Logic - Semantics Part 3
- 15 Mar: Propositional Logic - Normal Forms
- 20 Mar: MiniSAT and SAT Encoding + Coursework 1, Propositional Logic - Natural Deduction
- 22 Mar: Propositional Logic - Gentzen System
- 27 Mar: Propositional Logic - Hilbert System
- 29 Mar: Soundness and Completeness of Hilbert System
- 03 Apr: Propositional Logic - Resolution
- 05 Apr: Predicate Logic - Semantics Part 1
- 10 Apr: No Lecture (ICST 2018)
- 13 Apr: No Lecture (ICST 2018)
- 17 Apr: Midterm Exam
- 24 Apr: Predicate Logic - Semantics Part 2
- 26 Apr: Predicate Logic - Semantic Tableaux
- 01 May: Predicate Logic - Natural Deduction
- 03 May: Predicate Logic - Deductive systems
- 08 May: Predicate Logic - Normal Forms
- 10 May: Predicate Logic - Undecidability
- 15 May: Z3 Tutorial, Coursework 2
- Guide to Z3 Solver
- Example soot.sh script - this is an example: modify it to suit your OS/environment
- 17 May: Temporal Logic - Semantics and Tableux Part 1
- 22 May: No Lecture (Happy Birthday, Buddha!)
- 24 May: Temporal Logic - Semantics and Tableux Part 2
- 29 May: No Lecture (ICSE 2018)
- 31 May: Guest Lecture by Prof. Hongseok Yang - Datalog
- 05 Jun: Linear Temporal Logic - Deductive System
- 07 Jun: Linear Temporal Logic - Completeness and Soundness
- 12 Jun: Final Exam
Coursework
- Coursework 1: CNF and Nonogram
- Coursework 2: SMT Solver and Simple Program Verification Use the public test cases to test your implementation.