# Mathematical logic 2016

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.

## Evaluation structure

• Assignments : 40%, 4% each
• Midterm : 20% (1 hour)
• Presentation: 10% (15 min)
• Final : 30% (1.5 hour)
May change later.

## Lectures

The following lecture schedule is tentative

#### 2016-08-03 (Wednesday 9:30-11:00 and 11:30-13:00) : Week 1 - Introduction, Notation, Propositional Logic - syntax and semantics

• 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

#### 2016-08-12 : Week 2 - Equivalences, Normal forms, Encoding into SAT

• 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

#### 2016-08-21 (Sunday 11:45-13:15 and 14:15-15:45) : Week 3 - Proof methods, Soundness and completeness

• 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),

#### 2016-08-26 : Week 4 - Proof complexity, and low complexity subclasses

• 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

#### 2016-09-02 : Week 5 - Binary decision diagrams(BDDs), DPLL and SAT solvers

• 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

#### 2016-09-23 : Week 7 - Model existence theorem and compactness, and proof systems for FOL

• 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

#### 2016-09-30 : Week 8 - Unification, Normal forms and Resolution theorem proving

• Unifiers, Most general unification, Robinsion's algorithm
• Skolem functions
• Replacement theorems
• Rename apart, Prenex Form, Skolemization, First order CNF
• Resolution theorem proving
• 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

#### 2016-10-07 : Week 9 - First order theorem provers

• 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

#### 2016-10-14 : Week 10 - Logical theories and Sat modulo theory solvers

• 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

#### 2016-10-21/11-08/11-11 : Week 11 - Gödel's Incompleteness theorem

• 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

#### 2016-10-12: Week 12 - Coq - a proof assistant

• 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

## Presentation topics

• Conflict clause management in SAT solvers
• Modal logic/Temporal logic
• ZF axiomatization of set theory