## Logic for Computer Science (CS 228), July 2018

Time
T3, Monday 11.30am - 1.00pm
T1, Tuesday 10.30am - 11.30am
T1, Wednesday 2.00pm - 3.30pm
Textbook
[HR] Logic in Computer Science by Huth and Ryan.
[Sm] Mathematical Logic by R. M. Smullyan
Reference books
Logic for Computer Scientists by Uwe Schoning
A mathematical introduction to Logic by Enderton
[BM] The calculus of computation by Bradley and Manna
Mathematical Logic for Computer Science by Ben-Ari
Artificial Intelligence by Russell and Norvig
Assignment 1 (15%), Midsem (30%), Assignment 2 (15%), Endsem (40%)
[LN] Lecture Notes [PDF ]
Video Lectures
Video Help
[Kos] Strongly connected graph component: Kosaraju's algorithm
[Asp] 2-CNF satisfiability algorithm: Aspvall et al.
[Erik] NP-hardness of SAT, 3-SAT: MIT courseware
Assignments
1. Lecture room scheduling [PDF ]
2. Keen puzzle solution [PDF ]
Course Contents
# Date Contents Source
1 30 July, Mon Introduction, Motivation and History of Logic
2 1 Aug, Wed Propositional Logic, truth table, semantic entailment HR 1.1, LN 2.1 - 2.5, Sm 5
3 6 Aug, Mon (1.5hr) Encoding problems using Propositional logic LN 2.5
4 7 Aug, Tue Natural Deduction HR 1.2, LN 3.1
5 8 Aug, Wed Natural Deduction continued..
6 13 Aug, Mon (1.5hr) Natural Deduction continued. Exercises.
7 14 Aug, Tue Mathematical Induction. Soundness theorem. HR 1.4, LN 1.1, LN 3.3
8 20 Aug, Mon Tutorial (conducted by Prince) [PDF ]
9 21 Aug, Tue Introduction to Z3 (by Prince) Z3 in browser , Tutorial
10 24 Aug, Fri Completeness Theorem HR 1.4, LN 3.4
11 27 Aug, Mon (1.5hr) SAT, CNF, 3-CNF, NP-completness of 3-CNF HR 1.5, LN 4.1-4.2, see [Eric]
12 28 Aug, Tue Linear Time algorithm: 2-CNF satisfiability LN 4.3, see [Asp]
13 29 Aug, Wed (1.5hr) 2-CNF SAT, Horn Clause satisfiability HR 1.5, LN 4.4
14 3 Sep, Mon (1.5hr) DPLL algorithm LN 4.5
15 4 Sep, Tue (1hr) DPLL continued with examples
16 5 Sep, Wed (1.5hr) Revision of Propositional Logic
17 15 Sep, Sat Mid Sem [PDF ]
18 17 Sep, Mon Introduction to First order logic LN 5.1, HR 2.1
19 18 Sep, Tue First order logic: Terms and Formulas LN 5.2, HR 2.2
20 19 Sep, Wed Semantics of first order: Models HR 2.4
21 24 Sep, Mon Natural deduction for first order HR 2.3
22 25 Sep, Tue Soundness, Completeness and Compactness of FO HR 2.4
23 26 Sep, Wed Tutorial (conducted by Prince) [PDF ]
24 1 Oct, Mon Tutorial (conducted by Prince)
25 8 Oct, Mon Program Verification: Introduction HR 4.1, 4.2
26 9 Oct, Tue Hoare triples HR 4.2
27 10 Oct, Wed Partial Correctness: Factorial example HR 4.3
28 22 Oct, Mon Partial Correctness: Minimum Sum-section example HR 4.4
29 23 Oct, Tue Total Correctness HR 4.5
30 24 Oct, Wed First order theory LN 7.1, BM 3.1
31 29 Oct, Mon Theory of Equality, Peano arithmetic LN 7.2, BM 3.2/3.3
32 30 Oct, Tue Presburger arithmetic, Theory of Reals BM 3.3
33 31 Oct, Wed Mid-Sem paper review
34 5 Nov, Mon Theory of Arrays BM 3.4
35 6 Nov, Tue Course Summary
36 12 Nov, Mon Review of assignment 1