Preliminary Material
Preliminary logic primer, P. Madhusudan (for CS173)
Notes on induction on natural numbers, P. Madhusudan (for CS173)
More notes on induction, Chandra Chekuri (for CS173)
Motivation, Introduction to Logic, The place of logic in Computer Science, Themes covered in the course, Logic in the AI era, Administrivia
Informal introduction to first order logic; syntax of FO logic for any signature, informal semantics over first-order structures, FO over a single structure, over a class of structures, and over all structures, theories of a structure and a class of structures, theory of a set of axioms
LCS (Logic in CS notes, see resources page for link); Chapter 1Discussion theory of single structure, theory of a group of structures, and theory given by axioms continued; Theory of FOL and the relation between determining tautologies in FOL and other problems; Non-isomorphic structures that are indistinguishable using the power of first-order logic;
Overview of some main topics that will be covered in the course: (1) Dual-view between proofs and computation; review of Turing Machines; Decidable, recursively enumerable (r.e.) languages, and relationships between them; Halting problem; (2) Propositional Logic; Resolution proof system and its connection to SAT solvers; Compactness and completeness of propositional logic; (3) Godel's completeness theorem (i.e., theory of FOL is r.e.) and proof using quantifier instantiation; Compactness for FOL; Consequences of completeness theorem, including decidability/recursive enumerability of theory of single structure, theory of a finite or recursive set of axioms, etc; Connection between r.e and axiomatizability; (4) Decidability of particular theories; Natural numbers/rationals/reals with addition and/or multiplication; Techniques for proving decidability; Quantifier Elimination; Techniques for proving undecidability using reductions from problems on Turing Machines; (5) Quantifier-free theories and combinations of quantifier-free theories; SMT solvers.
Syntax and semantics of propositional logic; Truth tables; Models of propositional logic; Grammars, syntax trees, and induction on the structure of propositional formulas; Satisfiability and validity; P, NP, and co-NP, refresher about reductions, satisfiability is NP-complete, proving validity using satisfiability by refutation (connection to SAT solvers); Relevance lemma, occurrences of propositions in a formula; Compactness of propositional logic and proof
LCS; Chapter 2 until 2.3Continuing discussion about the compactness theorem for propositional logic, proof revisited; Entailment, Connection between the contrapositive of compactness and the idea of proofs for propositional validity; Applications of compactness, Four-colorability of infinite planar graphs; Conjunctive Normal Form, Tseitin transformation, Equisatisfiability; Proof systems for propositional logic, Resolution
LCS; Chapter 2 until 2.4Resolution continued, Examples of resolution proofs; Formal presentation of resolution, Resolution Lemma, Soundness of resolution and formal proof; Completeness of resolution and formal proof; Decision tree view of resolution proofs, Connection to SAT solvers
LCS; Chapter 2 until 2.4. Toniann Pitassi's notes on resolution (see resources page).First-Order Logic, syntax, semantics, models/structures and interpretation; Free variables; First-Order sentences, properties of sentences; Theory of a model, theory of a class of models, negation completeness; Theory of graphs; Tautologies; Theory of reals; Theory of a set of axioms, axiomatizable theories
Quantifier elimination (QE); Dense linear orders without endpoints (DLOWE); Disjunctive Normal Form; Decision procedure for DLOWE using QE; Theory of Reals and Rationals with order; Consequences of QE: decidability, axiomatizability; Elementary equivalence
LCS; Chapter 3 until 3.2Recap of QE for DLOWE; QE for Rationals/Reals with < and +, Ferrante and Rackoff's trick of averages; Complete (infinitary) axiomatization of Rationals/Reals with < and +
LCS; Chapter 3, Section 3.3 onwardsRecap of concepts in computability, Turing Machines, Decidability, Recursive languages, Recursively enumerable languages, Reductions; Proof of undecidability of validity for First-Order Logic, Construction using an encoding of the number line, Encoding Turing Machine computation on a number line, Nonstandard models and pitfalls in reductions; Proof of undecidability of validity for First-Order Logic over finite models
LCS; Chapter 4Recap of incompleteness for finite graphs; Brief look at incompleteness of program verification; First-Order Logic with theory of equality (uninterpreted functions), Universally quantified/quantifier-free fragment, Decidability of validity for quantifier-free formulas over uninterpreted functions, Existence of finite 'term' model obtained from terms occurring in the formula, NP-completeness; Algorithm for conjunctive quantifier-free formulas over uninterpreted functions, Congruence closure, Connection to SMT solvers
LCS; Chapter 5 until 5.2, page 46Continuing presentation of congruence closure algorithm for QF theory of equality, Terms and term model; Disjoint set datastructures; Discussion of complexity of datastructure operations implementing congruence closure, Ackermann function, Inverse Ackermann, Primitive recursive functions; Example of applying congruence closure to prove unsatisfiability of a QF formula over equality
(1) LCS; Chapter 5 (2) CC; Chapter 9 until 9.2 (3) Papers about algorithms for equality reasoning by Shostak as well as Nelson and Oppen (see resources page)Recap of Turing Machines: Definition, Accept v/s reject v/s not halting, Language of a TM; Undecidability of halting, Cantor's diagonalization argument; Diagonal language is not r.e, Reduction to halting; Complexity classes, P, NP, NP-completeness, SAT is NP-complete, Cook-Levin theorem
Appendix A in notes from CS474 Fall 2021 by Mahesh Viswanathan and Madhusudan Parthasarathy (see resources page)Gödel's completeness theorem: Part 1: Restatement in terms of Turing Machines (validity is r.e), Connection to provability from Axioms; FOL with equality v/s FOL without equality, Axiomatizing Equality, Equivalence classes, Quotients; Overview of Completeness Theorem in four phases: (1) Negation followed by Prenex Normal Form (2) Skolemization (3) Herbrand's Theorem (4) Instantiation ad-infinitum and reduction to the decision procedure for theory of equality; View of term instantiation from the perspective of validity/proof; Detailed presentation of conversion to Prenex Normal Form; Detailed presentation of Skolemization
LCS; Chapter 6 until 6.2Continuing presentation of Skolemization, Intuition for Skolem functions using 'inaccessible elements'; Herbrand's Theorem: Submodels satisfying universal formulae, Function-closed submodels, Intuition for Herbrand's Theorem, Ground Term Model modulo congruence, Theorem statement and proof outline
LCS; Chapter 6, Section 6.3Recap of Herbrand's Theorem; Final Phase of Completeness Proof: Quantifier instantiation using ground terms (i.e., Herbrand universe); Compactness for ground formulas with equality, Reduction to propositional compactness, Modeling equality of terms using propositions with reflexivity, symmetry, transitivity, and congruence constraints, Equivalence between satisfiability of ground formulas and satisfiability of propositional modeling
LCS; Chapter 6, Section 6.5 until 6.5.1Recap of construction of Completeness Theorem, Connection between construction and FOL validity procedure based on instantiation followed by equality reasoning; Gödel's strong completeness theorem with a recursive set of axioms; Consequences of completeness theorem: Compactness of FOL, Connectivity is not expressible in FOL, Equivalence of axiomatizability in FOL (negation complete axiomatization) and decidability; Statement of incompleteness of arithmetic
LCS; Chapter 6, from Section 6.5.2 onwardsContinuing discussion of FO completeness and its consequences; Three primary incompleteness results to know: FOL over finite models is not r.e, FOL over naturals with addition and multiplication is not r.e, program verification is not r.e (not complete = validity is not r.e = not all valid theorems have proofs! Consequently, no proof system captures all valid theorems about incomplete theories.), Discussion of the contents of each incompleteness theorem and subtleties; Worked out example of FOL validity using procedure covered in class: uniqueness of identity in groups (given group axioms)
LCS; Chapter 6, read in particular Example 6.2Gödel's Incompleteness Theorem for natural numbers with addition and multiplication: Theorem statement using recursive enumerability (validity of the logic is not r.e.), Proof; Subtleties in proof and ramifications of incompleteness
LCS; Chapter 7, Section 7.2High-level recap of results covered in the course through the lens of questions given in LCS Chapter 1, Section 1.4; Quantifier-Free Logic, Notion of validity and satisfiability, Example: Theory of Arrays, Modeling arrays as functions with updates, Axioms for arrays with extensionality; Interesting Properties of Quantifier-Free Logics; [Property 1] Complexity of validity for conjunctive fragment of quantifier-free logics is very tractable, Splitting quantifier-free validity into (i) propositional reasoning and (ii) theory reasoning over conjunctuve formulas, Connection to SMT solvers; Combination of quantifier-free logics, Example: Axiomatic Combination of Theories --- (i) Natural numbers with addition and (ii) Uninterpreted functions (theory of equality); [Property 2] Combination of decidable quantifier-free theories is decidable, Combination of decidable first-order fragments (with quantifiers) can be undecidable, Example: Combination of natural numbers with addition and uninterpreted functions; [Property 3] Nelson-Oppen combination, Combination of decision procedures for individual theories (as black-boxes) to make a decision procedure for the combined theory, Connection to SMT solvers, Example of satisfiability for a formula over combined theories; Examples of quantifier-free logics: EUF (equality with uninterpreted functions), Algebraic Datatypes, Arrays, BitVectors, Strings, Integers, Reals; Overview of material to be covered about quantifier-free logics, CDCL
CC Chapter 3, See Section 3.7 for complexity resultsDecidable combination of decidable theories: Signatures disjoint except for equality, Stably infinite theories, Formal statement of Nelson-Oppen Combination, Formal proof of simple case for single-sorted logic: Rewriting a formula over combined theories to a boolean combination of formulae over individual theories, Construction of a satisfying model for the combined theory as an 'amalgam' of satisfying models for individual theories, Formal argument using structural induction on original formula; Connection to SMT solvers, Worked out toy example of decision procedure and model construction
CC Chapter 10, Section 10.2Motivation of finite model theory using connections to computer science: algorithms, databases, automata/regular languages over finite and infinite structures, descriptive complexity; Connectedness is not expressible in FOL over arbitrary models, Proof using compactness; Failure of compactness for finite models, Proof; EF Games: Intuition as indistinguishability between classes of models, Quantifier rank, Partial isomorphism, Definition of EF games and meaning of winning strategies for the players Spolier and Duplicator, Formal statement of the result; Arbitrarily large ordered structures cannot be distinguished using formulae of small quantifier rank (see Gurevich's Theorem), Proof intuition using EF games; Even-ness of the size of the universe is not expressible in FOL over finite models, Proof intuition using Gurevich's Theorem; Connectedness is not expressible in FOL over finite graphs, Formal proof: Line graphs, Induced graph of 'skip' connections, Expressing graph of skip connections as a logical formula over edge predicate, Reduction of connectedness to even-ness of universe; Connections to learning logics, Separability problem using positive and negative structures, Discussion of recent decidability results for synthesizing separators
LL Chapter 3 for formal presentation of EF games (Section 3.5 has a detailed proof which was not covered in class), see resources page for decidable synthesis results by Krogmeier and MadhusudanOverview of complexity classes, Time complexity: P, NP, co-NP, Polynomial Hierarchy, EXPTIME, Space complexity: NL, co-NL, PSPACE, NPSPACE, NL = co-NL, PSPACE = NPSPACE; Reachability in graphs is NL-complete, Circuit evaluation is P-complete; Descriptive complexity theory, Motivation, Examples, Definition of Second-Order Logic (SO) and Monadic Second-Order Logic (MSO); Fagin's Theorem: ∃SO = NP, Example: graph coloring, Informal, overview of proof; Immerman-Vardi Theorem: FO+lfp pver ordered strucutres = P; Formal presentation of FO+lfp, Fixpoint, Monotonicity, Least Fixpoint, Tarski-Knaster, Iterative computation of least fixpoint from a monotonic definition, Informal proof that the limit of the iterative computation is the lfp, Informal sketch of proof of Immerman-Vardi theorem
Continuing presentation of FO+lfp, Example of monotonic function, Lattices, Formal presentation of Tarski-Knaster, Connection between fixpoints and recursion; Applications of lfp computation, Defining semantics of imperative programming languages (operational semantics), Abstract Interpretation, Stating properties of datastructures; Incompleteness of FO+lfp; Applications of finite model theory to databases, Connection between SQL queries and FOL formulas, Datalog (SQL + lfp), Proof intuition for Immerman-Vardi Theorem; Finite Model Theory and Formal Languages, MSO on finite and infinite structures (words, trees), MSO over words = Regular languages, Applications to reactive systems verified against LTL specifications
Overview of model theory related to MSO on words: Connections to regular languages, Decidability and decision procedures using automata, Model checking with LTL specifications, Treewidth and Courcelle's theorem, Nested words and Visibly Pushdown Languages, Applications of VPLs, Queries on XML documents, Infinitary words, Buchi's theorem; MSO over finite words: Labeled words, Examples of MSO formulae corresponding to properties over finite words (inequality between positions, last position of a word, languages such as a^+b^*); MSO over finite words is equivalent to regular languages: Intuition of proof, Construction of MSO formula from an automaton, Inductive construction of a regular language from an MSO formula by expanding the alphabet to include interpretation of quantified variables; Formal definition of MSO over finite labeled words, Formal statement of theorem, Proof of forward direction: given an MSO formula, inductively construct a regular language, Expanding the alphabet to contain both position labels and interpretations of quantified FO and MSO variables
WT Chapter 3, Section 3.1Continuing presentation of equivalence between MSO over finite words and regular languages; Recap of proof of forward direction; Formal proof of reverse direction: given an automaton, construct an MSO formula that captures the same language; View of automata as a monadic labeling on word positions with local constraints over word positions; Construction of MSO formula representing the monadic labeling given a DFA: existentially quantified second-order variables representing labels on word positions, universally quantified first-order variables to express local constraints over word positions; Ramifications: Satisfiability/validity of MSO formulae over finite words is decidable, MSO Model Checking is decidable; MONA tool to convert formulas to automata; Generalization to trees, Bottom-up tree automata (BUTA), Top-down tree automata (NTDTA), BUTA=NTDTA MSO over trees is equivalent to tree-regular languages, Proof intuition using properties of tree automata: closure under union, intersection, complement, and projection; Generalization to omega words (infinite words), Büchi automata, Büchi acceptance condition on omega words (final states appear 'infinitely often'), MSO over infinite words is equivalent to omega-regular languages, Applications to LTL model checking; Generalization to omega trees, MSO over omega trees is decidable, Rabin automata, Müller automata, Müller acceptance condition, Parity condition, Partiy games and the memerbship problem of parity automata; Applications of tree automata in synthesis, Church's synthesis problem
WT Chapters 3, 5, and 6Proving theorems in FOL and FOL+lfp using definition unfolding (a.k.a quantifier instantiation) and SMT solving
Final words on applications of logic and course recap; Program verification, pre/post conditions, Hoare triple, loop invariants, verification condiiton (VC) generation; Symbolic testing/symbolic evaluation, application of logic to symbolic testing, test input generation, concolic testing; Interpretation of one structure in another, interpreting integers with addition in natural numbers with addition, interpreting rational numbers in natural numbers (with addition and multiplication), general presentation of interpretation, Courcelle's theorem, interpreting MSO over graphs of bounded treewidth over the tree decomposition; Recap of topics and important results covered in the course