Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete

Marco Voigt 1 Christoph Weidenbach 1, 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Linear arithmetic extended with free predicate symbols is undecidable, in general. We show that the restriction of linear arithmetic inequations to simple bounds extended with the Bernays-Schönfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Schönfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.
Document type :
Other publications
Complete list of metadatas

https://hal.inria.fr/hal-01239399
Contributor : Stephan Merz <>
Submitted on : Monday, December 7, 2015 - 5:27:21 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM

Links full text

Identifiers

  • HAL Id : hal-01239399, version 1
  • ARXIV : 1501.07209

Collections

Citation

Marco Voigt, Christoph Weidenbach. Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete. 2015. ⟨hal-01239399⟩

Share

Metrics

Record views

165