### 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(s_{1}; ⋯ ; s_{m}) → r, where s_{1}; ⋯ ; s_{m} 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(x_{1}; ⋯ x_{m}) = 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) |
---|---|

Title of host publication | Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings |

Editors | David McAllester |

Publisher | Springer Verlag |

Pages | 324-345 |

Number of pages | 22 |

ISBN (Electronic) | 3540676643, 9783540676645 |

State | Published - Jan 1 2000 |

Event | 17th International Conference on Automated Deduction, CADE 2000 - Pittsburgh, United States Duration: Jun 17 2000 → Jun 20 2000 |

### Publication series

Name | Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) |
---|---|

Volume | 1831 |

ISSN (Print) | 0302-9743 |

### Other

Other | 17th International Conference on Automated Deduction, CADE 2000 |
---|---|

Country | United States |

City | Pittsburgh |

Period | 6/17/00 → 6/20/00 |

### Fingerprint

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings*(pp. 324-345). (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science); Vol. 1831). Springer Verlag.

**Extending decision procedures with induction schemes.** / Kapur, Deepak; Subramaniam, Mahadevan.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings.*Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science), vol. 1831, Springer Verlag, pp. 324-345, 17th International Conference on Automated Deduction, CADE 2000, Pittsburgh, United States, 6/17/00.

}

TY - GEN

T1 - Extending decision procedures with induction schemes

AU - Kapur, Deepak

AU - Subramaniam, Mahadevan

PY - 2000/1/1

Y1 - 2000/1/1

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

M3 - Conference contribution

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

ER -