Logic and Mechanized Reasoning

Contents:

• 1. Introduction
  • 1.1. Historical background
  • 1.2. An overview of this course
• 2. Mathematical Background
  • 2.1. Induction and recursion on the natural numbers
  • 2.2. Complete induction
  • 2.3. Generalized induction and recursion
  • 2.4. Invariants
  • 2.5. Exercises
• 3. Lean as a Programming Language
  • 3.1. About Lean
  • 3.2. Using Lean as a functional programming language
  • 3.3. Inductive data types in Lean
  • 3.4. Using Lean as an imperative programming language
  • 3.5. Exercises
• 4. Propositional Logic
  • 4.1. Syntax
  • 4.2. Semantics
  • 4.3. Calculating with propositions
  • 4.4. Complete sets of connectives
  • 4.5. Normal forms
  • 4.6. Exercises
• 5. Implementing Propositional Logic
  • 5.1. Syntax
  • 5.2. Semantics
  • 5.3. Normal Forms
  • 5.4. Exercises
• 6. Decision Procedures for Propositional Logic
  • 6.1. The Tseitin transformation
  • 6.2. Unit propagation and the pure literal rule
  • 6.3. DPLL
  • 6.4. Autarkies and 2-SAT
  • 6.5. CDCL
  • 6.6. Exercises
• 7. Using SAT Solvers
  • 7.1. First examples
  • 7.2. Encoding problems
  • 7.3. Exercise: grid coloring
  • 7.4. Exercise: NumberMind
• 8. Proof Systems for Propositional Logic
  • 8.1. Axiomatic systems
  • 8.2. Resolution
  • 8.3. Implementing resolution
  • 8.4. Resolution and DPLL
  • 8.5. A sequent calculus
  • 8.6. Natural deduction
  • 8.7. Compactness
  • 8.8. Exercises
• 9. Using Lean as a Proof Assistant
  • 9.1. Propositional logic
  • 9.2. Proof terms
  • 9.3. Structured proofs
  • 9.4. Equational reasoning
  • 9.5. Induction
  • 9.6. Exercises
• 10. First-Order Logic
  • 10.1. Syntax
  • 10.2. Using first-order logic
  • 10.3. Semantics
  • 10.4. Normal forms
• 11. Implementing First-Order Logic
  • 11.1. Terms
  • 11.2. Evaluating terms
  • 11.3. Formulas
  • 11.4. Unification
• 12. Decision Procedures for First-Order Logic
  • 12.1. Equality
  • 12.2. Implementing congruence closure
  • 12.3. Deciding universal sentences
  • 12.4. Linear arithmetic
  • 12.5. Implementing Fourier-Motzkin
  • 12.6. A full decision procedure
  • 12.7. Other theories
• 13. Using SMT solvers
  • 13.1. SMT-LIB Format
  • 13.2. Example: Magic squares
  • 13.3. Calling SMT solvers from Lean
  • 13.4. Application: Verification
  • 13.5. Exercise: Almost squares
• 14. Proof Systems for First-Order Logic
  • 14.1. Resolution
  • 14.2. Completeness of resolution
  • 14.3. Skolemization
  • 14.4. Adding equality
  • 14.5. Axiomatic proof systems
  • 14.6. A sequent calculus
  • 14.7. Natural deduction
• 15. Using First-Order Theorem Provers
  • 15.1. Example: Aunt Agatha
  • 15.2. Example: The Eighth Asylum
  • 15.3. Exercise: The Last Asylum
• 16. Beyond First-Order Logic
  • 16.1. Sorts
  • 16.2. Function types
  • 16.3. Higher-order logic
  • 16.4. Inductive Types
  • 16.5. Dependent Types