An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support
Ralph-Johan BackJohannes ErikssonPublished in: ThEdu (2011)
Keyphrases
- theorem prover
- first order logic
- theorem proving
- inference rules
- term rewriting
- formal proof
- programming language
- computer algebra systems
- automated theorem proving
- automated reasoning
- higher order logic
- desirable properties
- visual analytics
- mathematical knowledge
- support systems
- user interaction
- end users
- proof search
- active learning
- evolutionary algorithm
- search space