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.
Source material
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
- Advanced reading: Kunuth whole book chapter
2016-09-09 : Week 6 - First order logic(FOL)
2016-09-16 : Midterm
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
- 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
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
- Suggested reading: Endertorn section 3.3 (if any difficulty, please also read 3.0), 3.4-3.5(first three theorems)
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
2016-11-25 : Final exam
Presentation topics
- 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!
Student presentation
Student presentations will be held at the end of the last lecuture.
Please choose your presentation topic before Week 9.
There will be no assignment on week 11 for
the preparation for the presentation.
Last modified: Mon Nov 21 12:07:23 IST 2016