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
Grading Scheme
Assignment 1 (15%), Midsem (30%), Assignment 2 (15%), Endsem (40%)
[LN] Lecture Notes [PDF ]
Video Lectures
1. NPTEL Video by Prof. S Arun Kumar: click here
2. Video lecture by Prof. Shai Ben-David: click here
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