[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #89

Originator: Hubert Comon, Robert Nieuwenhuis
Date: January 1998

Summary: Is the satisfiablity of ordering constraints (lpo) in conjunction with predicates like irreducibility by a fixed rewrite system or membership in a regular tree language decidable?

Satisfiability of ordering constraints (lpo) for total precedences has been shown decidable in [Com90, Nie93]. Is the satisfiablity of total lpo ordering constraints together with the constraint Irr(x), expressing that x is not reducible by some fixed rewrite system, decidable? This would imply decidability of the confluence of ordered rewriting (see Problem #64).

Besides the irreducibility predicate the following related predicates are of interest:


Hubert Comon. Solving inequations in term algebras (Preliminary version). In John C. Mitchell, editor, Fifth Symposium on Logic in Computer Science, pages 62–69, Philadelphia, PA, June 1990. IEEE.
Robert Nieuwenhuis. Simple LPO constraint solving methods. Information Processing Letters, 47:65–69, 1993.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]