## 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 |

DOIs | |

State | Published - 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 |

## ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)