Technical Report CS0393

Title: Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems
Authors: S. Porat and N. Francez
Abstract: In [PF-85] the concepts of fair derivations and fair-termination in term-rewriting systems were introduced and studied. In this paper, we define the notion of fairness in equational terrn-rewriting systems, where a derivation step is a composition of the equality generated by a (finite) set of equations with one step rewriting using a set of rules. A natural generalization of .E-termination (termination of equational term-rewriting systems), namely E-fair-termination is presented. We show that fairtermination and E-fair-termination are the same whenever the underlying rewriting relation is E-fully-co mmuting, a propetty inspired by Jouannaud and Munoz' E-commutation property. We obtain anallogous results for combined term-rewriting systems.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 1986
To the main CS technical reports page

Computer science department, Technion