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

**Timings** : 8:30 Monday, 9:30 Tuesday, 10:35 Thursday

**Venue** : CC103

**TAs** :
Riya Baviskar(170050011@),
Kalyani Dole (163050022@),
Tuppe Omkar Vijaykumar (omkarvtuppe@cse.),
Anuj Diwan (anujdiwan@cse.),
Aneesh Shetty(a3grand _at_ gmail.com),
Jatin Lamba (170050039.iitb _at_ gmail.com )

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

**Optional tutorials** :

- Tutorial 1 : 2020-01-27T19:00@CC103 (Monday)
- Tutorial 2 : 2020-02-10T19:00@CC103 (Monday)
- Tutorial 3 : 2020-02-21T20:30@CC103 (Friday)

- A First Course in Logic, An Introduction to Model Theory, Proof Theory, Computability, and Complexity
- SAT solvers: Handbook of Satisfiability (2009), chapter 4.1-4.4

- Attendance: 5%
- Quizzes : 30% (4 quizzes)
- Midterm : 25% (2 hours)
- Final : 40% (3 hours)

May change later.

Attendance URL

View status of attendance

- Variables, Connectives, Shorthands, Puzzle modeling
- slides
- Unique parsing slides

- Semantics, satisfiability problem, truth table, expressive power
- slides

- derivations, proof rules
- slides

- derived rules and soundness of proof system
- slides

- Substitution theorem, and equivalences
- slides

- Negation normal form, and conjunctive normal forms
- Tseitin's encoding, Disjunction normal forms
- slides

- k-SAT, 3-SAT, 2-SAT, XOR-SAT
- Horn clauses
- slides

- You may bring 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.

- Resolution proof system
- slides

- Completeness and compactness
- slides

- DPLL and CDCL
- slides

- Encoding hard problems, Encoding bounds,
- slides

- Timing: 5PM-8PM
- Venue: SL1 and SL2 (at second floor of CC)
- Z3 will be installed in the lab machines!
- You may install in your own laptop before coming to the lab!
- slides
- Lab problems
- Z3 API
- Z3 installation instructions Linux Windows

- Syntax, functions, predicates, terms, atoms, formulas
- sentences, closed terms, bounded and free variables
- slides

- Structures and assignments
- slides

- Examples and limits of FOL
- Substitututions and formal rules for the quantifiers
- slides

- Timing: 09:00-12:00
- Venue: SL1 and SL2

- Proof rules, derived rules, proving some properties of quantifiers
- slides

- Here is the source code of the attendance of the system
- If you can change your attendance by finding a flaw in the system, you will get the 5% of the attendance irrespective of your attendance.
- Ground rules: DO NOT TRY TO STEAL MY PASSWORD! Once you find a flaw, please report to me and do not share with others.