CS 228 : Logic for computer science 2022

Instructors : Ashutosh Gupta and S. Krishna

Timings : 8:30 Monday, 9:30 Tuesday, 10:35 Thursday (Slot 1)
Venue : Online, MSTeams, To join the course team, use team code: 26vzr4x
TAs :
For non gmail email addresses Append "iitb.ac.in" in the text inside the parenthesis
Optional tutorials :

TBA

Source material

• Text book: A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity - Shawn Hedman
• Logic in Computer Science: Modelling and Reasoning about Systems - Huth and Ryan
• SAT solvers: Handbook of Satisfiability (2009), chapter 4.1-4.4
• Course syllabus: Slides define the syllabus. Everything before the problem section in slides is in the syllabus. I may skip simple topics in the videos, where there is not much to explain. In terms of problems, you must solve tutorial problems. All the other problems are optional. Any new concept defined there is not part of the course. If the concept appears in the exam, we will redefine it in the question paper.
• We do not provide solutions of the problems that are not in the tutorials. We can discuss your approach with you. Some TAs may give you answer to some of the problems. It is their choice. However, they are not obligated to provide written detailed answer.

Interaction policy

• Every week videos will be released by Sunday night
• No sessions on Mondays
• On Thursday 10:30, the instructor will do an interactive session for clearing doubts. If requested, we can also do a meeting on Tuesday.
• TAs will do a tutorial on a given set of problems at their chosen slot. Please discuss with your TA.
• On SAFE app students have to do a quiz every week. The quiz will remain available from Friday evening to Sunday night.

Evaluation structure

• Weekly quizzes: 15%
• Quizzes : 22.5% (3 quizzes)
• Programming : 7.5% (1 assignment)
• Midterm : 20% (2 hours)
• Final : 35% (3 hours)

May change later.

Lectures

Age of philosophy: propositional logic

2022-01-03 : Lecture 1 - Introduction

• Ashutosh slides
• Video: 1.1 Why study logic?, 1.3 Course plan first half, Krishna: Intro to the second half.

2022-01-04 : Lecture 2 - Propositional logic (PL), syntax

• 2.1Variables, Connectives, 2.2 Puzzle modeling, 2.3 Parsing, 2.4 Subformulas and substitutions, 2.5 Shorthands,
• slides
• Video: 2.1 PL syntax, 2.2 Puzzle modling, 2.3 Parsing. 2.5 Shorthands.
• Tutorial problems: 2.6 and 2.7

2022-01-06 : Lecture 3 - Semantics and Truth tables

• 3.1 Semantics, 3.2 satisfiability problem, 3.3 truth table, 3.4 expressive power
• Video: 3.1 Semantics, 3.2-3 SAT problem and truth table, 3.4 expressive power.
• slides
• Tutorial problems: 3.13, 3.15, and 3.23

Age of mathematics: formal proofs

2022-01-10 : Lecture 4 - Formal proofs

• 4.1 formal proofs derivations, 4.2 more proof rules, and 4.3 soundness of proof system
• Video: 4.1 Formal proofs, 4.2 More rules , 4.3 Soundness.
• slides
• Tutorial problems: 4.3 and 4.4.1

2022-01-11 : Lecture 5 - Formal proofs 2

• 5.1-2 derived rules, 5.3 substitutions in formal proofs
• Video: 5.1 Derived rules, 5.2 More derived rules , 5.3 Substitutions in formal proofs.
• slides
• Tutorial problems: 5.4

Age of computer science: resolution proof system

2022-01-13 : Lecture 6 - Substitutions and equivalences

• 6.1 Substitution theorem, 6.2 equivalences(simple topic; no video), 6.3 negation normal form(NNF)
• slides
• Video: 6.1 Substitution theorems, 6.3 NNF,
• Tutorial problems: 6.13 and 6.16

2022-01-17 : Lecture 7 - Conjunctive normal forms

• 7.1 conjunctive normal forms,7.2 Tseitin's encoding
• 7.3 Resolution
• slides
• Video: 7.1 CNF, 7.2 Tseitin's encoding, 7.3 Resolution,
• Tutorial problems: 7.12 and 7.20

2022-01-18 : Lecture 8 - Resolution completeness

• 8.1 Completeness, 8.2 compactness
• slides
• Video: 8.1 Completeness, 8.2 Completeness, derivations, and implication, 8.3 Compactness ,
• Tutorial problems: 8.3(at slide 12) and 8.8

2022-01-20 : Lecture 09 - Low complexity SAT

