 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
FirstOrder 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

FirstOrder Logic:
 Syntax and Semantics
 Proof system (Sequent Calculus)
 Completeness
 LowenheimSkolem and Compactness

Theories and Decision Procedures:
 Equality and Uninterpreted Functions (EUF)
 Linear Arithmetic
 Array logic
 NelsonOppen 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
 04012023: Course Overview: Kamal
and Deepak.
 09012023: Propositional Logic
 11012023: Sequent Calculus for PL
 16012023: Recap and
Exercise. Consistency
 18012023: Maximally Consistent
Sets
 23012023: Completeness
 25012023: FirstOrder Logic Syntax and Semantics
 Books and other material
 Mathematical Logic, H.D. Ebbinghaus, J. Flum, W. Thomas,
(3rd edition), Springer, 2021.
 Firstorder Logic and automated theorem proving, Melvin Fitting,
SpringerVerlag, 1990.
 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).
 Assignments
 Seminar Topics
 Decision Procedure for Real Arithmetic (Seidenberg and
Tarski)
 Bit Vector Arithmetic (KroeningStichman (2e)
Ch~6).
 Maximal Specification Synthesis (Albarghouthi, Dillig,
Gurfinkel, POPL 2016) (Logical Abduction).
 Undecidability of FirstOrder Logic (Reference: Boolos,
Burgess, and Jeffrey)
 A LinearTime 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).
 EMatching for Quantified Formulas (Greg Nelson PhD thesis (1980),
De Moura and Bjorner CADE 2007)

Weightage for evaluation:

Midsemester Exam: 20%

Assignments + Quizes + Seminar: 40%

Final Exam: 40%
 Exam Schedule:

Midsemester Exam:
TBA.

Final Exam: TBA.