Using linear arithmetic procedure for generating induction schemes

Deepak Kapur, Mahadevan Subramaniam

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

1 Citation (Scopus)

Abstract

Inspired by Boyer and Moore’s approach for generating induction schemes based on terminating function definitions, Zhang, Kapur and Krishnamoorthy introduced a cover set method for designing induction schemes for automating proofs by induction from specifications expressed as equations and conditional equations. This method has been implemented in the theorem prover Rewrite Rule Laboratory (RRL) and a proof management system Tecton built on top of RRL, and it has been used to prove many nontrivial theorems and reason about sequential as well as parallel programs. The cover set method is based on the assumption that a function symbol is defined using a finite set of terminating (conditional or unconditional) rewrite rules. The left side of the rules are used to design different cases of an induction scheme, and recursive calls to the function made in the right side can be used to design appropriate instantiations for generating induction hypotheses. A weakness of this method is that it relies on syntactic unification for generating an induction scheme for a conjecture. This paper goes a step further by proposing semantic analysis for generating an induction scheme for a conjecture from a cover set. The use of a decision procedure for Pres-burger arithmetic (quantifier-free theory of numbers with the addition operation and relational predicates >, <, ≠, =, ≥, ≤) is discussed for performing semantic analysis about numbers. The focus in this paper is on the use of the decision procedure for generating appropriate induction schemes from a conjecture and cover sets. This extension of the cover set method automates proofs of many theorems which otherwise, require human guidance and hints. The effectiveness of the method is demonstrated using simple examples which commonly arise in reasoning about specifications and programs. It is shown how semantic analysis using a Presburger arithmetic decision procedure can be used for checking the completeness of a cover set of a function defined using operations such as + and — on numbers. Using this check, the completeness of many function definitions used in a proof of the prime factorization theorem stating that every number can be factored uniquely into prime factors, which had to be checked manually, can now be checked automatically in RRL.

Original languageEnglish (US)
Title of host publicationFoundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings
PublisherSpringer Verlag
Pages438-449
Number of pages12
Volume880 LNCS
ISBN (Print)9783540587156
StatePublished - 1994
Externally publishedYes
Event14th Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1994 - Madras, India
Duration: Dec 15 1994Dec 17 1994

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume880 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other14th Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1994
CountryIndia
CityMadras
Period12/15/9412/17/94

Fingerprint

Set Cover
Proof by induction
Semantic Analysis
Semantics
Decision Procedures
Specifications
Completeness
Syntactics
Factorization
Theorem
Specification
L'Hôpital's Rule
Factorization Theorem
Prime factor
Parallel Programs
Quantifiers
Unification
Predicate
Guidance
Finite Set

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kapur, D., & Subramaniam, M. (1994). Using linear arithmetic procedure for generating induction schemes. In Foundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings (Vol. 880 LNCS, pp. 438-449). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 880 LNCS). Springer Verlag.

Using linear arithmetic procedure for generating induction schemes. / Kapur, Deepak; Subramaniam, Mahadevan.

Foundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings. Vol. 880 LNCS Springer Verlag, 1994. p. 438-449 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 880 LNCS).

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

