A Pragmatic Approach to Equality Reasoning
Christoph Walther · TUbilio (Technical University of Darmstadt) · 2006
We report about a first-order theorem prover which is imple- mented in the interactive verification toolX eriFun to prove the base and step cases of an induction proof. The use in an interactive environment requires at erminating system providing as atisfying balance between theorem proving power and runtime performance as well as the supply of results being useful for carrying on with a proof attempt (by some user interaction, say) if a proof cannot be found. The latter requirement is particularly important because non-valid formulas are frequently en- countered when proving theorems by induction. Our prover is based on symbolic evaluation, i.e. a method which combines symbolic execution of programs with techniques from classical theorem proving and term rewriting. We illustrate how to integrate the use of lemmas and induc- tion hypotheses into symbolic evaluation and discuss the incorporation of equality reasoning in particular. We call our approach pragmatic be- cause no interesting formal qualities (except soundness) can be assigned to it, but it successfully performs when runningX eriFun to prove state- ments about programs.