New uses of linear arithmetic in automated theorem proving by induction

Deepak Kapur, M. Subramaniam

Research output: Contribution to journalArticle

20 Citations (Scopus)

Abstract

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 by using a finite set of terminating (conditional or unconditional) rewrite rules. The termination ordering employed in orienting the rules is used to perform proofs by well-founded induction. The left sides 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. We discuss the use of a decision procedure for Presburger arithmetic (quantifier-free theory of numbers with the addition operation and relational predicates >, <, ≠, =, ≥, ≤) for performing semantic analysis about numbers. The decision procedure is used to generate appropriate induction schemes for a conjecture by using cover sets of function taking numbers as arguments. This extension of the cover set method automates proofs of many theorems that otherwise require human guidance and hints. The effectiveness of the method is demonstrated by using some examples that commonly arise in reasoning about specifications and programs. It is also 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 by using operations such as + and - on numbers. With this check, 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. The use of the decision procedure for guiding generalization for generating conjectures and merging induction schemes is also illustrated.

Original languageEnglish (US)
Pages (from-to)39-78
Number of pages40
JournalJournal of Automated Reasoning
Volume16
Issue number1-2
DOIs
StatePublished - Jan 1 1996

Fingerprint

Theorem proving
Semantics
Specifications
Syntactics
Factorization
Merging

Keywords

  • Automated theorem proving
  • Generalization
  • Heuristics
  • Induction
  • Linear arithmetic
  • Presburger arithmetic
  • Semantic unification

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Cite this

New uses of linear arithmetic in automated theorem proving by induction. / Kapur, Deepak; Subramaniam, M.

In: Journal of Automated Reasoning, Vol. 16, No. 1-2, 01.01.1996, p. 39-78.

Research output: Contribution to journalArticle

@article{a2e845161b66451e9e6bdd2533809f1e,
title = "New uses of linear arithmetic in automated theorem proving by induction",
abstract = "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 by using a finite set of terminating (conditional or unconditional) rewrite rules. The termination ordering employed in orienting the rules is used to perform proofs by well-founded induction. The left sides 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. We discuss the use of a decision procedure for Presburger arithmetic (quantifier-free theory of numbers with the addition operation and relational predicates >, <, ≠, =, ≥, ≤) for performing semantic analysis about numbers. The decision procedure is used to generate appropriate induction schemes for a conjecture by using cover sets of function taking numbers as arguments. This extension of the cover set method automates proofs of many theorems that otherwise require human guidance and hints. The effectiveness of the method is demonstrated by using some examples that commonly arise in reasoning about specifications and programs. It is also 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 by using operations such as + and - on numbers. With this check, 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. The use of the decision procedure for guiding generalization for generating conjectures and merging induction schemes is also illustrated.",
keywords = "Automated theorem proving, Generalization, Heuristics, Induction, Linear arithmetic, Presburger arithmetic, Semantic unification",
author = "Deepak Kapur and M. Subramaniam",
year = "1996",
month = "1",
day = "1",
doi = "10.1007/BF00244459",
language = "English (US)",
volume = "16",
pages = "39--78",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "1-2",

}

TY - JOUR

T1 - New uses of linear arithmetic in automated theorem proving by induction

AU - Kapur, Deepak

AU - Subramaniam, M.

PY - 1996/1/1

Y1 - 1996/1/1

N2 - 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 by using a finite set of terminating (conditional or unconditional) rewrite rules. The termination ordering employed in orienting the rules is used to perform proofs by well-founded induction. The left sides 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. We discuss the use of a decision procedure for Presburger arithmetic (quantifier-free theory of numbers with the addition operation and relational predicates >, <, ≠, =, ≥, ≤) for performing semantic analysis about numbers. The decision procedure is used to generate appropriate induction schemes for a conjecture by using cover sets of function taking numbers as arguments. This extension of the cover set method automates proofs of many theorems that otherwise require human guidance and hints. The effectiveness of the method is demonstrated by using some examples that commonly arise in reasoning about specifications and programs. It is also 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 by using operations such as + and - on numbers. With this check, 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. The use of the decision procedure for guiding generalization for generating conjectures and merging induction schemes is also illustrated.

AB - 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 by using a finite set of terminating (conditional or unconditional) rewrite rules. The termination ordering employed in orienting the rules is used to perform proofs by well-founded induction. The left sides 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. We discuss the use of a decision procedure for Presburger arithmetic (quantifier-free theory of numbers with the addition operation and relational predicates >, <, ≠, =, ≥, ≤) for performing semantic analysis about numbers. The decision procedure is used to generate appropriate induction schemes for a conjecture by using cover sets of function taking numbers as arguments. This extension of the cover set method automates proofs of many theorems that otherwise require human guidance and hints. The effectiveness of the method is demonstrated by using some examples that commonly arise in reasoning about specifications and programs. It is also 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 by using operations such as + and - on numbers. With this check, 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. The use of the decision procedure for guiding generalization for generating conjectures and merging induction schemes is also illustrated.

KW - Automated theorem proving

KW - Generalization

KW - Heuristics

KW - Induction

KW - Linear arithmetic

KW - Presburger arithmetic

KW - Semantic unification

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

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

U2 - 10.1007/BF00244459

DO - 10.1007/BF00244459

M3 - Article

AN - SCOPUS:0030101018

VL - 16

SP - 39

EP - 78

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 1-2

ER -