Kapur, D & Subramaniam, M 1994, Using linear arithmetic procedure for generating induction schemes. in Foundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings. vol. 880 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 880 LNCS, Springer Verlag, pp. 438-449, 14th Conference on Foundations of Software Technology and Theoretical Computer Science, FST and TCS 1994, Madras, India, 12/15/94.
Kapur D, Subramaniam M. Using linear arithmetic procedure for generating induction schemes. In Foundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings. Vol. 880 LNCS. Springer Verlag. 1994. p. 438-449. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Kapur, Deepak ; Subramaniam, Mahadevan. / Using linear arithmetic procedure for generating induction schemes. Foundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings. Vol. 880 LNCS Springer Verlag, 1994. pp. 438-449 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{22fde6fcccf24a169d61d6e528a999f7,
title = "Using linear arithmetic procedure for generating induction schemes",
abstract = "Inspired by Boyer and Moore’s approach for generating induction schemes based on terminating function definitions, Zhang, Kapur and Krishnamoorthy introduced a cover set method for designing induction schemes for automating proofs by induction from specifications expressed as equations and conditional equations. This method has been implemented in the theorem prover Rewrite Rule Laboratory (RRL) and a proof management system Tecton built on top of RRL, and it has been used to prove many nontrivial theorems and reason about sequential as well as parallel programs. The cover set method is based on the assumption that a function symbol is defined using a finite set of terminating (conditional or unconditional) rewrite rules. The left side of the rules are used to design different cases of an induction scheme, and recursive calls to the function made in the right side can be used to design appropriate instantiations for generating induction hypotheses. A weakness of this method is that it relies on syntactic unification for generating an induction scheme for a conjecture. This paper goes a step further by proposing semantic analysis for generating an induction scheme for a conjecture from a cover set. The use of a decision procedure for Pres-burger arithmetic (quantifier-free theory of numbers with the addition operation and relational predicates >, <, ≠, =, ≥, ≤) is discussed for performing semantic analysis about numbers. The focus in this paper is on the use of the decision procedure for generating appropriate induction schemes from a conjecture and cover sets. This extension of the cover set method automates proofs of many theorems which otherwise, require human guidance and hints. The effectiveness of the method is demonstrated using simple examples which commonly arise in reasoning about specifications and programs. It is shown how semantic analysis using a Presburger arithmetic decision procedure can be used for checking the completeness of a cover set of a function defined using operations such as + and — on numbers. Using this check, the completeness of many function definitions used in a proof of the prime factorization theorem stating that every number can be factored uniquely into prime factors, which had to be checked manually, can now be checked automatically in RRL.",
author = "Deepak Kapur and Mahadevan Subramaniam",
year = "1994",
language = "English (US)",
isbn = "9783540587156",
volume = "880 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "438--449",
booktitle = "Foundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Using linear arithmetic procedure for generating induction schemes

AU - Kapur, Deepak

AU - Subramaniam, Mahadevan

PY - 1994

Y1 - 1994

N2 - Inspired by Boyer and Moore’s approach for generating induction schemes based on terminating function definitions, Zhang, Kapur and Krishnamoorthy introduced a cover set method for designing induction schemes for automating proofs by induction from specifications expressed as equations and conditional equations. This method has been implemented in the theorem prover Rewrite Rule Laboratory (RRL) and a proof management system Tecton built on top of RRL, and it has been used to prove many nontrivial theorems and reason about sequential as well as parallel programs. The cover set method is based on the assumption that a function symbol is defined using a finite set of terminating (conditional or unconditional) rewrite rules. The left side of the rules are used to design different cases of an induction scheme, and recursive calls to the function made in the right side can be used to design appropriate instantiations for generating induction hypotheses. A weakness of this method is that it relies on syntactic unification for generating an induction scheme for a conjecture. This paper goes a step further by proposing semantic analysis for generating an induction scheme for a conjecture from a cover set. The use of a decision procedure for Pres-burger arithmetic (quantifier-free theory of numbers with the addition operation and relational predicates >, <, ≠, =, ≥, ≤) is discussed for performing semantic analysis about numbers. The focus in this paper is on the use of the decision procedure for generating appropriate induction schemes from a conjecture and cover sets. This extension of the cover set method automates proofs of many theorems which otherwise, require human guidance and hints. The effectiveness of the method is demonstrated using simple examples which commonly arise in reasoning about specifications and programs. It is shown how semantic analysis using a Presburger arithmetic decision procedure can be used for checking the completeness of a cover set of a function defined using operations such as + and — on numbers. Using this check, the completeness of many function definitions used in a proof of the prime factorization theorem stating that every number can be factored uniquely into prime factors, which had to be checked manually, can now be checked automatically in RRL.

AB - Inspired by Boyer and Moore’s approach for generating induction schemes based on terminating function definitions, Zhang, Kapur and Krishnamoorthy introduced a cover set method for designing induction schemes for automating proofs by induction from specifications expressed as equations and conditional equations. This method has been implemented in the theorem prover Rewrite Rule Laboratory (RRL) and a proof management system Tecton built on top of RRL, and it has been used to prove many nontrivial theorems and reason about sequential as well as parallel programs. The cover set method is based on the assumption that a function symbol is defined using a finite set of terminating (conditional or unconditional) rewrite rules. The left side of the rules are used to design different cases of an induction scheme, and recursive calls to the function made in the right side can be used to design appropriate instantiations for generating induction hypotheses. A weakness of this method is that it relies on syntactic unification for generating an induction scheme for a conjecture. This paper goes a step further by proposing semantic analysis for generating an induction scheme for a conjecture from a cover set. The use of a decision procedure for Pres-burger arithmetic (quantifier-free theory of numbers with the addition operation and relational predicates >, <, ≠, =, ≥, ≤) is discussed for performing semantic analysis about numbers. The focus in this paper is on the use of the decision procedure for generating appropriate induction schemes from a conjecture and cover sets. This extension of the cover set method automates proofs of many theorems which otherwise, require human guidance and hints. The effectiveness of the method is demonstrated using simple examples which commonly arise in reasoning about specifications and programs. It is shown how semantic analysis using a Presburger arithmetic decision procedure can be used for checking the completeness of a cover set of a function defined using operations such as + and — on numbers. Using this check, the completeness of many function definitions used in a proof of the prime factorization theorem stating that every number can be factored uniquely into prime factors, which had to be checked manually, can now be checked automatically in RRL.

UR - http://www.scopus.com/inward/record.url?scp=85000624417&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85000624417&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9783540587156

VL - 880 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 438

EP - 449

BT - Foundations of Software Technology and Theoretical Computer Science - 14th Conference, 1994, Proceedings

PB - Springer Verlag

ER -