CS228M: Logic for Computer Science
(Spring 2026)

Announcements

We will be using Piazza for all discussions in this course. If you have registered for the course but have not received a welcome mail from Piazza for CS228M after the first week of classes, please signup here.

Regular tutorials on every alternate Wed, from 8:30-10pm in CC 103.

End-semester exam on Mon, Apr 27, 5:30-8:30pm in LH 101. Please report to the exam hall 15 mins before the exam starts. Please be seated exactly according to this seating arrangement.

End-semester exam is open book and notes (printed, photo-copied, or hand-written). However, no electronic deviced like laptops, tablets, mobile phones or smart watches are allowed.

Teaching Staff

Instructor	Supratik Chakraborty
Friendly TAs	Rahul Kapur, Dhvanil Gheewala, Aryan Katiyar, Ishita, Vedant Saini, Ansh Garg

Hours

What	When	Where
Lectures	Wed 9:30-10:55, Fri 9:30-10:55	KR 225, Kanwal Rekhi Building
Office hour	Thu 17:00-18:00 (by email appointment)	CC 314, Computing Complex
Tutorials (optional)	Every alternate Wed, 8.30-10pm	CC 103, Computing Complex
Pre-scheduled Quizes	Fri Jan 30, 8.30-9.30 am Fri Mar 13, 8.30-9.30 am Fri Apr 10, 8:30-9:30 am	CC 101, CC 103, CC 105, Computing Complex

Grading

Midterm	35%
Endterm	35%
Pre-scheduled Quizes	18%
Surprise Quizes (best 4)	12%

Ground Rules

All quizes and exams are open book and notes.
Surprise quizes are just that -- there will be no prior intimation of these. However, there will be many such quizes, all with equal weightage, and we will take the best 4 of your scores for this component of the evaluation.
The instructor reserves the right to admit students coming late to class.
Practice problem sheets will be given at regular intervals. It is in your interest to solve these problems on your own.
Mutual discussion on practice problems is encouraged. However, copying solutions from others in quizes and exams will be severely penalized. To understand the distinction between "copying" and "discussion", please read this.
There is zero tolerance for dishonest means like copying solutions from others.
Anybody found indulging in such activities during graded classworks/quizes and exams will be summarily referred to the Department Academic Disciplinary ActionCommittee (DADAC).
There will be no second chances as far as penalty for dishonest means goes: you will be referred to DADAC the first time you are caught indulging in dishonest and unethical activities.

Textbook

Logic in Computer Science: Modeling and Reasoning about Systems by Michael Huth and Mark Ryan, Cambridge University Press.

Online resources

A cool online tool for trying out natural deduction proofs in propositional logic.

Problems for solving

Quiz and exam problems (solutions discussed in class)

Exam/Quiz date	Question paper
Jan 14, 2026	Surprise Quiz 1
Jan 30, 2026	Quiz 1
Feb 18, 2026	Surprise Quiz 2
Feb 25, 2026	Midsem Exam
Mar 13, 2026	Quiz 2
Apr 8, 2026	Surprise Quiz 3
Apr 10, 2026	Quiz 3
Apr 15, 2026	Surprise Quiz 4

Practice Problems

Date of posting	Problem set
Jan 21, 2026	Tutorial 1 Problems (solutions discussed in tutorial)
Jan 24, 2026	Practice Problem Set 1, Sample solutions
Jan 28, 2026	Tutorial 2 Problems (solutions discussed in tutorial)
Feb 2, 2026	Practice Problem Set 2, Sample solutions
Feb 6, 2026	Tutorial 3 Problems (solutions discussed in tutorial)
Feb 18, 2026	Practice Problem Set 3, Solutions
Mar 11, 2026	Tutorial 4 Problems (solutions discussed in tutorial)
Mar 15, 2026	Practice Problem Set 4, Solutions
Mar 25, 2026	Tutorial 5 Problems (solutions discussed in tutorial)
Apr 6, 2026	Practice Problem Set 5, Solutions
Apr 8, 2026	Tutorial 6 Problems (solutions discussed in tutorial)

Lecture Schedule

