Extending decision procedures with induction schemes

Deepak Kapur, Mahadevan Subramaniam

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

14 Citations (Scopus)

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 languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings
EditorsDavid McAllester
PublisherSpringer Verlag
Pages324-345
Number of pages22
ISBN (Electronic)3540676643, 9783540676645
StatePublished - Jan 1 2000
Event17th International Conference on Automated Deduction, CADE 2000 - Pittsburgh, United States
Duration: Jun 17 2000Jun 20 2000

Publication series

NameLecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
Volume1831
ISSN (Print)0302-9743

Other

Other17th International Conference on Automated Deduction, CADE 2000
CountryUnited States
CityPittsburgh
Period6/17/006/20/00

Fingerprint

Decision Procedures
Proof by induction
Quantifiers
Syntactics
Byproducts
Term
Arithmetic Circuits
Set Cover
Networks (circuits)
Compatibility
Congruence
Finite Set
Lemma
Correctness
Calculus
Closure
Heuristics
Distinct
Predict

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kapur, D., & Subramaniam, M. (2000). Extending decision procedures with induction schemes. In D. McAllester (Ed.), 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.

Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. ed. / David McAllester. Springer Verlag, 2000. p. 324-345 (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science); Vol. 1831).

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

Kapur, D & Subramaniam, M 2000, Extending decision procedures with induction schemes. in D McAllester (ed.), 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.
Kapur D, Subramaniam M. Extending decision procedures with induction schemes. In McAllester D, editor, Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. Springer Verlag. 2000. p. 324-345. (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)).
Kapur, Deepak ; Subramaniam, Mahadevan. / Extending decision procedures with induction schemes. Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. editor / David McAllester. Springer Verlag, 2000. pp. 324-345 (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)).
@inproceedings{f27ff69154084fd2a7bee7710ddb6a9a,
title = "Extending decision procedures with induction schemes",
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.",
author = "Deepak Kapur and Mahadevan Subramaniam",
year = "2000",
month = "1",
day = "1",
language = "English (US)",
series = "Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)",
publisher = "Springer Verlag",
pages = "324--345",
editor = "David McAllester",
booktitle = "Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings",

}

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 -