[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #34 (Solved !)

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 >?

Remark

A proposal appears in [Dev91]; more work is called for.

A positive answer has been given in [BGNR99].

References

[BGNR99]

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, and Albert Rubio. Paramodulation with non-monotonic orderings. In Fourteenth IEEE Annual Symposium on Logic in Computer Science, Trento, Italy, July 1999. IEEE.

[Dev91]

Hervé Devie. Une approche algébrique de la réécriture de preuves équationnelles et son application à la dérivation de procédures de complétion. PhD thesis, Université Paris-Sud, Orsay, France, October 1991.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]