Deciding whether the ordering is necessary in a Presburger formulaArticle
Authors: Christian Choffrut 1; Achille Frigeri 1,2
NULL##NULL
Christian Choffrut;Achille Frigeri
- 1 Laboratoire d'informatique Algorithmique : Fondements et Applications
- 2 Dipartimento di Matematica, "Francesco Brioschi"
Automata, Logic and Semantics
[en]
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.
Volume: Vol. 12 no. 1
Section: Automata, Logic and Semantics
Published on: January 1, 2010
Imported on: March 26, 2015
Keywords: [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], [en] Presburger arithmetics