Skip to main content

The Complexity of Deciding Whether Ordering is Necessary in a Presburger Formula


Christoph Haase

Suitable for

Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C


It has been shown in [1] that the sets of integers definable in the first-order theory of the integers with addition and order, FO(Z,+,<=), is a strict superset of those sets of integers definable when only equality instead of order is allowed (i.e. those definable in FO(Z,+,=)). The goal of this project is to determine the computational complexity of deciding whether a given sentence of FO(Z,+,<=) is definable in FO(Z,+,=).

[1] C. Choffrut and A. Frigeri. Deciding whether the ordering is necessary in a Presburger formula. Discrete Mathematics and Theoretical Computer Science, 12(1):20–37, 2010.  URL