Bernays-Schoenfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
Abstract
First-order predicate logic extended with linear arithmetic is undecidable, in general. We show that the Bernays-Sch\"onfinkel-Ramsey (BSR) fragment extended with linear arithmetic restricted to simple bounds (SB) is decidable through finite ground instantiation. The identified ground instances can be employed to restrict the search space of existing automated reasoning procedures for BSR(SB). Satisfiability of BSR(SB) compared to BSR remains NEXPTIME-complete. The decidability result is almost tight because BSR is undecidable if extended with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.
Keywords
Cite
@article{arxiv.1501.07209,
title = {Bernays-Schoenfinkel-Ramsey with Simple Bounds is NEXPTIME-complete},
author = {Marco Voigt and Christoph Weidenbach},
journal= {arXiv preprint arXiv:1501.07209},
year = {2020}
}
Comments
This is a revised version of the initial arXiv submission. Although submitted in 2020, the last update of its contents dates back to June 2015