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.
https://hal.inria.fr/hal-00990437
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s
<>
Soumis le : mardi 13 mai 2014 - 15:36:55
Dernière modification le : vendredi 4 janvier 2019 - 17:32:57
Document(s) archivé(s) le : lundi 10 avril 2017 - 22:10:22
Christian Choffrut, Achille Frigeri. Deciding whether the ordering is necessary in a Presburger formula. Discrete Mathematics and Theoretical Computer Science, DMTCS, 2010, 12 (1), pp.20-37. 〈hal-00990437〉
