Logic and Mechanized Reasoning

Contents:

• 1. Introduction
  • 1.1. Historical background
  • 1.2. An overview of this course
  • 1.3. Acknowledgments
• 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. Deduction for Propositional Logic
  • 8.1. Axiomatic systems
  • 8.2. A sequent calculus
  • 8.3. Resolution
  • 8.4. Natural deduction
  • 8.5. Compactness
  • 8.6. Exercises
• 9. Propositional Logic in Lean
  • 9.1. Implication
  • 9.2. Conjunction
  • 9.3. Disjunction
  • 9.4. Negation
  • 9.5. Miscellany
  • 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. Linear arithmetic
  • 12.2. Linear integer arithmetic
  • 12.3. Equality
• 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. Deduction for First-Order Logic
  • 14.1. Axiomatic systems
  • 14.2. A sequent calculus
  • 14.3. Resolution
  • 14.4. 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. First-Order Logic in Lean
  • 16.1. Quantifiers
  • 16.2. Equational reasoning
  • 16.3. Structural induction
• 17. Beyond First-Order Logic
  • 17.1. Sorts
  • 17.2. Function types
  • 17.3. Higher-order logic
  • 17.4. Inductive Types
  • 17.5. Dependent Types