THE FIRST-ORDER THEORY OF LEXICOGRAPHIC PATH ORDERINGS IS UNDECIDABLE

Authors
COMON H TREINEN R
Citation
H. Comon et R. Treinen, THE FIRST-ORDER THEORY OF LEXICOGRAPHIC PATH ORDERINGS IS UNDECIDABLE, Theoretical computer science, 176(1-2), 1997, pp. 67-87
Citations number
15
Categorie Soggetti
Computer Sciences","Computer Science Theory & Methods
Journal title
Theoretical computer science → ACNP
ISSN journal
03043975
Volume
176
Issue
1-2
Year of publication
1997
Pages
67 - 87
Database
ISI
SICI code
0304-3975(1997)176:1-2<67:TFTOLP>2.0.ZU;2-D
Abstract
We show, under some assumption on the signature, that the There Exists For All* fragment of the theory of a lexicographic path ordering is u ndecidable, both in the partial and in the total precedence cases. Our result implies in particular that the simplification rule of ordered completion is undecidable.