Automatic verification of non-recursive algorithm of Hanoi Tower by using Isabelle Theorem Prover.
Huazhen XuZhen YouJinyun XuePublished in: SNPD (2016)
Keyphrases
- theorem prover
- recursive algorithm
- hypothesis testing
- term rewriting
- theorem proving
- upper bound
- first order logic
- automated theorem proving
- natural deduction
- inference rules
- computer algebra
- formal proof
- proof search
- formal semantics
- minimum mean square error
- convex hull
- boolean algebra
- expert systems
- propositional logic
- proof planning
- high dimensional