Disproving confluence of term rewriting systems by interpretation and ordering

Takahito Aoto

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

7 Citations (Scopus)

Abstract

In order to disprove confluence of term rewriting systems, we develop new criteria for ensuring non-joinability of terms based on interpretation and ordering. We present some instances of the criteria which are amenable for automation, and report on an implementation of a confluence disproving procedure based on these instances. The experiments reveal that our method is successfully applied to automatically disprove confluence of some term rewriting systems, on which state-of-the-art automated confluence provers fail. A key idea to make our method effective is the introduction of usable rules - this allows one to decompose the constraint on rewrite rules into smaller components that depend on starting terms.

Original languageEnglish
Title of host publicationFrontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings
Pages311-326
Number of pages16
DOIs
Publication statusPublished - 2013 Nov 6
Event9th International Symposium on Frontiers of Combining Systems, FroCoS 2013 - Nancy, France
Duration: 2013 Sep 182013 Sep 20

Publication series

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

Other

Other9th International Symposium on Frontiers of Combining Systems, FroCoS 2013
CountryFrance
CityNancy
Period13/9/1813/9/20

Keywords

  • Confluence
  • Interpretation
  • Non-Joinability
  • Ordering
  • Term Rewriting Systems

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Disproving confluence of term rewriting systems by interpretation and ordering'. Together they form a unique fingerprint.

  • Cite this

    Aoto, T. (2013). Disproving confluence of term rewriting systems by interpretation and ordering. In Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings (pp. 311-326). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8152 LNAI). https://doi.org/10.1007/978-3-642-40885-4_22