Skip to Main content Skip to Navigation
Other publications

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 metadata
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Monday, December 7, 2015 - 5:27:21 PM
Last modification on : Saturday, October 16, 2021 - 11:26:05 AM

Links full text


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



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



Les métriques sont temporairement indisponibles