CS 228 : Logic for computer science 2021
Instructors : Ashutosh Gupta and
S. Krishna
Timings : 8:30 Monday, 9:30 Tuesday, 10:35 Thursday (Slot 1)
Venue : MSTeams, To join the course team, use team code: cfgfg9h
TAs :
For non gmail email addresses Append "iitb.ac.in" in the text inside the parenthesis
Optional tutorials :
Source material
- 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
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.
- On Friday 4:00, TAs will do a tutorial on a given set of problems.
- On SAFE app students have to do a quiz. 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
2021-01-07 : Lecture 1 - Introduction
2021-01-11 : Lecture 2 - Propositional logic (PL), syntax
2021-01-12 : Lecture 3 - Semantics and Truth tables
Age of mathematics: formal proofs
2021-01-16 (Saturday) : Lecture 4 - Formal proofs
2021-01-18 : Lecture 5 - Formal proofs 2
Age of computer science: resolution proof system
2021-01-19 : Lecture 6 - Substitutions and equivalences
2021-01-21 : Lecture 7 - Conjunctive normal forms
2021-01-25 : Lecture 8 - Low complexity SAT
2021-01-28 : Lecture 9 - Resolution
2021-01-30T10:30 (Saturday) : Quiz 1
- Quiz is postponed to 21-02-06T10:30
2021-02-01 : Lecture 10 - Resolution completeness
Age of hacker : SAT solvers
2021-02-02 : Lecture 11 - SAT solvers
2021-02-04 : Lecture 12 - SAT encoding
2021-02-08 : 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
- Video:
13.1 Z3,
- Practice tutorial problems (ungraded): problems.tar contains three problems: at-most-one, sudoku, and graph-color solutions
- Suggested reading : A tutorial on z3py
- Assignment 1: solve problems 12.21 and 12.22
- We will test your code using harness code similar to the following.
- If your code will not work with the above harness, you will not get marks
- Deadline: 2020-02-21
Age of mathematics: First-Order Logic (FOL)
2021-02-09 : Lecture 14 - First-order logic
2021-02-11 : Lecture 15 - Understanding FOL
2021-02-15 : Lecture 16 - Formal proofs
Age of computer science: First-Order Logic (FOL)
2021-02-16 : Lecture 17 - First-order logic conjunctive normal form (FOL CNF)
- Steps of CNF conversion: 17.1 rename apart, 17.2 negation normal form(NNF)
- 17.3 prenex form, 17.4 skolemization, 17.5 clausification, 17.6 quantifier drop
- slides
-
Video:
17.0 CNF overview ,
17.1-3 Rename,NNF,Prenex ,
17.4-6 Skolem,Clauses,Quantifier drop,
- Tutorial problems: 17.10 and 17.12
2021-02-18 : Lecture 18 - Unification
2018-02-24 : Midterm week
- Solution of some midterm problems are added in slides
- Problem 2: Lecture 6, Exercise 6.14
- Problem 4: Lecture 16, Example 16.12
- Problem 5: Lecture 18, Exercise 18.9
- Problem 6: Lecture 10, Exercise 10.8
- Problem 7: Lecture 16, Exercise 16.15
- We will not give solution of problem 8.
2021-03-04 : Lecture 19 - FOL Resolution
2021-03-08 Handover to Krishna