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.
Type de document :
Article dans une revue
Discrete Mathematics and Theoretical Computer Science, DMTCS, 2010, 12 (1), pp.20-37
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

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 : jeudi 11 janvier 2018 - 06:17:42
Document(s) archivé(s) le : lundi 10 avril 2017 - 22:10:22

Fichier

1300-4872-1-PB.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00990437, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

78

Téléchargements de fichiers

279