文章基本信息

标题：On the Power of Ordering in Linear Arithmetic Theories
本地全文：下载
作者：Dmitry Chistikov ; Christoph Haase
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：168
页码：119:1-119:15
DOI：10.4230/LIPIcs.ICALP.2020.119
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We study the problems of deciding whether a relation definable by a first-order formula in linear rational or linear integer arithmetic with an order relation is definable in absence of the order relation. Over the integers, this problem was shown decidable by Choffrut and Frigeri [Discret. Math. Theor. C., 12(1), pp. 21 - 38, 2010], albeit with non-elementary time complexity. Our contribution is to establish a full geometric characterisation of those sets definable without order which in turn enables us to prove coNP-completeness of this problem over the rationals and to establish an elementary upper bound over the integers. We also provide a complementary Î â,,^P lower bound for the integer case that holds even in a fixed dimension. This lower bound is obtained by showing that universality for ultimately periodic sets, i.e., semilinear sets in dimension one, is Î â,,^P-hard, which resolves an open problem of Huynh [Elektron. Inf.verarb. Kybern., 18(6), pp. 291 - 338, 1982].
关键词：logical definability; linear arithmetic theories; semi linear sets; ultimately periodic sets; numerical semigroups