Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers.
Lawrence C. PaulsonJasmin Christian BlanchettePublished in: IWIL@LPAR (2010)
Keyphrases
- theorem prover
- computer algebra systems
- theorem proving
- term rewriting
- first order logic
- computer algebra
- automated theorem proving
- automated reasoning
- automated deduction
- fully automatic
- inference rules
- years ago
- experience gained
- semi automatic
- natural deduction
- formal semantics
- real world
- machine learning
- immersive environments
- computer graphics