The First-Order Theory of Lexicographic Path Orderings is Undecidable
(pdf)
Hubert Comon, Ralf Treinen
Theoretical Computer Science
Ordering Constraints on Trees
(pdf)
Hubert Comon, Ralf Treinen
Colloquium on Trees in Algebra and Programming