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
»
Index
Index