**Instructor** : Ashutosh Gupta

**Timings** : Friday, 11:45-13:15 and 14:15-15:45

**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.
- Algorithms for the Satisfiability (SAT) Problem - Gu et. al. p67-74
- Introduction to BDDs - Henrik Reif Anderson

- Assignments : 40%, 4% each
- Midterm : 20% (1 hour)
- Presentation: 10% (15 min)
- Final : 30% (1.5 hour)

- Introduction, course contents
- Sets, relations, tuples, functions, etc. Cardinality
- Propositional logic syntax, unique parsing, precedence order
- Semantics, satisfaction relation, decision problem, truth tables
- Lecture 1 slides, Lecture 2 slides
- Assignment: Excercise 1.6, 1.13, 1.16, 2.16, and 2.18
- Suggested reading : Fitting 2.1--2.4,Enderton 1.3-1.4 for unique parsing, Enderton 1.5 for truth tables

- Substitution theorems, equivalences, Expressive power
- Negation/Conjunctive/Disjunctive normal forms(NNF/CNF/DNF)
- Tseitin's encoding, k-SAT/3-SAT
- Encoding NP-complete problems into SAT
- Lecture 3 slides, Lecture 4 slides
- Assignment: Excercise 3.12, 3.14, 3.15, 4.13, and 4.16
- Suggested reading : Fitting 2.5 for replacement theorems, Fitting 2.6-2.8 for CNF
- Suggested reading : For 3-SAT conversion NPTEL Video, watch after 10:58
- Suggested reading : Kunuth p1-20 for very lucid discussion on encoding into SAT

- Proof methods: Tableaux and Resolution
- Implementation issues in Resolution
- Hinttika set, Model existence theorem
- Soundness and Completeness of Tableaux and Resolution
- Compactness of Propositional logic, Semi-decidablity of implication
- Lecture 5 slides, Lecture 6 slides
- Assignment: Excercise 5.9, 5.11, 6.11, and 6.12
- Suggested reading : Fitting 3.1,3.3 for proof systems, 3.4-3.7 for soundness and completeness proofs
- Suggested reading : For implementation issues in resolution NPTEL Video, watch after 18:42
- Suggested reading : Enderton, p61-65 for the semi-decidablity (strongly recommended),

- Complexity of resolution proofs
- Subclasses: 2-SAT,Horn SAT,XOR-SAT,SLUR,q-Horn
- Lecture 7 Slides, Lecture 8 Slides
- Assignment: Excercise 7.4, 7.6, 8.6.1,8.11,8.14
- Suggested reading : Kunuth p57-60 for proof complexity
- Suggested reading : Algorithms for the Satisfiability (SAT) Problem - Gu et. al. p67-74 for subclasses

- BDDs,Ordered BDDs,Reduced ordered BDDs(ROBDDs)
- Canonicity of ROBDDs, BDD construction algorithms
- DPLL,Clause Learning,CDCL
- 2-watched literals, Decision ordering, Restarts
- Proof generation in DPLL, resolution proof minimization
- Lecture 9 Slides, Lecture 10 Slides
- Assignment: Excercise 10.10
- Suggested reading : Introduction to BDDs - Henrik Reif Anderson
- Suggested reading: Handbook of satisfiability chapter 4 for CDCL
- Advanced reading: Kunuth whole book chapter

- Syntax, Semantics of FOL
- Substitution,Herbrand model,Hinttika set
- Lecture 11 Slides, Lecture 12 Slides
- Assignment: Excercise 11.10, 11.11, 12.4, 12.5 (due on 7th week)
- Suggested video: NPTEL course: hurdles in giving meaning
- Suggested reading: Fitting 5.1-5,8.1-4
- Suggested reading: Enderton 2.2 p90-99

- Model existence theorem, Compactness, Lowenheim-Skolem Theorem
- Tableaux and Resolution proof systems
- Tableaux and Resolution soundness and completeness
- Lecture 13 slides, Lecture 14 slides
- Suggested reading: Fitting 5.6-5.9, 6.1-6.4, and 8.5-8.7
- Assignment: Excercise 13.3, 13.6, 14.9

- Unifiers, Most general unification, Robinsion's algorithm
- Skolem functions
- Replacement theorems
- Rename apart, Prenex Form, Skolemization, First order CNF
- Resolution theorem proving
- Suggested reading: Fitting 7.1-7.2,7.10-12
- Lecture 15 slides, Lecture 16 slides
- Assignment: Excercise 15.6, 15.7, 16.7, 16.9
- Choose presentation topic before next week!
- FYI: How to give a great research talk -- Simon Peyton Jones

- Reduction order
- Completeness of resolution using the reduction order
- Complete resolution proof system with ordering constraints
- Redundancy criterian, Standard redundancy criterian
- FOL theorem prover with ordering and subsumption
- Completeness of the theorem prover
- Lecture 17 slides,
- Assignment: Excercise 17.8
- Suggested reading: Handbook of Automated reasoning - Chapter 2 section 1-4

- Theories, Decidability of theories
- Example of theories
- DPLL(T),Theory propagations
- EUF theory solver
- Optimizations
- Lecture 19 slides, Lecture 20 slides
- Assignment: Excercise 19.5,20.6,20.7
- Suggested reading: Endertorn section 2.6, section 3.1

- A specialized subtheory of number theory
- Representability, Numeralwise determined
- Gödel numbers, Encoding proofs using Gödel numbers
- Recursive relations
- The incompleteness theorem
- Lecture 21 slides, Lecture 22 slides
- Suggested reading: Endertorn section 3.3 (if any difficulty, please also read 3.0), 3.4-3.5(first three theorems)

- Student presentation.
- Prerona Chatterjee - Skolem's paradox
- Coq Assisted theorem prover, basics - no theory, only usage
- Coq syntax, tactics, basic type system, proof scripts, proof terms
- Boolean reasoning, Predicate logic, Equality, Inductive types, Fixedpoints
- Suggested reading : Coq tutorial
- Suggested reading : Another Coq tutorial

- 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: Mon Nov 21 12:07:23 IST 2016