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

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

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

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

May change later.

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

- 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

- 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

- 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

- 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

- 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

- 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

- 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

- 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

- 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 students if allowed by the institute.