The Complexity of Deciding Whether Ordering is Necessary in a Presburger Formula
AbstractIt has been shown in  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,+,=).
 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 https://www.dmtcs.org/dmtcs-ojs/index.php/dmtcs/article/view/1300/0.html.