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?
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 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].
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.
Springer-Verlag.
- [CCD93]
-
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.
- [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 first-order theory of lexicographic path orderings is
undecidable.
Theoretical Computer
Science, 176(1–2):67–87, April 1997.
- [JO91]
-
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.
- [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.