**Instructors** : Ashutosh Gupta and
S. Krishna

**Timings** : 9:30 Monday, 10:30 Tuesday, 11:35 Thursday (Slot 2)

**Venue** : LH 102, (discussions on Piazza)

**TAs** : TBA

For non gmail email addresses Append "iitb.ac.in" in the text inside the parenthesis

**Optional tutorials** :

- TBA

- 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. 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.

- TAs will do a tutorial on a given set of problems at their chosen slot. Please discuss with your TA.

- Attendance quiz: 5% (half marks for attempt and half marks for 3+ options correct)
- Quizzes : 22.5% (3 quizzes)
- Programming : 7.5% (1 assignment)
- Midterm : 25% (2 hours)
- Final : 40% (3 hours)

May change later.

- 2.1Variables, Connectives, 2.2 Puzzle modeling, 2.3 Parsing, 2.4 Subformulas and substitutions, 2.5 Shorthands,
- slides
- Tutorial problems: 2.6 and 2.7

- 3.1 Semantics, 3.2 satisfiability problem, 3.3 truth table, 3.4 expressive power
- slides
- Tutorial problems: 3.10, 3.15(for next week), 3.23, and 3.28

- 4.1 formal proofs derivations, 4.2 more proof rules, and 4.3 soundness of proof system
- slides
- Tutorial problems: 4.3 and 4.4.1

- 5.1-2 derived rules, 5.3 substitutions in formal proofs
- slides
- Tutorial problems: 5.4

- 6.1 Substitution theorem, 6.2 equivalences, 6.3 negation normal form(NNF)
- slides
- Tutorial problems: 6.13 and 6.16

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

- 8.1 Completeness, 8.2 compactness
- slides
- Tutorial problems: 8.3(at slide 12) and 8.8

- 10.1 k-SAT and 3-SAT, 10.2 2-SAT
- slides
- Tutorial problems: 10.8 and 10.10

- DPLL and CDCL
- slides
- Tutorial problems: 11.8 and 11.9

- Syllabus: everything that is covered in lectures before the quiz.
- You may have a sheet of paper with the rules of the formal proof system.
- You may also include the eight derived rules from lecture 5.
- Write only on single side. We will collect the sheet at the end.
- Nothing else should be on your sheet.
- Bring your student id.

- 12.1 encoding hard problems, 12.2 Cardinality constraints, 12.3 encoding more problems
- slides
- Tutorial problems: 12.09 and 12.11

- 13.1 Z3, 13.2 Using Python interface of Z3, 13.3 SMT2 file format
- Encoding simple problems into satisfiability problems
- slides
- Code from class
- Tutorial problems: 13.07 and 13.08
- Suggested reading : A tutorial on z3py

- Assignment 1: Please find the problem description in sat-assignment.zip
- Deadline: 2020-03-01

- 14.1 Syntax, functions, predicates, terms, atoms, formulas
- 14.2 Models and assignments
- slides
- Tutorial problems: 14.6 and 14.11-12

- 15.1 sentences, closed terms, bounded and free variables
- 15.2 Examples and limits of FOL, 15.3 Substitututions
- slides
- Tutorial problems: 15.8-9 (page 15) and 15.12

- 16.1 Formal rules for the quantifiers,16.2 Introduction rules for quantifiers
- 16.3 Elimination rules for forall
- slides
- Tutorial problems: 16.6 and 16.8

- 17.1 Elimination rules for forall, 17.2 Rules for equality
- slides
- Tutorial problems: 17.4 and 17.5

- Steps of CNF conversion: 18.1 rename apart, 18.2 negation normal form(NNF)
- 18.3 prenex form, 18.4 skolemization, 18.5 clausification, 18.6 quantifier drop
- slides
- Tutorial problems: 18.10 and 18.11

- 19.1 Why unification? 19.2 Unification
- 19.3 Robinson algorithm
- slides
- Tutorial problems: 19.6-8

- 20.1 Refutation proof system 20.2 Adapting resolution for FOL
- 20.3 Resolution proof system for FOL
- slides
- Tutorial problems: 20.2 and 20.3

- Syllabus: everything that is covered in lectures before the midsem.
- You may have an A4 sheet of paper with any text.
- Write only on single side. We will collect the sheet at the end.
- Bring your student id.