Deepak Kapur and M. Subramaniam

Zhang, Kapur and Krishnamoorthy introduced a cover set method for designing
induction schemes for automating proofs by induction from
specifications expressed as equations and conditional equations.
This method has been implemented in the theorem prover
* Rewrite Rule Laboratory* (* RRL*) and a proof management
system * Tecton* built on top of * RRL,* and it has been
used to prove many nontrivial theorems and reason about
sequential as well as parallel programs. The cover set method is
based on the assumption that a function symbol is defined using a
finite set of terminating (conditional or unconditional) rewrite
rules. The termination ordering employed in orienting the rules is used
to perform proofs by well-founded induction. The left side of the rules are
used to design different cases of an induction scheme, and recursive calls to
the function made in the right side can be used to design appropriate
instantiations for generating induction hypotheses. A weakness of this method
is that it relies on syntactic unification for generating an induction scheme
for a conjecture. This paper goes a step further by proposing semantic
analysis for generating an induction scheme for a conjecture from a cover set.
We discuss the use of a decision procedure for Presburger arithmetic
(quantifier-free theory of numbers with the addition operation
and relational predicates >, <, not =, >=, <=) for performing
semantic analysis about numbers. The decision procedure is used to
generate appropriate induction schemes for a conjecture
using cover sets of function taking numbers as arguments.
This extension of the cover set method automates proofs of many theorems
which otherwise, require human guidance and hints. The effectiveness of
the method is demonstrated using some examples which commonly arise in
reasoning about specifications and programs. It is also shown how semantic
analysis using a Presburger arithmetic decision procedure can be used for
checking the completeness of a cover set of a function defined
using operations such as + and - on numbers. Using this check, many function definitions
used in a proof of the prime factorization theorem stating that every number
can be factored uniquely into prime factors, which had to be checked manually,
can now be checked automatically in * RRL*. The use of the decision
procedure for guiding generalization for generating conjectures and merging
induction schemes is also illustrated.