@online{VoigtWeidenbacharXiv2015,
TITLE = {Bernays-Sch{\"o}nfinkel-Ramsey with Simple Bounds is {NEXPTIME}-complete},
AUTHOR = {Voigt, Marco and Weidenbach, Christoph},
URL = {http://arxiv.org/abs/1501.07209},
EPRINT = {1501.07209},
EPRINTTYPE = {arXiv},
YEAR = {2015},
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\"onfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Sch\"onfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.},
}