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 First-Order Logic
13. Using SMT solvers
14. Proof Systems for First-Order Logic
15. Using First-Order Theorem Provers
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
Logic and Mechanized Reasoning
»
16.
Beyond First-Order Logic
View page source
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