Termination modulo combinations of equational theories

Francisco Durán, Salvador Lucas, José Meseguer

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


Rewriting with rules R modulo axioms E is a widely used technique in both rule-based programming languages and in automated deduction. Termination methods for rewriting systems modulo specific axioms E (e.g., associativity- commutativity) are known. However, much less seems to be known about termination methods that can be modular in the set E of axioms. In fact, current termination tools and proof methods cannot be applied to commonly occurring combinations of axioms that fall outside their scope. This work proposes a modular termination proof method based on semantics- and termination-preserving transformations that can reduce the proof of termination of rules R modulo E to an equivalent proof of termination of the transformed rules modulo a typically much simpler set B of axioms. Our method is based on the notion of variants of a term recently proposed by Comon and Delaune. We illustrate its practical usefulness by considering the very common case in which E is an arbitrary combination of associativity, commutativity, left- and right-identity axioms for various function symbols.

Original languageEnglish (US)
Title of host publicationFrontiers of Combining Systems - 7th International Symposium, FroCoS 2009, Proceedings
Number of pages17
StatePublished - 2009
Event7th International Symposium on Frontiers of Combining Systems, FroCoS 2009 - Trento, Italy
Duration: Sep 16 2009Sep 18 2009

Publication series

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


Other7th International Symposium on Frontiers of Combining Systems, FroCoS 2009

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Termination modulo combinations of equational theories'. Together they form a unique fingerprint.

Cite this