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

Problem #24

Originator: Jean-Pierre Jouannaud
Date: April 1991

Summary: Is satisfiability of lpo or rpo ordering constraints decidable in case of non-total precedences?

The existential fragment of the first-order theory of the “recursive path ordering” (with multiset and lexicographic “status”) is decidable when the precedence on function symbols is total [Com90, JO91], but is undecidable for arbitrary formulas. Is the existential fragment decidable for partial precedences?


The Σ4 (∃****) fragment is undecidable, in general [Tre92]. The positive existential fragment for the empty precedence (that is, for homeomorphic tree embedding) is decidable [BC93]. One might also ask whether the first-order theory of total recursive path orderings is decidable. Related results include the following: The existential fragment of the subterm ordering is decidable, but its Σ2 (∃**) fragment is not [Ven87]. The first-order theory of encompassment (the instance-of-subterm relation) is decidable [CCD93]. The satisfiability problem for the existential fragment in the total case is NP-complete [Nie93].

Though the first-order theory of encompassment is decidable [CCD93], the first-order (Σ2) theory of the recursive (lexicographic status) path ordering, assuming certain simple conditions on the precedence, is not [CT97].


Alexandre Boudet and Hubert Comon. About the theory of tree embedding. In M. C. Gaudel and J.-P. Jouannaud, editors, 4th International Joint Conference on Theory and Practice of Software Development, volume 668 of Lecture Notes in Computer Science, Orsay, France, April 1993. Springer-Verlag.
Anne-Cécile Caron, Jean-Luc Coquidé, and Max Dauchet. Encompassment properties and automata with constraints. In Claude Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, pages 328–342, Montreal, Canada, June 1993. Springer-Verlag.
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.
Hubert Comon and Ralf Treinen. The first-order theory of lexicographic path orderings is undecidable. Theoretical Computer Science, 176(1–2):67–87, April 1997.
Jean-Pierre Jouannaud and Mitsuhiro Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In J. Leach Albert, B. Monien, and M. Rodríguez Artalejo, editors, Proceedings of the Eighteenth EATCS Colloquium on Automata, Languages and Programming (Madrid, Spain), volume 510 of Lecture Notes in Computer Science, pages 455–468, Berlin, July 1991. Springer-Verlag.
Robert Nieuwenhuis. Simple LPO constraint solving methods. Information Processing Letters, 47:65–69, 1993.
Ralf Treinen. A new method for undecidability proofs of first order theories. Journal of Symbolic Computation, 14(5):437–458, November 1992.
K. N. Venkataraman. Decidability of the purely existential fragment of the theory of term algebras. J. of the Association for Computing Machinery, 34(2):492–510, 1987.

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