Proving confluence of term rewriting systems automatically

Takahito Aoto; Junichi Yoshida; Yoshihito Toyama

doi:10.1007/978-3-642-02348-4_7

Proving confluence of term rewriting systems automatically

Takahito Aoto, Junichi Yoshida, Yoshihito Toyama

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

42 Citations (Scopus)

Abstract

We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown.

Original language	English
Title of host publication	Rewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings
Pages	93-102
Number of pages	10
DOIs	https://doi.org/10.1007/978-3-642-02348-4_7
Publication status	Published - 2009
Externally published	Yes
Event	20th International Conference on Rewriting Techniques and Applications, RTA 2009 - Brasilia, Brazil Duration: 2009 Jun 29 → 2009 Jul 1

Publication series

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

Other

Other	20th International Conference on Rewriting Techniques and Applications, RTA 2009
Country/Territory	Brazil
City	Brasilia
Period	09/6/29 → 09/7/1

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-642-02348-4_7

Cite this

Aoto, T., Yoshida, J., & Toyama, Y. (2009). Proving confluence of term rewriting systems automatically. In Rewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings (pp. 93-102). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5595 LNCS). https://doi.org/10.1007/978-3-642-02348-4_7

Proving confluence of term rewriting systems automatically. / Aoto, Takahito; Yoshida, Junichi; Toyama, Yoshihito.

Rewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings. 2009. p. 93-102 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5595 LNCS).

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

Aoto, T, Yoshida, J & Toyama, Y 2009, Proving confluence of term rewriting systems automatically. in Rewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5595 LNCS, pp. 93-102, 20th International Conference on Rewriting Techniques and Applications, RTA 2009, Brasilia, Brazil, 09/6/29. https://doi.org/10.1007/978-3-642-02348-4_7

Aoto T, Yoshida J, Toyama Y. Proving confluence of term rewriting systems automatically. In Rewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings. 2009. p. 93-102. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-02348-4_7

@inproceedings{000a511c79ee47e9b42a3a054c1bf9d6,

title = "Proving confluence of term rewriting systems automatically",

abstract = "We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown.",

author = "Takahito Aoto and Junichi Yoshida and Yoshihito Toyama",

year = "2009",

doi = "10.1007/978-3-642-02348-4_7",

language = "English",

isbn = "3642023479",

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

pages = "93--102",

booktitle = "Rewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings",

note = "20th International Conference on Rewriting Techniques and Applications, RTA 2009 ; Conference date: 29-06-2009 Through 01-07-2009",

}

TY - GEN

T1 - Proving confluence of term rewriting systems automatically

AU - Aoto, Takahito

AU - Yoshida, Junichi

AU - Toyama, Yoshihito

PY - 2009

Y1 - 2009

N2 - We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown.

AB - We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown.

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

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

U2 - 10.1007/978-3-642-02348-4_7

DO - 10.1007/978-3-642-02348-4_7

M3 - Conference contribution

AN - SCOPUS:70350649118

SN - 3642023479

SN - 9783642023477

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

SP - 93

EP - 102

BT - Rewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings

T2 - 20th International Conference on Rewriting Techniques and Applications, RTA 2009

Y2 - 29 June 2009 through 1 July 2009

ER -

Proving confluence of term rewriting systems automatically

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this