E0 205 Mathematical Logic and Theorem Proving

Teaching Assistants: Alan Jojo and Abhishek Uppar

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

• Course Outline
  • Propositional Logic:
    • Semantics and Normal Forms
    • Sequent Calculus proof system
    • Consistency and Completeness
  • First-Order Logic:
    • Syntax and Semantics
    • Definability
    • Substitution and Prenex Normal Form
    • Sequent Calculus
    • Completeness
    • Lowenheim-Skolem and Compactness
  • Theories and Decision Procedures:
    • DPLL algorithm
    • Equality and Uninterpreted Functions (EUF)
    • Linear Arithmetic
    • Array logic
    • Nelson-Oppen combination
    • DPLL(T)

• Meeting Schedule

3:30pm Mon/Wed in Room 117 CSA Department.

First meeting will be at 3:30pm on Mon 6th Jan 2025.

Use code bim2wm5 to join MLTP 2025 Team on Teams.

• Lectures
  1. 06-01-2025: Course Overview: Kamal and Deepak.
  2. 08-01-2025: Propositional Logic.
  3. 13-01-2025 and 15-01-2025: Sequent Calculus for PL.
  4. 20-01-2025: Quiz + Consistency
  5. 22-01-2025, 27-01-2025: Maximally Consistent Sets and Completness.
  6. 29-01-2025: First-Order Logic Syntax and Semantics
  7. 03-02-2025, 05-02-2025, 12-02-2025: : First-Order Definability
  8. 10-02-2025: Quiz and Definability.
  9. 17-02-2025: Midsem.
  10. 19-02-2025: Substitution and Prenex Normal Form
  11. 24-02-2025, 26-02-2025: Sequent Calculus for FO
  12. 26-02-2025: Consistency and Completness for FO
  13. 03-03-2025, 05-03-2025: Completness for FO by Michael Kohlhase (FAU, Erlangen-Nurnberg). Also see his Notes.
  14. 10-03-2025, 12-03-2025: DPLL and CDCL
  15. 17-03-2025, 19-03-2025: Equality and Uninterpreted Functions.
  16. 24-03-2025, 26-03-2025, 02-04-2025 Linear Arithmetic.
  17. 07-04-2025, 09-04-2025 Array Logic.
  18. 15-04-2025 Nelson-Oppen Combination.

• Books and other material
  1. Mathematical Logic, H.D. Ebbinghaus, J. Flum, W. Thomas, (3rd edition), Springer, 2021.
  2. First-Order Logic and Automated Theorem Proving, Melvin Fitting, Springer-Verlag, 1990.
  3. Logic for Computer Science -- Foundations for Automatic Theorem Proving, Jean H. Gallier.
  4. Decision Procedures, Kroening and Strichman, Springer, 2008.
  5. The Calculus of Computation, Bradley and Manna, Springer, 2007.
  6. Computability and Logic, George Boolos, John Burgess and Richard Jeffrey, Cambridge U Press, 2007.
  7. An Introduction to Logic, Madhavan Mukund and S P Suresh, Lecture Notes, Chennai Mathematical Institute (2011).
  8. Jakob Nordstrom's lecture at SAT+SMT Winter School.
  9. Chapter on Confilict Driven Clause Learning by Joao Marques-Silva, Ines Lynce and Sharad Malik, in Handbook of Satisfiability,
  10. Greg Nelson's PhD Thesis.

• Assignments
  • Assignment 1 (Propositional Logic) due on Wed 05 Feb 2025.
  • Assignment 2 (First-Order Logic) due on Mon 24 Feb 2025.
  • Assignment 3 (FO, DPLL and EUF) due on Wed 02 Apr 2025.
  • Assignment 4 (EUF using DPLL+Ackermann) due on Mon 21 Apr 2025.
  • Assignment 5 (Linear Arithmetic, Array Logic, Nelson-Oppen) (not to be handed in).

• Seminar Topics
  • Bit Vector Arithmetic (Kroening-Stichman (2e) Ch~6).
  • Undecidability of First-Order Logic (Reference: Boolos, Burgess, and Jeffrey).
  • A Linear-Time algorithm for Horn SAT (Dowling and Gallier, J. Logic Programming 1984. Link to paper).
  • Decision Procedure for Presburger Logic (Reference: Boolos, Burgess, and Jeffrey).
  • Uninterpreted Programs (Mathur, Madhusudan, Vishwanathan, PoPL 2019).
  • Fraisse's Theorem on elementary equivalence (EFT, Ch XII).
  • Decision Procedure for Real Arithmetic (Seidenberg and Tarski)
  • Maximal Specification Synthesis (Albarghouthi, Dillig, Gurfinkel, POPL 2016) (Logical Abduction).
  • 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:
  • Mid-semester Exam: 3.30pm Mon 17 Feb 2025.
  • Final Exam: 2pm Tue 22 Apr 2025.