# 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.

## 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.
• 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-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
• 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
• 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
• Horn SAT
• XOR-SAT

#### 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-28 : Presentations (choose topic by Lecture 18)

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

#### 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