The first-order theory of lexicographic path orderings is undecidable

被引：10
|
作者：
Comon, H
Treinen, R
机构：
[1] UNIV PARIS 11, CNRS, F-91405 ORSAY, FRANCE
[2] UNIV PARIS 11, LRI, F-91405 ORSAY, FRANCE
[3] GERMAN RES CTR ARTIFICIAL INTELLIGENCE DKFI, D-66123 SAARBRUCKEN, GERMANY
来源：
THEORETICAL COMPUTER SCIENCE | 1997年 / 176卷 / 1-2期
关键词：
D O I：
10.1016/S0304-3975(96)00049-7
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：67 / 87
页数：21
相关论文
共 50 条
12345