Logic and Mechanized Reasoning

Contents:

  • 1. Introduction
  • 2. Mathematical Background
  • 3. Lean as a Programming Language
  • 4. Propositional Logic
  • 5. Implementing Propositional Logic
  • 6. Decision Procedures for Propositional Logic
  • 7. Using SAT Solvers
  • 8. Proof Systems for Propositional Logic
  • 9. Using Lean as a Proof Assistant
  • 10. First-Order Logic
  • 11. Implementing First-Order Logic
  • 12. Decision Procedures for Equality
  • 13. Equality and Induction in Lean
  • 14. Decision Procedures for Arithmetic
  • 15. Using SMT solvers
  • 16. Proof Systems for First-Order Logic
  • 17. Using First-Order Theorem Provers
  • 18. Beyond First-Order Logic
Logic and Mechanized Reasoning
  • »
  • Search

© Copyright 2021, Jeremy Avigad, Marijn J. H. Heule, and Wojciech Nawrocki.

Built with Sphinx using a theme provided by Read the Docs.