# On the Combination of the Bernays-Sch\"onfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic

## TL;DR

This paper demonstrates that extending the Bernays-Schönfinkel-Ramsey fragment with a restricted form of linear integer arithmetic remains decidable through finite ground instantiation, reducing the search space for automated reasoning.

## Contribution

It introduces a decidability result for a fragment combining Bernays-Schönfinkel-Ramsey with restricted linear integer arithmetic, enabling more efficient automated reasoning.

## Key findings

- Decidability is achieved via finite ground instantiation.
- Fewer instances are needed for reasoning about array data structures.
- Reduces the search space in automated reasoning procedures.

## 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.