UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

On the power of ordering in linear arithmetic theories

Chistikov, D; Haase, C; (2020) On the power of ordering in linear arithmetic theories. In: Proceedings of the 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). (pp. p. 119). Leibniz International Proceedings in Informatics, LIPIcs: Saarbrücken, Germany (Virtual Conference). Green open access

[thumbnail of Haase_LIPIcs-ICALP-2020-119.pdf]
Preview
Text
Haase_LIPIcs-ICALP-2020-119.pdf - Published Version

Download (758kB) | Preview

Abstract

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].

Type: Proceedings paper
Title: On the power of ordering in linear arithmetic theories
Event: 47th International Colloquium on Automata, Languages and Programming (ICALP 2020)
Open access status: An open access version is available from UCL Discovery
DOI: 10.4230/LIPIcs.ICALP.2020.119
Publisher version: https://doi.org/10.4230/LIPIcs.ICALP.2020.119
Language: English
Additional information: This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/3.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10096878
Downloads since deposit
42Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item