Skip to Main content Skip to Navigation
Journal articles

Deciding whether the ordering is necessary in a Presburger formula

Abstract : We characterize the relations which are first-order definable in the model of the group of integers with the constant 1. This allows us to show that given a relation defined by a first-order formula in this model enriched with the usual ordering, it is recursively decidable whether or not it is first-order definable without the ordering.
Document type :
Journal articles
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-00990437
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s Connect in order to contact the contributor
Submitted on : Tuesday, May 13, 2014 - 3:36:55 PM
Last modification on : Saturday, November 20, 2021 - 3:49:30 AM
Long-term archiving on: : Monday, April 10, 2017 - 10:10:22 PM

File

1300-4872-1-PB.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Christian Choffrut, Achille Frigeri. Deciding whether the ordering is necessary in a Presburger formula. Discrete Mathematics and Theoretical Computer Science, DMTCS, 2010, Vol. 12 no. 1 (1), pp.20-37. ⟨10.46298/dmtcs.510⟩. ⟨hal-00990437⟩

Share

Metrics

Record views

49

Files downloads

689