Date	Topics	Readings, slides, etc.
Jan 7	Introduction, course logistics, motivation for studying logic; introduction to propositional logic: syntax and semantics	Motivation slides Huth and Ryan: Sec 1.3
Jan 9	Delving deeper into semantics of propositional logic: truth tables and their impracticality, notions of (un)satisfiabiliy, validity, semantic entailment, semantic equivalence and equisatisfiability;	Slides Huth and Ryan: Sec 1.3, 1.4.1
Jan 14	Introduction to Natural Deduction (ND) proof rules: rules without assumptions; soundness of rules and simple applications; syntactic entailment and its relation to semantic entailment	Huth and Ryan: Sec 1.2.1
Jan 14 Compensation lecture	More ND proof rules: rules with assumptions and their usage: soundness and simple applications	Huth and Ryan: Sec 1.2.1
Jan 16	Derived rules in ND; examples of use of ND proof rules for proving sequents (syntactic entailments); completeness of ND proof system -- mimicking truth tables using ND proofs	Online tool for ND proofs in propositional logic Huth and Ryan: Sec 1.2.2, 1.2.3, 1.2.4, 1.4.3, 1.4.4
Jan 23 Guest lecture	Normal forms in propositional logic: NNF, CNF, DNF; Tseitin (also Tseytin) encoding and examples; equisatisfiable formulas using Tseitin encoding; example of graph coloring encoded as CNF, and solution using SAT solver	Huth and Ryan: Sec 1.5.1, 1.5.2 Wiki page on Tseytin encoding, Prof. Ashutosh's slides: 1-15 from here, 3-5 from here
Jan 28	More on NNF, CNF, DNF; converting from one normal form to another; resolution proof system; soundness of resolution	Huth and Ryan: Sec 1.5.1, 1.5.2 A good reference chapter on resolution
Jan 30	Completeness of resolution, and illustration through examples; introduction to Horn formulas and an sketch of Horn-SAT solving	A good reference chapter on resolution Huth and Ryan: Sec 1.5.3
Feb 4 Guest lecture	Horn formulas; an efficient algorithm for checking satisfiabilty of Horn formulas	Huth and Ryan: Sec 1.5.3 Prof. Krishna's slides
Feb 11	DPLL algorithm for satisfiability (SAT) solving, unit propagation, pure literals, branching and chronological backtracking; illustrating run of the algorithm for satisfiable problem instances	Prof. Ashutosh Gupta's slides (1-15) Chapter from Handbook of Satisfiability
Feb 11 Compensation lecture	DPLL algorithm: run on unsatisfiable instances; conflict-driven clause learning (CDCL): conflicts, implication graphs, cuts, conflict clauses, non-chronological backtracking; illustrating run of algorithm with conflicts and clause learning	Prof. Ashutosh Gupta's slides here (17-29) Prof. Marijn Heule's slides here (1-12) Chapter from Handbook of Satisfiability
Feb 13	Illustrating effect of branching choices on performance of DPLL solver; VSIDS and other variable selection heuristics in CDCL	Prof. Ashutosh Gupta's slides here (13-14) Prof. Marijn Heule's slides here (20-24) Chapter from Handbook of Satisfiability
Feb 17	Smart data structures in SAT solvers; two watched literals scheme; Implication graphs and unique implication points in CDCL	Prof. Ashutosh Gupta's slides here (4-11) and here (29-32) Prof. Marijn Heule's slides here (13-18, 31) Chapter from Handbook of Satisfiability
Feb 20	First order logic: syntax and intuitive meaning of predicates, universal and existential quantifiers; illustration through examples	Huth and Ryan: Sec 2.1, 2.2.1 Slides (1-6)
Mar 4	First order logic: recap of syntax; terms and formulas; notion of free and bound variables: illustration through examples; substitution in first-order logic	Huth and Ryan: Sec 2.2.1, 2.2.2, 2.2.3, 2.2.4 Slides (7-10)
Mar 6	Vocabulary V and V-structures: illustration through examples; semantics of FOL and its dependence on structures and binding	Slides (11-13)
Mar 11	Formal semantics of first-order logic: illustration through examples; notions of semantic entailment, satisfiability, validity, consistency	Slides (14-17)
Mar 13	More on semantic relations in FOL, quantifier equivalences in FOL, scoping rules for quantifiers, renaming bound variables to enable application of scoping rules	Slides (17-19)
Mar 18	Natural deduction proof system for first-order logic; introduction and elimination rules for equality, universal and existential quantifiers; reasoning about soundness of above rules	Huth and Ryan: Sec 2.3
Mar 20	Illustrating application of natural deduction proof rules to prove sequents in first-order logic; soundness and completeness of natural deduction proof systems	Huth and Ryan: Sec 2.3
Mar 25	More practice on proving sequents in first-order logic using natural deduction; soundness, completeness and compactness of first-order logic; using compactness to show inexpressibility results	Huth and Ryan: Sec 2.3, 2.6 (excluding 2.6.1)
Mar 27	Additional examples on use of compactness theorem to show inexpressibility results in first-order logic. Guest lecture by R. Venkatesh on use of logic in industrial applications	Huth and Ryan: Sec 2.6 (excluding 2.6.1)
Apr 1	Alternative statement of compactness theorem; Lowenheim-Skolem theorem and applications; quantified equivalences and prenex normal forms for first-order logic	Huth and Ryan: Sec 2.6 (excluding 2.6.1) Slides (18-20)
Apr 8	Prenex normal forms; notion of Skolem functions; Skolemization and Skolem Normal Form	Slides by Valentin Goranko
Apr 10	More on Skolem normal form; Herbrand models; Godel-Herbrand-Skolem Theorem, Herbrand Theorem	Excellent slides from TU Munich
Apr 15	More on Herbrand Theorem, ground clauses of Skolem normal form formulas, and a glimpse of first-order logic resolution	Sec 8.1 and 8.2 of chapter by David Toman
Apr 17	Problem solving session: Prenex normal form, Skolem normal form, converting a formula with function symbols to an equisatisfiable one without function symbols, finding a formula all of whose models are necessarily infinite	(Problems solved in class)

CS228M: Logic for Computer Science (Spring 2026)