@online{Voigt_arXIv1706.08504,
TITLE = {The {B}ernays--{S}ch{\"o}nfinkel--{R}amsey {Fragment with Bounded Difference Constraints over the Reals Is Decidable}},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1706.08504},
EPRINT = {1706.08504},
EPRINTTYPE = {arXiv},
YEAR = {2017},
ABSTRACT = {First-order linear real arithmetic enriched with uninterpreted predicate<br>symbols yields an interesting modeling language. However, satisfiability of<br>such formulas is undecidable, even if we restrict the uninterpreted predicate<br>symbols to arity one. In order to find decidable fragments of this language, it<br>is necessary to restrict the expressiveness of the arithmetic part. One<br>possible path is to confine arithmetic expressions to difference constraints of<br>the form $x -- y \mathrel{\#} c$, where $\#$ ranges over the standard relations<br>$<, \leq, =, \neq, \geq, >$ and $x,y$ are universally quantified. However, it<br>is known that combining difference constraints with uninterpreted predicate<br>symbols yields an undecidable satisfiability problem again. In this paper, it<br>is shown that satisfiability becomes decidable if we in addition bound the<br>ranges of universally quantified variables. As bounded intervals over the reals<br>still comprise infinitely many values, a trivial instantiation procedure is not<br>sufficient to solve the problem.<br>},
}