**Instructor** : Ashutosh Gupta

**Timings** : Monday & Wednesday, 09:45-11:15

**Venue** : A-203

This is an introductory course for mathematical logic. In the course, we will cover propositional logic, first-order logic, logical theories, and (un)decidablity of various theories. Most of the course is about the theoretical foundation of logic. Additionally, we will use SAT solvers, first order provers, and assisted theorem provers for some hands on experience.

- Text book: A Mathematical Introduction to Logic, Second Edition - Herbert B. Enderton
- Book: First-Order Logic and Automated Theorem Proving - Melvin Fitting
- Book: Symbolic logic, Fifth edition - Irving M. Copi
- NPTEL Video Course: Mathematical logic - Arindama Singh, IITM
- Book chapter: The Art of computer programming Section 7.2.2.2 (Beta version) - Donald Kunuth
- Coq tutorial
- Handbook of Satisfiability - by A. Biere (Editor), et al.
- Handbook of Automated reasoning - by A. Robinson (Editor), et al.

- Please do not take any lecture notes in the class. Slides will be online and plenty of other stuff is online. The age of notes is gone.
- Only electronic submissions of assignments (no papers). Please email the instructor either a scan of hand written answers or preferably a pdf file (if you unfortunately work in MS word or google doc then convert them into pdf)
- Assignments are due before the lecture on the due date. Deadlines are strict, no extensions.
- Please bring laptops to the lectures, we may do some programming in the class. Small mobile devices will not work.
- All presentations should be with slides. No chalk and board presentations.
- NEVER overtime your presentations.
- One is allowed to bring any electronic device in the exams. However, use of internet during the exam is not allowed.
**Please discuss the assignments, but not copy!**

- Assignments : 25%, 5% each
- Midterm : 20% (1 hour)
- Presentation: 15% (15 min)
- Final : 40% (2 hour)

- Introduction
- Course contents
- Sets,relations,Tuples,Functions
- Cardinality
- (No slides available; please look at the latest version of the course)

- Syntax
- Unique parsing
- Precedence order
- Semantics - satisfaction relation
- (No slides available; please look at the latest version of the course)
- Suggested reading : Fitting 2.1--2.4,Enderton 1.3-1.4 for unique parsing

- Decision problem
- Truth tables
- Substitution theorems
- Expressive power
- Common equivalences
- (No slides available; please look at the latest version of the course)
- Suggested reading : Fitting 2.5 for replacement theorems, Enderton 1.5 for truth tables

- Negation normal forms(NNF)
- Conjunctive normal forms(CNF)
- Tseitin's encoding
- Disjunctive normal forms(DNF)
- k-SAT/3-SAT
- (No slides available; please look at the latest version of the course)
- Suggested reading : Fitting 2.6-2.8 for CNF
- Suggested reading : For 3-SAT conversion NPTEL Video, watch after 10:58

- Tableaux
- Resolution
- Implementation issues in Resolution
- (No slides available; please look at the latest version of the course)
- Suggested reading : Fitting 3.1,3.3 for proof systems
- Suggested reading : For implementation issues in resolution NPTEL Video, watch after 18:42

- Soundness of Tableaux and Resolution
- Hinttika set
- Model existence theorem
- Compactness of Propositional logic
- Completeness of Tableaux and Resolution
- Semi-decidablity of implication
- (No slides available; please look at the latest version of the course)
- Suggested reading : Fitting 3.4-3.7 for soundness and completeness proofs
- Suggested reading : Enderton, p61-65 for the semi-decidablity (strongly recommended),

- Encoding NP hard problem into SAT
- Complexity of resolution proofs
- (No slides available; please look at the latest version of the course)
- Suggested reading : Kunuth p1-20 for very lucid discussion on encoding into SAT
- Suggested reading : Kunuth p57-60 for proof complexity (please help me understand the proof of the existence of the restriction, the solution of exercise 240)

- Discussion Assignment 1
- Coq Assisted theorem prover, basics - no theory, only usage
- 2-SAT
- (No slides available; please look at the latest version of the course)
- Coq proof script from the class
- Suggested reading : Coq tutorial (upto "Existence and Equality" heading)

