E0 205 Mathematical Logic and Theorem Proving
D'Souza and Kamal
Alvin George 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.
- Proof system
- Consistency and Hintikka theory; Completeness
- Normal Forms and Resolution
- DPLL algorithm
- Syntax and Semantics
- Proof system (Sequent Calculus)
- Lowenheim-Skolem and Compactness
Theories and Decision Procedures:
- Equality and Uninterpreted Functions (EUF)
- Linear Arithmetic
- Array logic
- Nelson-Oppen combination
- Meeting Schedule
3:30pm Mon/Wed in Room 252 CSA Department.
First meeting will be at 3:30pm on Wed 4th Jan
- 04-01-2023: Course Overview: Kamal
- 09-01-2023: Propositional Logic
- 11-01-2023: Sequent Calculus for PL
- 16-01-2023: Recap and
- 18-01-2023: Maximally Consistent
- 23-01-2023: Completeness
- 25-01-2023: First-Order Logic Syntax and Semantics
- Books and other material
- Mathematical Logic, H.D. Ebbinghaus, J. Flum, W. Thomas,
(3rd edition), Springer, 2021.
- 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
- Bit Vector Arithmetic (Kroening-Stichman (2e)
- Maximal Specification Synthesis (Albarghouthi, Dillig,
Gurfinkel, POPL 2016) (Logical Abduction).
- Undecidability of First-Order Logic (Reference: Boolos,
Burgess, and Jeffrey)
- A Linear-Time algorithm for Horn SAT (Dowling and Gallier,
J. Logic Programming 1984
- Fraisse's Theorem on elementary equivalence (EFT, Ch XII).
- Uninterpreted Programs (Mathur, Madhusudan, Vishwanathan, PoPL
- Decision Procedure for Presburger Logic (Reference: Boolos,
Burgess, and Jeffrey).
- 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:
Final Exam: TBA.