[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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:
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |