CS 228 : Logic for computer science 2023
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 :
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. 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
- TAs will do a tutorial on a given set of problems at their chosen slot. Please discuss with your TA.
Evaluation structure
- 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.
Attendance Quiz URL
Lectures
Age of philosophy: propositional logic
2023-01-02 : Lecture 1 - Introduction
2023-01-03 : 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
- Tutorial problems: 2.6 and 2.7
2023-01-05 : Lecture 3 - Semantics and Truth tables
- 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
Age of mathematics: formal proofs
2023-01-09 : Lecture 4 - Formal proofs
- 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
2023-01-10 : Lecture 5 - Formal proofs 2
- 5.1-2 derived rules, 5.3 substitutions in formal proofs
- slides
- Tutorial problems: 5.4
Age of computer science: resolution proof system
2023-01-12 : Lecture 6 - Substitutions and equivalences
- 6.1 Substitution theorem, 6.2 equivalences, 6.3 negation normal form(NNF)
- slides
- Tutorial problems: 6.13 and 6.16
2023-01-16 : Lecture 7 - Conjunctive normal forms
- 7.1 conjunctive normal forms,7.2 Tseitin's encoding
- 7.3 Resolution
- slides
- Tutorial problems: 7.12 and 7.20
2023-01-17/19 : Lecture 8/9 - Resolution completeness
- 8.1 Completeness, 8.2 compactness
- slides
- Tutorial problems: 8.3(at slide 12) and 8.8
2023-01-23 : Lecture 10 - Low complexity SAT
- 10.1 k-SAT and 3-SAT, 10.2 2-SAT
- slides
- Tutorial problems: 10.8 and 10.10
Age of hacker : SAT solvers
2023-01-24 : Lecture 11 - SAT solvers
- DPLL and CDCL
- slides
- Tutorial problems: 11.8 and 11.9
2023-01-25T08:30 (Wednesday) : Quiz 1
- 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.
2023-01-30 : Lecture 12 - SAT encoding
- 12.1 encoding hard problems, 12.2 Cardinality constraints, 12.3 encoding more problems
- slides
- Tutorial problems: 12.09 and 12.11
2023-01-31 : Lecture 13 - Encoding problems into SAT solver
- 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
2023-02-02 : Assignment 1
- Assignment 1: Please find the problem description in sat-assignment.zip
- Deadline: 2020-03-01
Back to Age of mathematics: First-Order Logic (FOL)
2023-01-02 : Lecture 14 - First-order logic
- 14.1 Syntax, functions, predicates, terms, atoms, formulas
- 14.2 Models and assignments
- slides
- Tutorial problems: 14.6 and 14.11-12
2023-02-06 : Lecture 15 - Understanding FOL
- 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
2023-02-07 : Lecture 16 - Formal proofs
- 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
2023-02-09 : Lecture 17 - Formal proofs : Equality
- 17.1 Elimination rules for forall, 17.2 Rules for equality
- slides
- Tutorial problems: 17.4 and 17.5
Return to age of computer science: First-Order Logic (FOL)
2023-02-13 : Lecture 18 - First-order logic conjunctive normal form (FOL CNF)
- 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
2023-02-14 : Lecture 19 - Unification
- 19.1 Why unification? 19.2 Unification
- 19.3 Robinson algorithm
- slides
- Tutorial problems: 19.6-8
2023-02-16 : Lecture 20 - FOL Resolution
- 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
2023-02-20 : Midterm week
- 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.
2023-02-20 Handover to Krishna