Proving confluence of term rewriting systems via persistency and decreasing diagrams

Takahito Aoto, Yoshihito Toyama, Kazumasa Uchida

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

2 Citations (Scopus)

Abstract

The decreasing diagrams technique (van Oostrom, 1994) has been successfully used to prove confluence of rewrite systems in various ways; using rule-labelling (van Oostrom, 2008), it can also be applied directly to prove confluence of some linear term rewriting systems (TRSs) automatically. Some efforts for extending the rule-labelling are known, but non-left-linear TRSs are left beyond the scope. Two methods for automatically proving confluence of non-(left-)linear TRSs with the rule-labelling are given. The key idea of our methods is to combine the decreasing diagrams technique with persistency of confluence (Aoto & Toyama, 1997).

Original languageEnglish
Title of host publicationRewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer-Verlag
Pages46-60
Number of pages15
ISBN (Print)9783319089171
DOIs
Publication statusPublished - 2014 Jan 1
Event25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: 2014 Jul 142014 Jul 17

Publication series

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

Other

Other25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
CountryAustria
CityVienna
Period14/7/1414/7/17

Keywords

  • Confluence
  • Decreasing Diagrams
  • Non-Linear
  • Persistency
  • Rule- Labelling
  • Term Rewriting Systems

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Proving confluence of term rewriting systems via persistency and decreasing diagrams'. Together they form a unique fingerprint.

Cite this