Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete - Archive ouverte HAL Access content directly
Other Publications Year : 2015

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

(1) , (1, 2)
1
2

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.

Dates and versions

hal-01239399 , version 1 (07-12-2015)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More