Files in this item



application/pdfduran-lucas-meseguer-termination-modulo.pdf (311kB)
(no description provided)PDF


Title:Termination Modulo Combinations of Equational Theories
Author(s):Duran, Francisco; Lucas, Salvador; Meseguer, José
Subject(s):term rewriting, termination, modularity
Abstract: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.
Issue Date:2009-06-19
Genre:Technical Report
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Sponsor:F. Dur ́an and S. Lucas were partially supported by Spanish MEC under grants TIN 2008-03107 and TIN 2007-68093-C02, respectively. J. Meseguer was partially supported by NSF Grants CNS 07-16638 and CNS 08-31064.
Date Available in IDEALS:2009-06-19

This item appears in the following Collection(s)

Item Statistics