E0 205 Mathematical Logic and Theorem Proving
D'Souza and Kamal
P. Habeeb and
- Motivation and Objectives
This course is about mathematical logic with a focus on automated
reasoning techniques that are useful in reasoning about programs.
In the first part of the course we cover Propositional and
First-Order logic and some of the classical results like sound and
complete proof systems, compactness, and decidability of the
satisfiability/validity problems. In the second part we focus on
decision procedures for various theories that arise while reasoning
about assertions in programs.
- Proofs in arithmetic
- Propositional logic, proof
- Decision procedure, completeness and compactness
- Proof systems
- Completeness and compactness
Theories and Decision Procedures:
- Equality and Uninterpreted Functions (EUF)
- Linear Arithmetic
- Nelson-Oppen combination
- Array logics
- Constrained Horn Clauses
- Meeting Schedule
First meeting will be at 3:30pm on Wed 24th Feb
Meetings are online on Google Meet.
- (24-Feb-2021) Course Overview: Mathematical Logic, Decision Procedures + Course Logistics.
- (01-Mar-2021) Zeroeth-Order Logic:
[Recording Part 1]
[Recording Part 2].
- (03-Mar-2021) Zoroeth-Order Logic:
Models. [Slides] [Recording]
- (08-Mar-2021) Zoroeth-Order Logic:
Theories to Models. [Slides] [Recording]
- (10-Mar-2021) Intro to Propositional
Decidability / Resolution. [Slides]
- (24-Mar-2021 and 29-Mar-2021) DPLL Satisfiability
First Order Logic. [Slides]
First Order Logic (Proof System). [Slides]
First Order Logic (Universal Fragment). [Slides]
First Order Logic (Existential
Theories to Models. [Slides]
- (26,28-Apr-2021 and 03-May-2021)
Equality and Uninterpreted Functions (EUF). [Slides]
- (05, 10, 12-May-2021)
Linear Arithmetic. [Slides]
05-May-2021, Part 1]
05-May-2021, Part 2]
- (17, 19-May-2021)
Array Logic. [Slides]
Constrained Horn Clauses (Sumanth Prabhu). [Slides]
Model-Based Projection (Stanly Samuel). [Slides]
Wrap-up lecture [Slides]
- Books and other material
- First-order Logic and automated theorem proving, Melvin Fitting,
- Logic for Computer Science -- Foundations for Automatic Theorem
Proving, Jean H. Gallier.
- Decision Procedures, Kroening and Strichman, Springer, 2008.
- The Calculus of Computation, Bradley and Manna, Springer, 2007.
- Computability and logic, George Boolos, John Burgess and Richard Jeffrey,
Cambridge U Press, 2007.
- An Introduction to Logic, Madhavan Mukund and S P Suresh, Lecture
Notes, Chennai Mathematical Institute (2011).
- Seminar Topics
- Decision Procedure for Real Arithmetic (Seidenberg and
Tarski) (Mohith and Upamanyu, 10am Tue 11th May)
- Bit Vector Arithmetic (Kroening-Stichman (2e)
Ch~6). Nabarun and Prathamesh (10am Tue 18th May). Slides.
- Maximal Specification Synthesis (Albarghouthi, Dillig,
Gurfinkel, POPL 2016) (Logical Abduction). Alvin (10am, Tue
- Undecidability of First-Order Logic (Reference: Boolos,
Burgess, and Jeffrey) K. Sreehari (10am, Tue 1st June)
- A Linear-Time algorithm for Horn SAT (Dowling and Gallier,
J. Logic Programming 1984
paper). Sai Sanjeev and Shreepranav (3:30pm, Wed 2nd
- Uninterpreted Programs (Mathur, Madhusudan, Vishwanathan, PoPL
2019). Ajinkya (10am, Thu 3rd June)
- Decision Procedure for Presburger Logic (Reference: Boolos,
Burgess, and Jeffrey). Gaurish and Prashik (3:30pm, Wed 9th June).
- E-Matching for Quantified Formulas (Greg Nelson PhD thesis (1980),
De Moura and Bjorner CADE 2007)
Weightage for evaluation:
Mid-semester Exam: 20%
Assignments + Quizes + Seminar: 40%
Final Exam: 40%
- Exam Schedule:
3:30pm Wed 21st April 2021.
Final Exam: 3:30pm Fri, 04 June 2021.