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 |
Type: | Text |
Language: | English |
URI: | http://hdl.handle.net/2142/12311 |
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 |