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. Deduction for Propositional Logic
- 9. Propositional Logic in Lean
- 10. First-Order Logic
- 11. Implementing First-Order Logic
- 12. Decision Procedures for First-Order Logic
- 13. Using SMT solvers
- 14. Deduction for First-Order Logic
- 15. Using First-Order Theorem Provers
- 16. First-Order Logic in Lean
- 17. Beyond First-Order Logic