## CS402 Introduction to Logic for Computer Science (Spring 2016)

### Syllabus

This course is about basics of logic used in computer programming. Topics covered in this course are: propositional calculus, predicate calculus, axiomatic theories, skolemization, unification, and resolution. 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%

### Schedule

- There won’t be any lectures on 12th and 14th April, due to ICST 2016.
- There won’t be any lecture on 12th May, due to another lecture in Software Graduate Program.
- I will schedule make-up lectures after consulting the entire class as we move forward.

### Teaching Assistant

- Jeongju Sohn
- email: kasio555@kaist.ac.kr
- Office Hour: N1 401 Tuseday 18:30 ~ 20:00, Thursday 16:00 ~ 17:30.

**NEW LOCATION**

From 10th March onwards, the lectures will be in **Room 401 at E11**.

### References

The following books have chapters corresponding to the lecture material. It is not necessary to buy the books, but you can consult them to get the bigger picture.

- “Mathematical Logic for Computer Science” by M.Ben-Ari, Springer (Chapter 1-3, 5)
- “Logic in Computer Science” by M.Huth and M.Ryan, Cambridge university press (Chapter 2-3)

### Lectures

The following schedule is *tentative* and will be adjusted as the class progresses.

- 03 March: Administrative Introduction
- 08 March: Introduction to Logic
- Beautifying Gödel by Eric C. R. Hehner

- 10 March: Propositional Logic - Semantics Part 1
- 15 March: Propositional Logic - Semantics Part 2
- 17 March: Propositional Logic - Semantics Part 3
- 22 March: Propositional Logic - Normal Forms
- 24 March: MiniSAT and SAT Encoding
- 29 March: Propositional Logic - Deductive Proofs and Natural Deduction Part 1
- 31 March: Propositional Logic - Deductive Proofs and Natural Deduction Part 2
- 05 April: Propositional Logic - Gentzen System
- 07 April: Propositional Logic - Hilbert System
- 12 April: No Lecture (ICST 2016)
- 14 April: No Lecture (ICST 2016)
- 19 April: Soundness and Completeness of Hilbert System
**26 April: Midterm Exam**- 28 April: Predicate Logic - Semantics Part 1
- 03 May: Predicate Logic - Semantics Part 2
- 05 May: No lecture (National Holiday)
- 10 May: Looking back at the SAT encoding of Nonogram solver submissions
- 11 May: Applications of Logic in Software Engineering -
**Make-up lecture, from 18:00 to 20:00, E-11 402** - 12 May: No Lecture (SGP Commitment)
- 17 May: First Order Theories
- 19 May: Predicate Logic - Semantic Tableau
- 24 May: Predicate Logic - Natural Deduction
- 26 May: No Lecture (Admission Interview Commitment)
- 31 May: Predicate Logic - Undecidability
- 02 June: Temporal Logic - Semantics and Tableux Part 1
- 07 June: Temporal Logic - Semantics and Tableux Part 2
- 09 June: Linear Temporal Logic - Deductive System
- 14 June: Linear Temporal Logic - Completeness and Soundness
**21 June: Final Exam: E-11 Room 304, 1pm - 3pm**

### Coursework

- Coursework 1: The Warming Up Due on 8th March, 13:00 (submit at the beginning of the lecture)
- Coursework 2: Normal Forms, Validity, and Satisfiability Due on 7th April, 18:00 (submit through KLMS)
- Coursework 3: SMT Solver & Basic Program Verification Due on 7th June, 18:00 (submit through KLMS)