• 9.1 k-SAT and 3-SAT, 9.2 2-SAT, 9.3 XOR-SAT
• 9.4 Horn clauses
• Video: 9.1 k-SAT, 9.2 2-SAT , 9.3-4 XOR SAT and Horn SAT
• slides
• Tutorial problems: 9.11 and 9.15

Age of hacker : SAT solvers

2022-01-24 : Lecture 10 - SAT solvers

• DPLL and CDCL
• slides
• Video: 10.1 DPLL, 10.2 Clause learning, 10.3 CDCL,
• Tutorial problems: 10.8 and 10.9

2022-01-25 : Lecture 11 - SAT encoding

• 11.1 encoding hard problems, 11.2 Cardinality constraints, 11.3 encoding more problems
• slides
• Video: 11.1 Encoding problems, 11.2 Cardinality constraints 11.3 Encoding more problems
• Tutorial problems: 11.11 and 11.12

2022-01-27 : Lecture 12 - Encoding problems into SAT solver

• 12.1 Z3, 12.2 Using Python interface of Z3, 12.3 SMT2 file format
• Encoding simple problems into satisfiability problems
• slides
• Video: 12.1 Z3,
• Practice tutorial problems (ungraded): problems.tar contains three problems: at-most-one, sudoku, and graph-color
• Suggested reading : A tutorial on z3py

2022-01-29T10:30 (Saturday) : Quiz 1

• Quiz is postponed to 2022-02-02T08:30
• You may have a sheet of paper with the rules of the formal proof system.
• You may also include the 8 derived rules from lecture 5.
• Nothing else should be on your sheet.
• Offline for on-campus and not quarantined students.
• Offline exam will also happen using SAFE. Only change is that you are physically present.
• Please ensure that your phone is charged during the quiz.

2022-02-02 : Assignment 1

• Assignment 1: Please find the problem description in rush-hour.tar
• If your code will not work with the above harness, you will not get marks
• Deadline: 2020-02-15

Back to Age of mathematics: First-Order Logic (FOL)

2022-01-31 : Lecture 13 - First-order logic

• 13.1 Syntax, functions, predicates, terms, atoms, formulas
• 13.2 Models and assignments
• slides
• Video: 13.1 FOL syntax, 13.2 FOL semantics,
• Tutorial problems: 13.4 and 13.6

2022-02-01 : Lecture 14 - Understanding FOL

• 14.1 sentences, closed terms, bounded and free variables
• 14.2 Examples and limits of FOL, 14.3 Substitututions
• slides
• Video: 14.1 more definitions, 14.2 unstanding semantics , 14.3 FOL substitutions ,
• Tutorial problems: 14.8-9 (page 14) and 14.12

2022-02-03 : Lecture 15 - Formal proofs

• 15.1 Formal rules for the quantifiers,15.2 Introduction rules for quantifiers
• 15.3 Elimination rules for quantifiers,15.4 Rules for equality
• slides
• Video: 15.1 formal proofs , 15.2 Intro rules, 15.3 Elim rules, 15.4 Equality rules,
• Tutorial problems: 15.12 and 15.15

Return to age of computer science: First-Order Logic (FOL)

2022-02-07 : Lecture 16 - First-order logic conjunctive normal form (FOL CNF)

• Steps of CNF conversion: 16.1 rename apart, 16.2 negation normal form(NNF)
• 16.3 prenex form, 16.4 skolemization, 16.5 clausification, 16.6 quantifier drop
• slides
• Video: 16.0 CNF overview , 16.1-3 Rename,NNF,Prenex , 16.4-6 Skolem,Clauses,Quantifier drop,
• Tutorial problems: 16.10 and 16.12

2022-02-08 : Lecture 17 - Unification

• 17.1 Why unification? 17.2 Unification
• 17.3 Robinson algorithm 17.4 Correctness of Robinson algorithm
• slides
• Video: 17.1 Why unification?, 17.2 Unification, 17.3 Robinson algorithm, 17.4 Correctness,
• Tutorial problems: 17.6-8

2022-02-10 : Lecture 18 - FOL Resolution

• 18.1 Refutation proof system 18.2 Adapting resolution for FOL
• 18.3 Resolution proof system for FOL
• slides
• Video: 18.1-2Adapting resolution , 18.3 Resolution proof system ,
• Tutorial problems: 18.2 and 18.3

2022-02-17 Handover to Krishna (one lecture before midterm)

2018-02-19 : Midterm week