Dealing with non-orientable equations in rewriting induction

Takahito Aoto

doi:10.1007/11805618_18

Dealing with non-orientable equations in rewriting induction

Takahito Aoto

Systems & Software Division

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

18 Citations (Scopus)

Abstract

Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order. Thus, when the given conjecture is not orientable by the reduction order in use, any proof attempts for that conjecture fails; also conjectures such as a commutativity equation are out of the scope of the rewriting induction because they can not be oriented by any reduction order. In this paper, we give an enhanced rewriting induction which can deal with non-orientable conjectures. We also present an extension which intends an incremental use of our enhanced rewriting induction.

Original language	English
Title of host publication	Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings
Publisher	Springer Verlag
Pages	242-256
Number of pages	15
ISBN (Print)	3540368345, 9783540368342
DOIs	https://doi.org/10.1007/11805618_18
Publication status	Published - 2006 Jan 1
Event	17th International Conference on Term Rewriting and Applications, RTA 2006 - Seattle, WA, United States Duration: 2006 Aug 12 → 2006 Aug 14

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4098 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	17th International Conference on Term Rewriting and Applications, RTA 2006
Country/Territory	United States
City	Seattle, WA
Period	06/8/12 → 06/8/14

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/11805618_18

Cite this

Aoto, T. (2006). Dealing with non-orientable equations in rewriting induction. In Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings (pp. 242-256). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4098 LNCS). Springer Verlag. https://doi.org/10.1007/11805618_18

Dealing with non-orientable equations in rewriting induction. / Aoto, Takahito.

Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings. Springer Verlag, 2006. p. 242-256 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4098 LNCS).

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

Aoto, T 2006, Dealing with non-orientable equations in rewriting induction. in Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4098 LNCS, Springer Verlag, pp. 242-256, 17th International Conference on Term Rewriting and Applications, RTA 2006, Seattle, WA, United States, 06/8/12. https://doi.org/10.1007/11805618_18

@inproceedings{4a39e3c1516a4462b434a34687a4c9bd,

title = "Dealing with non-orientable equations in rewriting induction",

abstract = "Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order. Thus, when the given conjecture is not orientable by the reduction order in use, any proof attempts for that conjecture fails; also conjectures such as a commutativity equation are out of the scope of the rewriting induction because they can not be oriented by any reduction order. In this paper, we give an enhanced rewriting induction which can deal with non-orientable conjectures. We also present an extension which intends an incremental use of our enhanced rewriting induction.",

author = "Takahito Aoto",

year = "2006",

month = jan,

day = "1",

doi = "10.1007/11805618_18",

language = "English",

isbn = "3540368345",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "242--256",

booktitle = "Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings",

note = "17th International Conference on Term Rewriting and Applications, RTA 2006 ; Conference date: 12-08-2006 Through 14-08-2006",

}

TY - GEN

T1 - Dealing with non-orientable equations in rewriting induction

AU - Aoto, Takahito

PY - 2006/1/1

Y1 - 2006/1/1

N2 - Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order. Thus, when the given conjecture is not orientable by the reduction order in use, any proof attempts for that conjecture fails; also conjectures such as a commutativity equation are out of the scope of the rewriting induction because they can not be oriented by any reduction order. In this paper, we give an enhanced rewriting induction which can deal with non-orientable conjectures. We also present an extension which intends an incremental use of our enhanced rewriting induction.

AB - Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order. Thus, when the given conjecture is not orientable by the reduction order in use, any proof attempts for that conjecture fails; also conjectures such as a commutativity equation are out of the scope of the rewriting induction because they can not be oriented by any reduction order. In this paper, we give an enhanced rewriting induction which can deal with non-orientable conjectures. We also present an extension which intends an incremental use of our enhanced rewriting induction.

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

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

U2 - 10.1007/11805618_18

DO - 10.1007/11805618_18

M3 - Conference contribution

AN - SCOPUS:33749402649

SN - 3540368345

SN - 9783540368342

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

SP - 242

EP - 256

BT - Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings

PB - Springer Verlag

T2 - 17th International Conference on Term Rewriting and Applications, RTA 2006

Y2 - 12 August 2006 through 14 August 2006

ER -

Dealing with non-orientable equations in rewriting induction

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this