hide
Free keywords:
Computer Science, Logic in Computer Science, cs.LO,Computer Science, Computational Complexity, cs.CC
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.