THE FIRST-ORDER THEORY OF LEXICOGRAPHIC PATH ORDERINGS IS UNDECIDABLE

摘要

We show, under some assumption on the signature, that the There Exists*For All* fragment of the theory of a lexicographic path ordering is undecidable, both in the partial and in the total precedence cases. Our result implies in particular that the simplification rule of ordered completion is undecidable. [References: 15]