Item

Abstract

First-order linear real arithmetic enriched with uninterpreted predicate
symbols yields an interesting modeling language. However, satisfiability of
such formulas is undecidable, even if we restrict the uninterpreted predicate
symbols to arity one. In order to find decidable fragments of this language, it
is necessary to restrict the expressiveness of the arithmetic part. One
possible path is to confine arithmetic expressions to difference constraints of
the form $x - y \mathrel{\#} c$, where $\#$ ranges over the standard relations
$<, \leq, =, \neq, \geq, >$ and $x,y$ are universally quantified. However, it
is known that combining difference constraints with uninterpreted predicate
symbols yields an undecidable satisfiability problem again. In this paper, it
is shown that satisfiability becomes decidable if we in addition bound the
ranges of universally quantified variables. As bounded intervals over the reals
still comprise infinitely many values, a trivial instantiation procedure is not
sufficient to solve the problem.