Christian Choffrut ; Achille Frigeri - Deciding whether the ordering is necessary in a Presburger formula

dmtcs:510 - Discrete Mathematics & Theoretical Computer Science, January 1, 2010, Vol. 12 no. 1 - https://doi.org/10.46298/dmtcs.510
Deciding whether the ordering is necessary in a Presburger formula

Authors: Christian Choffrut 1; Achille Frigeri 1,2

  • 1 Laboratoire d'informatique Algorithmique : Fondements et Applications
  • 2 Dipartimento di Matematica, "Francesco Brioschi"

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://doi.org/10.46298/dmtcs.510
Source: HAL:hal-00990437v1
Volume: Vol. 12 no. 1
Section: Automata, Logic and Semantics
Published on: January 1, 2010
Imported on: March 26, 2015
Keywords: Presburger arithmetics,[INFO.INFO-DM] Computer Science [cs]/Discrete Mathematics [cs.DM]

Linked publications - datasets - softwares

Source : ScholeXplorer IsRelatedTo DOI 10.1145/236869.237084
  • 10.1145/236869.237084
Near optimal algorithms for computing Smith normal forms of integer matrices

Share and export

Consultation statistics

This page has been seen 294 times.
This article's PDF has been downloaded 231 times.