New uses of linear arithmetic in automated theorem proving by induction |
| |
Authors: | Deepak Kapur M Subramaniam |
| |
Affiliation: | (1) Computer Science Department, State University of New York, 12222 Albany, NY, U.S.A. |
| |
Abstract: | 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 by 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 sides of the rules are used to design different cases of an induction sheme, 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 >, <, ≠, =, ⩾, ⩽) for performing semantic analysis about numbers. The decision procedure is used
to generate appropriate induction schemes for a conjecture by using cover sets of function taking numbers as arguments. This
extension of the cover set method automates proofs of many theorems that otherwise require human guidance and hints. The effectiveness
of the method is demonstrated by using some examples that 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 by using operations such as + and — on numbers. With 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, an 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.
Partially supported by the National Science Foundation Grant No. CCR-9303394 and subcontract CB0249 of SRI contract MDA904-92-C-5186
with The Maryland Procurement Office. |
| |
Keywords: | Induction automated theorem proving heuristics linear arithmetic Presburger arithmetic generalization semantic unification |
本文献已被 SpringerLink 等数据库收录! |
|