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

Marco Voigt (1) , Christoph Weidenbach (1, 2)

1 MPII - Max-Planck-Institut für Informatik
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems

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.

Domaines: Logique en informatique [cs.LO]

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