E0 205 Mathematical Logic and Theorem Proving

Teaching Assistants: Alvin George and Prathamesh Patil.

• 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:
    • Proof system
    • Consistency and Hintikka theory; Completeness
    • Normal Forms and Resolution
    • DPLL algorithm
  • First-Order Logic:
    • Syntax and Semantics
    • Proof system (Sequent Calculus)
    • Completeness
    • Lowenheim-Skolem and Compactness
  • Theories and Decision Procedures:
    • Equality and Uninterpreted Functions (EUF)
    • Linear Arithmetic
    • Array logic
    • Nelson-Oppen combination
    • DPLL(T)

• Meeting Schedule

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

First meeting will be at 3:30pm on Wed 4th Jan 2023.

• Lectures
  1. 04-01-2023: Course Overview: Kamal and Deepak.
  2. 09-01-2023: Propositional Logic
  3. 11-01-2023: Sequent Calculus for PL
  4. 16-01-2023: Recap and Exercise. Consistency
  5. 18-01-2023: Maximally Consistent Sets
  6. 23-01-2023: Completeness
  7. 25-01-2023: First-Order Logic Syntax and Semantics

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

• Assignments
  • Assignment 1 (Propositional Logic) due on Mon 30 Jan 2023.

• Seminar Topics
  • Decision Procedure for Real Arithmetic (Seidenberg and Tarski)
  • Bit Vector Arithmetic (Kroening-Stichman (2e) Ch~6).
  • 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 Link to paper).
  • Fraisse's Theorem on elementary equivalence (EFT, Ch XII).
  • Uninterpreted Programs (Mathur, Madhusudan, Vishwanathan, PoPL 2019).
  • 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:
  • Mid-semester Exam: TBA.
  • Final Exam: TBA.