# 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 :

TBA

## 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 computer science: resolution proof system

#### 2021-01-30T10:30 (Saturday) : Quiz 1

• Quiz is postponed to 21-02-06T10:30

### Age of hacker : SAT solvers

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

### Age of computer science: First-Order Logic (FOL)

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