Problem #24
Originator: JeanPierre Jouannaud
Date: April 1991
Summary:
Is satisfiability of lpo or rpo ordering constraints decidable in case of
nontotal precedences?
The existential fragment of the firstorder 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?
Remark
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 firstorder 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 firstorder theory of encompassment (the
instanceofsubterm relation) is decidable [CCD93]. The
satisfiability problem for the existential fragment in the total case is
NPcomplete [Nie93].
Though the firstorder theory of encompassment is decidable [CCD93],
the firstorder (Σ_{2}) theory of the recursive (lexicographic status)
path ordering, assuming certain simple conditions on the precedence, is not
[CT97].
References

[BC93]

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.
SpringerVerlag.
 [CCD93]

AnneCécile Caron, JeanLuc 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.
SpringerVerlag.
 [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.
 [CT97]

Hubert Comon and Ralf Treinen.
The firstorder theory of lexicographic path orderings is
undecidable.
Theoretical Computer
Science, 176(1–2):67–87, April 1997.
 [JO91]

JeanPierre 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.
SpringerVerlag.
 [Nie93]

Robert Nieuwenhuis.
Simple LPO constraint solving methods.
Information Processing Letters, 47:65–69, 1993.
 [Tre92]

Ralf Treinen.
A new method for undecidability proofs of first order theories.
Journal of Symbolic
Computation, 14(5):437–458, November 1992.
 [Ven87]

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.