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.
- Coursework: 30%
- Midterm Exam: 30%
- Final Exam: 30%
- Class Participation: 10%
- 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.
- Jeongju Sohn
- email: firstname.lastname@example.org
- Office Hour: N1 401 Tuseday 18:30 ~ 20:00, Thursday 16:00 ~ 17:30.
From 10th March onwards, the lectures will be in Room 401 at E11.
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)
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