Proving confluence of term rewriting systems automatically

Takahito Aoto, Junichi Yoshida, Yoshihito Toyama

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

46 Citations (Scopus)


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 languageEnglish
Title of host publicationRewriting Techniques and Applications - 20th International Conference, RTA 2009, Proceedings
Number of pages10
Publication statusPublished - 2009
Externally publishedYes
Event20th International Conference on Rewriting Techniques and Applications, RTA 2009 - Brasilia, Brazil
Duration: 2009 Jun 292009 Jul 1

Publication series

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


Other20th International Conference on Rewriting Techniques and Applications, RTA 2009

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Proving confluence of term rewriting systems automatically'. Together they form a unique fingerprint.

Cite this