[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Nachum Dershowitz, Jean-Pierre Jouannaud
Date: April 1991
Summary: Is there a set of inference rules that always succeeds in computing a convergent set of rewrite rules for a given set of equations and an ordering, provided that it exists?
Ordered rewriting computes a given convergent set of rewrite rules for an equational theory E and an ordering > whenever such a set R exists for >, provided > can be made total on ground terms. Unfortunately, this is not always possible, even if > is derivability (→_{R}^{+}) in R. Is there a set of inference rules that will always succeed in computing R whenever R exists for >?
A proposal appears in [Dev91]; more work is called for.
A positive answer has been given in [BGNR99].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |