Publikation

The First-Order Theory of Lexicographic Path Orderings is Undecidable

Hubert Comon, Ralf Treinen

DFKI DFKI Research Reports (RR) 93-42 1993.

Abstrakt

We show, under some assumption on the signature, that the ∀* ∃* fragment of the theory of any lexicographic path ordering is undecidable. This applies to partial and to total precedences. Our result implies in particular that the simplification rule of ordered completion is undecidable.

RR-93-42.pdf (pdf, 15 MB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence