Calculation by tactic in theorem proving
Bing Li, Jian Zhang, Wei Su, Lian Li · Lanzhou University Institutional Repository · 2012
We illustrate a proof in a theorem proving system can be used not only to show the correctness of a given proposition but also as a calculator to perform symbolic calculation by giving out two case studies under Isabelle/HOL. Through simulating an imperative language, we show this method can be used to realizing various algorithms. Tactics which are designed to construct such proofs can be used to realize automatic theorem proving and fill the gap between the proof in textbook mathematic text and that in a theorem proving system.