For theorem provers to be effective as well as acceptable for use in applications, it is essential that properties considered trivial and obvious by domain experts are proved automatically without any user guidance. To make theorem provers such as Rewrite Rule Laboratory (RRL), a rewrite-based induction prover, more effective, it is important that decision procedures for well-known data structures and representations frequently used in many application domains be integrated efficiently with rewriting and induction. Using the example of the quantifier-free subtheory of Presburger arithmetic, requirements for integration of rewriting and induction with decision procedures are discussed. It is shown how a decision procedure can be used for generating appropriate instantiations of definitions and lemmas, suggesting induction schemes which exploit semantic information, and speculating intermediate lemmas needed to prove theorems.
Sufficient conditions are identified for deciding a priori, the validity of a family of equational conjectures expressed using function symbols that are recursively defined over the terms of a decidable theory. These conjectures can be decided only using induction. The concept of a theory-based function definition is introduced. Conditions on conjectures and interaction among the definitions of functions appearing in them that guarantee the simplification of each induction subgoal to a formula in the decidable theory are identified. It is shown that the cover set method which implements inductive reasoning in RRL can be used as a decision procedure for such conjectures.