# Extending decision procedures with induction schemes

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations

## Abstract

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.

Original language English (US) Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings David McAllester Springer Verlag 324-345 22 3540676643, 9783540676645 https://doi.org/10.1007/10721959_26 Published - 2000 17th International Conference on Automated Deduction, CADE 2000 - Pittsburgh, United StatesDuration: Jun 17 2000 → Jun 20 2000

### Publication series

Name Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) 1831 0302-9743

### Other

Other 17th International Conference on Automated Deduction, CADE 2000 United States Pittsburgh 6/17/00 → 6/20/00

## ASJC Scopus subject areas

• Theoretical Computer Science
• Computer Science(all)