Mathematical logic 2015
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.
Source material
Some course rules
- 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!
Evaluation structure
- Assignments : 25%, 5% each
- Midterm : 20% (1 hour)
- Presentation: 15% (15 min)
- Final : 40% (2 hour)
May change later.
Lectures
2015-08-10 : Lecture 1 - Introduction and background
2015-08-12 : Lecture 2 - Propositional Logic - syntax and semantics
2015-08-17 : Lecture 3 - Decision problem, Truth tables, Equivalences
2015-08-19 : Lecture 4 - Normal forms
2015-08-24 : Lecture 5 - Proof methods - Tableaux and Resolution
2015-08-26 : Lecture 6 - Soundness and completeness
- 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),
2015-08-31 : Lecture 7 - Proof Complexity,Encoding problems into SAT
- 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)
2015-09-02 : Lecture 8 - Coq and Low complexity subclasses
Spilled over to next lecture
2015-09-07 : Lecture 9 - Binary decision diagrams(BDDs)
2015-09-09 : Lecture 10 - DPLL and SAT solvers
2015-09-14 : NO Lecture
2015-09-16 : Midterm
2015-09-21 : Lecture 11 - First order logic(FOL) - syntax and semantics
2015-09-23 : Lecture 12 - Substitution, Herbrand model, Hinttika set
2015-09-28 : Lecture 13 - Model existence theorem and Compactness
2015-09-30 : Lecture 14 - Tableaux and Resolution for FOL
2015-10-05 : Lecture 15 - Unification
2015-10-07 : Lecture 16 - Tableaux with free variables
2015-10-12 : Lecture 17 - Normal forms and Resolution theorem proving
2015-10-14 : Lecture 18 - First order theorem provers
2015-10-19 : Lecture 19 - First order theorem provers II
- 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.
2015-10-21 : Lecture 20 - Logical theories
2015-10-26 : Lecture 21 - Sat modulo theory solvers
2015-10-28 : Presentations (choose topic by Lecture 18)
- Modal Logic - Rahul
- Monadic Second Order Logic - Gunjan
- Type Theory - Anamay
2015-11-02 : Lecture 22 - Gödel's Incompleteness theorem - Representability
2015-11-04/09 : Lecture 23/24 - Gödel's Incompleteness theorem - Gödel numbering
2015-11-23 : Final exam
- Assignment 5 due (please submit well before the 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!
Last modified: Sun Jul 10 18:52:54 IST 2016