hide
Free keywords:
Computer Science, Logic in Computer Science, cs.LO
Abstract:
In general, first-order predicate logic extended with linear integer
arithmetic is undecidable. We show that the Bernays-Sch\"onfinkel-Ramsey
fragment ($\exists^* \forall^*$-sentences) extended with a restricted form of
linear integer arithmetic is decidable via finite ground instantiation. The
identified ground instances can be employed to restrict the search space of
existing automated reasoning procedures considerably, e.g., when reasoning
about quantified properties of array data structures formalized in Bradley,
Manna, and Sipma's array property fragment. Typically, decision procedures for
the array property fragment are based on an exhaustive instantiation of
universally quantified array indices with all the ground index terms that occur
in the formula at hand. Our results reveal that one can get along with
significantly fewer instances.
