LIPIcs.ICALP.2020.119.pdf
- Filesize: 0.72 MB
- 15 pages
Document
On the Power of Ordering in Linear Arithmetic Theories
Authors
Dmitry Chistikov 
,
Christoph Haase
-
Part of:
Volume:
47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Colloquium on Automata, Languages, and Programming (ICALP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-06-29
File
Document Identifiers
Author Details
- Centre for Discrete Mathematics and its Applications (DIMAP) & Department of Computer Science, University of Warwick, Coventry, UK
Cite AsGet BibTex
Dmitry Chistikov and Christoph Haase. On the Power of Ordering in Linear Arithmetic Theories. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 119:1-119:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ICALP.2020.119
https://doi.org/10.4230/LIPIcs.ICALP.2020.119
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].
Subject Classification
ACM Subject Classification
- Theory of computation → Automated reasoning
Keywords
- logical definability
- linear arithmetic theories
- semi linear sets
- ultimately periodic sets
- numerical semigroups
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- B. Boigelot, I. Mainz, V. Marsault, and M. Rigo. An efficient algorithm to decide periodicity of b-recognisable sets using MSDF convention. In International Colloquium on Automata, Languages, and Programming, ICALP, volume 80 of LIPIcs, pages 118:1-118:14, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2017.118.
- D. Chistikov and C. Haase. The taming of the semi-linear set. In International Colloquium on Automata, Languages, and Programming, ICALP, volume 55 of LIPIcs, pages 128:1-128:13, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.128.
- D. Chistikov and C. Haase. On the complexity of quantified integer programming. In International Colloquium on Automata, Languages, and Programming, ICALP, volume 80 of LIPIcs, pages 94:1-94:13, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2017.94.
- D. Chistikov, C. Haase, and S. Halfon. Context-free commutative grammars with integer counters and resets. Theor. Comput. Sci., 735:147-161, 2018. URL: http://dx.doi.org/10.1016/j.tcs.2016.06.017.
- C. Choffrut and A. Frigeri. Deciding whether the ordering is necessary in a Presburger formula. Discret. Math. Theor. C., 12(1):21-38, 2010. URL: http://dmtcs.episciences.org/510.
- S. Ginsburg and E.H. Spanier. Bounded ALGOL-like languages. T. Am. Math. Soc., pages 333-368, 1964. URL: http://dx.doi.org/10.2307/1994067.
- F.W. Glover and R.E.D. Woolsey. Aggregating diophantine equations. Zeitschr. für OR, 16(1):1-10, 1972. URL: http://dx.doi.org/10.1007/BF01917186.
-
T.-D. Huynh. The complexity of semilinear sets. Elektron. Inf.verarb. Kybern., 18(6):291-338, 1982.
- J. Leroux. A polynomial time Presburger criterion and synthesis for number decision diagrams. In Symposium on Logic in Computer Science, LICS, pages 147-156, 2005. URL: http://dx.doi.org/10.1109/LICS.2005.2.
- A.A. Muchnik. The definable criterion for definability in Presburger arithmetic and its applications. Theor. Comput. Sci., 290(3):1433-1444, 2003. URL: http://dx.doi.org/10.1016/S0304-3975(02)00047-6.
- R. Parikh. On context-free languages. J. ACM, 13(4):570-581, 1966. URL: http://dx.doi.org/10.1145/321356.321364.
-
M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I congres de Mathematiciens des Pays Slaves, pages 92-101. Warszawa, 1929.
- J. Robinson. Definability and decision problems in arithmetic. J. Symb. Log., 14(2):98-114, 1949. URL: http://dx.doi.org/10.2307/2266510.
-
A. Ronquist. A lower bound on the complexity of real addition without order. Master’s thesis, University of Oxford, United Kingdom, 2019.
-
A. Schrijver. Theory of linear and integer programming. John Wiley & Sons, 1986.
- H.U. Simon. On the containment problem for linear sets. In Symposium on Theoretical Aspects of Computer Science, STACS, volume 96 of LIPIcs, pages 55:1-55:12, 2018. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2018.55.
- J. von zur Gathen and M. Sieveking. A bound on solutions of linear integer equalities and inequalities. P. Am. Math. Soc., 72(1):155-158, 1978. URL: http://dx.doi.org/10.1090/S0002-9939-1978-0500555-0.