Automated confluence proof by decreasing diagrams based on rule-labelling

Takahito Aoto

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

13 Citations (Scopus)

Abstract

Decreasing diagrams technique (van Oostrom, 1994) is a technique that can be widely applied to prove confluence of rewrite systems. To directly apply the decreasing diagrams technique to prove confluence of rewrite systems, rule-labelling heuristic has been proposed by van Oostrom (2008). We show how constraints for ensuring confluence of term rewriting systems constructed based on the rule-labelling heuristic are encoded as linear arithmetic constraints suitable for solving the satisfiability of them by external SMT solvers. We point out an additional constraint omitted in (van Oostrom, 2008) that is needed to guarantee the soundness of confluence proofs based on the rule-labelling heuristic extended to deal with non-right-linear rules. We also present several extensions of the rule-labelling heuristic by which the applicability of the technique is enlarged.

Original languageEnglish
Title of host publicationProceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010
Pages7-16
Number of pages10
Publication statusPublished - 2010 Dec 1
Event21st International Conference on Rewriting Techniques and Applications, RTA 2010 - Edinburgh, United Kingdom
Duration: 2010 Jul 112010 Jul 13

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume6
ISSN (Print)1868-8969

Other

Other21st International Conference on Rewriting Techniques and Applications, RTA 2010
Country/TerritoryUnited Kingdom
CityEdinburgh
Period10/7/1110/7/13

Keywords

  • Automation
  • Confluence
  • Decreasing diagrams
  • Term rewriting systems

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Automated confluence proof by decreasing diagrams based on rule-labelling'. Together they form a unique fingerprint.

Cite this