E0 205 Mathematical Logic and Theorem Proving

Teaching Assistants: P. Habeeb and Stanly Samuel.

• 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
  • Zeroth-Order/Propositional Logic:
    • Proofs in arithmetic
    • Propositional logic, proof
    • Decision procedure, completeness and compactness
  • First-Order Logic:
    • Proof systems
    • Undecidability
    • Completeness and compactness
  • Theories and Decision Procedures:
    • Equality and Uninterpreted Functions (EUF)
    • Linear Arithmetic
    • Nelson-Oppen combination
    • Array logics
    • Constrained Horn Clauses

• Meeting Schedule

3:30pm Mon/Wed

First meeting will be at 3:30pm on Wed 24th Feb 2021.

Meetings are online on Google Meet. Google Meet Meeting Link

• Lectures
  1. (24-Feb-2021) Course Overview: Mathematical Logic, Decision Procedures + Course Logistics. Recording Part 1, Recording Part 2
  2. (01-Mar-2021) Zeroeth-Order Logic: Syntax. [Slides] [Recording Part 1] [Recording Part 2].
  3. (03-Mar-2021) Zoroeth-Order Logic: Models. [Slides] [Recording]
  4. (08-Mar-2021) Zoroeth-Order Logic: Theories to Models. [Slides] [Recording]
  5. (10-Mar-2021) Intro to Propositional Logic. [Slides] [Recording]
  6. (15-Mar-2021) Consistency. [Slides] [Recording]
  7. (17-Mar-2021) Completeness. [Slides] [Recording]
  8. (22-Mar-2021) Decidability / Resolution. [Slides] [Recording]
  9. (24-Mar-2021 and 29-Mar-2021) DPLL Satisfiability Procedure. [Slides] [Whiteboard notes [Recording 24 Mar] [Recording 29 Mar]
  10. (31-Mar-2021) First Order Logic. [Slides] [Recording]
  11. (05-Apr-2021) First Order Logic (Proof System). [Slides] [Recording]
  12. (07-Apr-2021) First Order Logic (Universal Fragment). [Slides] [Recording]
  13. (12-Apr-2021) First Order Logic (Existential Fragment). [Slides] [Recording]
  14. (19-Apr-2021) Theories to Models. [Slides] [Recording]
  15. (26,28-Apr-2021 and 03-May-2021) Equality and Uninterpreted Functions (EUF). [Slides] [Recording 26-Apr-2021] [Recording 28-Apr-2021] [Recording 03-May-2021]
  16. (05, 10, 12-May-2021) Linear Arithmetic. [Slides] [Recording 05-May-2021, Part 1] [Recording 05-May-2021, Part 2] [Recording 10-May-2021] [Recording 12-May-2021]
  17. (17, 19-May-2021) Array Logic. [Slides] [Recording 19-May-2021]
  18. (24-May-2021) Constrained Horn Clauses (Sumanth Prabhu). [Slides] [Recording]
  19. (26-May-2021) Model-Based Projection (Stanly Samuel). [Slides] [Recording]
  20. (31-May-2021) Wrap-up lecture [Slides] [Recording]

• Books and other material
  1. First-order Logic and automated theorem proving, Melvin Fitting, Springer-Verlag, 1990.
  2. Logic for Computer Science -- Foundations for Automatic Theorem Proving, Jean H. Gallier.
  3. Decision Procedures, Kroening and Strichman, Springer, 2008.
  4. The Calculus of Computation, Bradley and Manna, Springer, 2007.
  5. Computability and logic, George Boolos, John Burgess and Richard Jeffrey, Cambridge U Press, 2007.
  6. An Introduction to Logic, Madhavan Mukund and S P Suresh, Lecture Notes, Chennai Mathematical Institute (2011).

• Assignments
  • Assignment 1 due by 2pm on Mon 15 March 2021.
  • Assignment 2 due on Wed 14 April 2021.
  • Assignment 3 Q1,2,3 due on Mon 10 May (Tutorial on 07-May-2021 slides on Python/Z3, example code. [Recording 06-May-2021], [Recording 10-May-2021].)
  • Assignment 4 due on Mon 31 May 2021.

• Seminar Topics
  • Decision Procedure for Real Arithmetic (Seidenberg and Tarski) (Mohith and Upamanyu, 10am Tue 11th May) Slides.
  • 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 25th May).
  • 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 Link to paper). Sai Sanjeev and Shreepranav (3:30pm, Wed 2nd June). Slides.
  • 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:
  • Mid-semester Exam: 3:30pm Wed 21st April 2021.
  • Final Exam: 3:30pm Fri, 04 June 2021.