- Horn SAT
- XOR-SAT

- BDDs
- Ordered BDDs
- Reduced ordered BDDs(ROBDDs)
- Canonicity
- BDD construction algorithms
- Suggested reading : Introduction to BDDs - Henrik Reif Anderson
- (No slides available; please look at the latest version of the course)

- DPLL
- 2-watched literals
- Clause Learning
- CDCL
- Decision ordering
- Restarts
- (No slides available; please look at the latest version of the course)
- Suggested reading: Handbook of satisfiability chapter 4 for CDCL (read ch. 3 before if you find ch. 4 difficult to read)
- Advanced reading: Kunuth whole book chapter

- Syntax
- Semantics
- (No slides available; please look at the latest version of the course)
- Suggested reading: Fitting 5.1,5.3,8.1,8.2
- Suggested video: NPTEL course: hurdles in giving meaning

- Substitution
- Herbrand model
- Hinttika set
- (No slides available; please look at the latest version of the course)
- Suggested reading: Fitting 5.2,5.4,5.5,8.3, and 8.4

- Model existence theorem
- Compactness
- Lowenheim-Skolem Theorem
- (No slides available; please look at the latest version of the course)
- Suggested reading: Fitting 5.6-5.9 and 8.5-8.6

- Tableaux
- Tableaux soundness and completeness
- Resolution
- Resolution soundness and completeness
- (No slides available; please look at the latest version of the course)
- Suggested reading: Fitting 6.1-6.4 and 8.7

- Unifiers
- Most general unification
- Robinsion's algorithm
- Skolem function
- (No slides available; please look at the latest version of the course)
- Suggested reading: Fitting 7.1-7.2
- See below for the possible presentation topics.

- Free tableaux
- Soundness and completeness of free tableaux
- (No slides available; please look at the latest version of the course)
- Suggested reading: Fitting 7.4,7.7,7.8,8.9

- Replacement theorem
- Prenex Form
- Skolemization
- First order CNF
- Resolution theorem proving
- (No slides available; please look at the latest version of the course)
- Suggested reading: Fitting 7.10-12,

- Reduction order
- Completeness of resolution using the reduction order
- Complete resolution proof system with ordering constraints
- (No slides available; please look at the latest version of the course)
- How to give a great research talk -- Simon Peyton Jones
- Suggested reading: Handbook of Automated reasoning - Chapter 2 section 1-3

- Redundancy criterian
- Standard redundancy criterian
- FOL theorem prover with ordering and subsumption
- Completeness of the theorem prover
- Suggested reading: Handbook of Automated reasoning - Chapter 2, section 4(pp 17-28)
- Since the topics were not fully covered in the class, slides are not available!
- However, the above reading is part of the final exam.

- Theories
- Decidability of theories
- Example of theories
- (No slides available; please look at the latest version of the course)
- Suggested reading: Endertorn section 2.6, section 3.1

- DPLL(T)
- Theory propagations
- EUF theory solver
- Optimizations
- (No slides available; please look at the latest version of the course)

- Modal Logic - Rahul
- Monadic Second Order Logic - Gunjan
- Type Theory - Anamay

- A specialized subtheory of number theory
- Representability
- Numeralwise determined
- (No slides available; please look at the latest version of the course)(updated on 2015-11-09)
- Suggested reading: Endertorn section 3.3 (if any difficulty also read 3.0)

- Gödel numbers
- encoding proofs using Gödel numbers
- recursive relations
- the incompleteness theorem
- (No slides available; please look at the latest version of the course)
- Suggested reading: Endertorn section 3.4-3.5(first three theorems)

- Assignment 5 due (please submit well before the final exam!)

- Conflict clause management in SAT solvers
- Modal logic/Temporal logic
- ZF axiomatization of set theory
- Skolem's paradox
- Schaefer's dichotomy theorem and other low complexity SAT subclasses
- Second order logic, and type theory in general
- Separation logic
- Fundamentals of Coq proof system
- Databases and logic
- Automata theory and logic
- Any other topic you think is suitable for the class!

Last modified: Sun Jul 10 18:52:54 IST 2016