[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:

• membership in a fixed regular tree language
• a predicate expressing that a fixed symbol does not occur in a term.

References

[Com90]

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.

[Nie93]

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]