The Lean Theorem Prover (System Description).
Leonardo Mendonça de MouraSoonho KongJeremy AvigadFloris van DoornJakob von RaumerPublished in: CADE (2015)
Keyphrases
- theorem prover
- theorem proving
- automated theorem proving
- first order logic
- automated reasoning
- term rewriting
- formal proof
- inference rules
- computer algebra
- automated deduction
- high level
- formal semantics
- higher order logic
- natural deduction
- mathematical knowledge
- timed automata
- propositional logic
- desirable properties
- logic programming