TY - GEN
T1 - Extending decision procedures with induction schemes
AU - Kapur, Deepak
AU - Subramaniam, Mahadavan
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2000.
PY - 2000
Y1 - 2000
N2 - Families of function definitions and conjectures based in quantifier-free decidable theories are identified for which inductive va- lidity of conjectures can be decided by the cover set method, a heuristic implemented in a rewrite-based induction theorem prover Rewrite Rule Laboratory (RRL) for mechanizing induction. Conditions characterizing definitions and conjectures are syntactic, and can be easily checked, thus making it possible to determine a priori whether a given conjecture can be decided. The concept of a Τ-based function definition is introduced that consists of a finite set of terminating complete rewrite rules of the form f(s1; ⋯ ; sm) → r, where s1; ⋯ ; sm are interpreted terms from a decidable theory Τ , and r is either an interpreted term or has non- nested recursive calls to f with all other function symbols from Τ . Two kinds of conjectures are considered. Simple conjectures are of the form f(x1; ⋯ xm) = t, where f is Τ-based, xi's are distinct variables, and t is interpreted in Τ . Complex conjectures differ from simple conjectures in their left sides which may contain many function symbols whose defini- tions are Τ-based and the nested order in which these function symbols appear in the left sides have the compatibility property with their defini- tions. The main objective is to ensure that for each induction subgoal gener- ated from a conjecture after selecting an induction scheme, the resulting formula can be simplified so that induction hypothesis(es), whenever needed, is applicable, and the result of this application is a formula in T . Decidable theories considered are the quantifier-free theory of Pres- burger arithmetic, congruence closure on ground terms (with or with- out associative-commutative operators), propositional calculus, and the quantifier-free theory of constructors (mostly, free constructors as in the case of finite lists and finite sequences). A byproduct of the approach is that it can predict the structure of intermediate lemmas needed for au- tomatically deciding this subclass of conjectures. Several examples over lists, numbers and of properties involved in establishing the number- theoretic correctness of arithmetic circuits are given.
AB - Families of function definitions and conjectures based in quantifier-free decidable theories are identified for which inductive va- lidity of conjectures can be decided by the cover set method, a heuristic implemented in a rewrite-based induction theorem prover Rewrite Rule Laboratory (RRL) for mechanizing induction. Conditions characterizing definitions and conjectures are syntactic, and can be easily checked, thus making it possible to determine a priori whether a given conjecture can be decided. The concept of a Τ-based function definition is introduced that consists of a finite set of terminating complete rewrite rules of the form f(s1; ⋯ ; sm) → r, where s1; ⋯ ; sm are interpreted terms from a decidable theory Τ , and r is either an interpreted term or has non- nested recursive calls to f with all other function symbols from Τ . Two kinds of conjectures are considered. Simple conjectures are of the form f(x1; ⋯ xm) = t, where f is Τ-based, xi's are distinct variables, and t is interpreted in Τ . Complex conjectures differ from simple conjectures in their left sides which may contain many function symbols whose defini- tions are Τ-based and the nested order in which these function symbols appear in the left sides have the compatibility property with their defini- tions. The main objective is to ensure that for each induction subgoal gener- ated from a conjecture after selecting an induction scheme, the resulting formula can be simplified so that induction hypothesis(es), whenever needed, is applicable, and the result of this application is a formula in T . Decidable theories considered are the quantifier-free theory of Pres- burger arithmetic, congruence closure on ground terms (with or with- out associative-commutative operators), propositional calculus, and the quantifier-free theory of constructors (mostly, free constructors as in the case of finite lists and finite sequences). A byproduct of the approach is that it can predict the structure of intermediate lemmas needed for au- tomatically deciding this subclass of conjectures. Several examples over lists, numbers and of properties involved in establishing the number- theoretic correctness of arithmetic circuits are given.
UR - http://www.scopus.com/inward/record.url?scp=35248869003&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35248869003&partnerID=8YFLogxK
U2 - 10.1007/10721959_26
DO - 10.1007/10721959_26
M3 - Conference contribution
AN - SCOPUS:35248869003
T3 - Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
SP - 324
EP - 345
BT - Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings
A2 - McAllester, David
PB - Springer Verlag
T2 - 17th International Conference on Automated Deduction, CADE 2000
Y2 - 17 June 2000 through 20 June 2000
ER -