Matthias Horbach

Marco Voigt

Christoph Weidenbach

On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic

Keywords: Bernays-Schönfinkel-Ramsey fragment, Linear integer arithmetic, Complete instantiation

In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Schönfinkel-Ramsey fragment (∃ * ∀ * -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.

Introduction

The Bernays-Schönfinkel-Ramsey (BSR) fragment comprises exactly the firstorder logic prenex sentences with the ∃ * ∀ * quantifier prefix, resulting in a CNF where all occurring function symbols are constants. Formulas may contain equality. Satisfiability of the BSR fragment is decidable and NExpTime-complete [START_REF] Harry | Complexity Results for Classes of Quantificational Formulas[END_REF]. Its extension with linear arithmetic is undecidable [START_REF] Putnam | Decidability and Essential Undecidability[END_REF][START_REF] Peter | Undecidability of Presburger Arithmetic with a Single Monadic Predicate Letter[END_REF][START_REF] Joseph | Presburger Arithmetic with Unary Predicates is Π 1 1 Complete[END_REF][START_REF] Fietzke | Superposition as a Decision Procedure for Timed Automata[END_REF].

We prove decidability of the restriction to arithmetic constraints of the form s t, x t, where is one of the standard relations <, ≤, =, =, ≥, > and s, t are ground arithmetic terms, and x y, where stands for ≤, =, or ≥. Underlying the result is the observation that similar to the finite model property of BSR, only finitely many instances of universally quantified clauses with arithmetic constraints need to be considered. Our construction is motivated by results from quantifier elimination [START_REF] Loos | Applying Linear Quantifier Elimination[END_REF] and hierarchic superposition [START_REF] Bachmair | Refutational Theorem Proving for Hierarchic First-Order Theories[END_REF][START_REF] Althaus | Superposition Modulo Linear Arithmetic SUP(LA)[END_REF][START_REF] Kruglov | Superposition Decides the First-Order Logic Fragment Over Ground Theories[END_REF][START_REF] Fietzke | Superposition as a Decision Procedure for Timed Automata[END_REF][START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF]. In particular, the insights gained from the quantifier elimination side lead to instantiation methods that can result in significantly fewer instances than known, more naive approaches for comparable logic fragments generate, such as the original instantiation approach for the array property fragment [START_REF] Bradley | What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation[END_REF][START_REF] Bradley | Safety Analysis of Systems[END_REF]. For example, consider the following two clauses (∧ and ∨ bind stronger than →)

x 2 = 5 ∧ R(x 1 ) → Q(u 1 , x 2 ) y 1 < 7 ∧ y 2 ≤ 2 → Q(d, y 2 ) ∨ R(y 1 ) where the variable u 1 ranges over a freely selectable domain, x i , y i are variables over the integers, and the constant d addresses an element of the same domain that u 1 ranges over. All occurring variables are implicitly universally quantified. Our main result reveals that this clause set is satisfiable if and only if a finite set of ground instances is satisfiable in which (i) u 1 is being instantiated with the constant d, (ii) x 2 and y 2 are being instantiated with the (abstract) integer values 5 + 1 and -∞, and (iii) x 1 and y 1 are being instantiated with -∞ only. The instantiation does not need to consider the constraints y 1 < 7, y 2 ≤ 2, because it is sufficient to explore the integers either from -∞ upwards-in this case upper bounds on integer variables can be ignored-or from +∞ downwards-ignoring lower bounds-, as is similarly done in linear quantifier elimination over the reals [START_REF] Loos | Applying Linear Quantifier Elimination[END_REF]. Moreover, instantiation does not need to consider the value 5 + 1 for x 1 and y 1 , motivated by the fact that the argument x 1 of R is not affected by the constraint x 2 = 5.

The abstract values -∞ and +∞ are represented by Skolem constants over the integers, together with defining axioms. For the example, we introduce the fresh Skolem constant c -∞ to represent -∞ (a "sufficiently small" value) together with the axiom c -∞ < 2, where 2 is the smallest occurring constant. Eventually, we obtain the ground clause set 5

+ 1 = 5 ∧ R(c -∞ ) → Q(d, 5 + 1) c -∞ = 5 ∧ R(c -∞ ) → Q(d, c -∞ ) c -∞ < 7 ∧ 5 + 1 ≤ 2 → Q(d, 5 + 1) ∨ R(c -∞ ) c -∞ < 7 ∧ c -∞ ≤ 2 → Q(d, c -∞ ) ∨ R(c -∞ ) c -∞ < 2 which has the model A with c A -∞ = 1, R A = {1}, Q A = {(d, 6
), (d, 1)}. After developing our instantiation methodology in Section 3, we show in Sections 4 that our instantiation methods are also compatible with uninterpreted functions and additional background theories under certain syntactic restrictions. These results are based on an (un)satifiability-preserving embedding of uninterpreted functions into BSR clauses. There are interesting known logic fragments that fall into this syntactic category: many-sorted clause sets over stratified vocabularies [START_REF] Abadi | Decidable Fragments of Many-Sorted Logic[END_REF][START_REF] Korovin | Non-cyclic Sorts for First-Order Satisfiability[END_REF], the array property fragment [START_REF] Bradley | What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation[END_REF], and the finite essentially uninterpreted fragment, possibly extended with simple integer arithmetic [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF]. Consequently, reasoning procedures for these fragments that employ forms of instantiation may benefit from our findings. The paper ends with a discussion in Section 5, where we consider the impact of our results on automated reasoning procedures for our and similar logic fragments and outline possible further improvements.

Due to space limitations, we mostly resort to sketches of proofs. The interested reader is referred to the extended version of the present paper [START_REF] Horbach | On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic[END_REF].

Preliminaries

Hierarchic combinations of first-order logic with background theories build upon sorted logic with equality [START_REF] Bachmair | Refutational Theorem Proving for Hierarchic First-Order Theories[END_REF][START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF]. We instantiate this framework with the BSR fragment and linear arithmetic over the integers as the base theory. The base sort Z shall always be interpreted by the integers Z. For simplicity, we restrict our considerations to a single free sort S, which may be freely interpreted as some nonempty domain, as usual.

We denote by V Z a countably infinite set of base-sort variables. Linear integer arithmetic (LIA) terms are build from integer constants 0, 1, -1, 2, -2, . . ., the operators +, -, and the variables from V Z . We moreover allow base-sort constant symbols whose values have to be determined by an interpretation (Skolem constants). They can be conceived as existentially quantified. The LIA constraints we consider are of the form s t, where ∈ {<, ≤, =, =, ≥, >} and s and t are either LIA variables or ground LIA terms.

In order to hierarchically extend the base theory by the BSR fragment, we introduce the free sort S, a countably infinite set V S of free-sort variables, a finite set Ω of free (uninterpreted) constant symbols of sort S and a finite set Π of free predicate symbols equipped with sort information. Note that every predicate symbol in Π has a finite, nonnegative arity and can have a mixed sort over the two sorts Z and S, e.g. P : Z × S × Z. We use the symbol ≈ to denote the built-in equality predicate on S. To avoid confusion, we tacitly assume that no constant or predicate symbol is overloaded, i.e. they have a unique sort.

Definition 1 (BSR with Simple Linear Integer Constraints-BSR(SLI)).

A BSR(SLI) clause has the form Λ Γ → ∆, where Λ, Γ , ∆ are multisets of atoms satisfying the following conditions.

(i) Every atom in Λ is a LIA constraint of the form s t or x t or x y where s, t are ground, ∈{<, ≤, =, =, ≥, >}, and ∈{≤, =, ≥}, (ii) Every atom in Γ and ∆ is either an equation s ≈ s with s, s ∈ Ω ∪ V S , or a non-equational atom P (s 1 , . . . , s m ), where every s i of sort Z must be a variable x ∈ V Z , and every s i of sort S may be a variable u ∈ V S or a constant symbol c ∈ Ω.

We omit the empty multiset left of "→" and denote it by right of "→" (where at the same time stands for falsity). The clause notation separates arithmetic constraints from the free (also: uninterpreted ) part. We use the vertical double bar " " to indicate this separation syntactically. Intuitively, clauses Λ Γ → ∆ can be read as Λ ∧ Γ → ∆, i.e. the multisets Λ, Γ stand for conjunctions of atoms and ∆ stands for a disjunction of atoms.

Requiring the free part Γ → ∆ of clauses to not contain any base-sort terms apart from variables does not limit expressiveness. Every base-sort term t ∈ V Z in the free part can safely be replaced by a fresh base-sort variable x t when an atomic constraint x t = t is added to the constraint part of the clause (a process known as purification or abstraction [START_REF] Bachmair | Refutational Theorem Proving for Hierarchic First-Order Theories[END_REF][START_REF] Kruglov | Superposition Decides the First-Order Logic Fragment Over Ground Theories[END_REF]).

A hierarchic interpretation is an algebra A which interprets the base sort Z as Z A = Z, assigns integer values to all occurring base-sort Skolem constants, and interprets all LIA terms and constraints in the standard way. Moreover, A comprises a nonempty domain S A , assigns to each free-sort constant symbol c in Ω a domain element c A ∈ S A , and interprets every sorted predicate symbol P : ξ 1 × . . . × ξ m in Π by a set P A ⊆ ξ A 1 × . . . × ξ A m , as usual. Given a hierarchic interpretation A and a sort-respecting variable assignment β : V Z ∪ V S → Z A ∪ S A , we write A(β)(s) to address the value of the term s under A with respect to the variable assignment β. Given a BSR(SLI) clause C, consts(C) denotes the set of all constant symbols occurring in C. The set bconsts(N ) (fconsts(N )) is the restriction of consts(N ) to base-sort (free-sort) constant symbols. By vars(C) we denote the set of all variables occurring in C. Similar notation is used for other syntactic objects.

We define substitutions σ in the standard way as sort-respecting mappings from variables to terms. The restriction of the domain of a substitution σ to a set V of variables is denoted by σ| V and is defined such that vσ| V := vσ for every v ∈ V and vσ| V = v for every v ∈ V . While the application of a substitution σ to terms, atoms and multisets thereof is defined as usual, we need to be more specific for clauses. Consider a BSR(SLI) clause C := Λ Γ → ∆ and let x 1 , . . . , x k denote all base-sort variables occurring in C for which x i σ = x i . We then set Cσ := Λσ,

x 1 = x 1 σ, . . . , x k = x k σ Γ σ| V S → ∆σ| V S .
A term, atom, etc. is called ground, if it does not contain any variables. A BSR(SLI) clause C is called essentially ground if it does not contain free-sort variables and for every base-sort variable x occurring in C there is a constraint x = t in C for some ground LIA term t. A clause set N is essentially ground if all the clauses it contains are essentially ground.

Definition 2 (Normal Form of BSR(SLI) Clauses). A BSR(SLI) clause

Λ Γ → ∆ is in normal form if
(1) all non-ground atoms in Λ have the form x c or x ≤ y (or their symmetric variants) where c is an integer or Skolem constant and ∈{≤, =, ≥}, (2) all base-sort variables that occur in Λ also occur in Γ → ∆, and (3) Γ does not contain any equation of the form u ≈ t.

A BSR(SLI) clause set N is in normal form if all clauses in N are in normal form and pairwise variable disjoint. Moreover, we assume that N contains at least one free-sort constant symbol.

For every BSR(SLI) clause set N there is an equisatisfiable BSR(SLI) clause set N in normal form. It can be constructed from N by straightforward purification/abstraction methods [START_REF] Bachmair | Refutational Theorem Proving for Hierarchic First-Order Theories[END_REF][START_REF] Kruglov | Superposition Decides the First-Order Logic Fragment Over Ground Theories[END_REF] and a simple procedure for eliminating existentially quantified variables in LIA constraints (see [START_REF] Horbach | On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic[END_REF] for details).

Instantiation for BSR(SLI)

In this section, we present and prove our main technical result: Theorem 3. Satisfiability of a finite BSR(SLI) clause set N is decidable.

In essence, one can show that N is equisatisfiable to a finite set of essentially ground clauses (cf. Lemma 12). There are calculi, such as hierarchic superposition [START_REF] Bachmair | Refutational Theorem Proving for Hierarchic First-Order Theories[END_REF][START_REF] Althaus | Superposition Modulo Linear Arithmetic SUP(LA)[END_REF][START_REF] Kruglov | Superposition Decides the First-Order Logic Fragment Over Ground Theories[END_REF][START_REF] Fietzke | Superposition as a Decision Procedure for Timed Automata[END_REF][START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF] or DPLL(T) [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T)[END_REF], that can decide satisfiability of ground clause sets. Our decidability result for BSR(SLI) does not come as a surprise, given the similarity to other logic fragments that are known to be decidable, such as the array property fragment by Bradley, Manna, and Sipma [START_REF] Bradley | What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation[END_REF][START_REF] Bradley | The Calculus of Computation -Decision Procedures with Applications to Verification[END_REF] and Ge and de Moura's finite essentially uninterpreted fragment extended with simple integer arithmetic constraints [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF].

More important than the obtained decidability result is the instantiation methodology that we employ, in particular for integer-sort variables. Typically, decision procedures for the integer-indexed 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 (cf. the original approach [START_REF] Bradley | What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation[END_REF][START_REF] Bradley | Safety Analysis of Systems[END_REF] and standard literature [START_REF] Bradley | The Calculus of Computation -Decision Procedures with Applications to Verification[END_REF][START_REF] Kroening | Decision Procedures[END_REF]). In more sophisticated approaches, only a relevant portion of the occurring arithmetic terms is singled out before instantiation [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF].

Our methodology will also be based on a concept of relevant terms, determined by connections between the arguments of predicate symbols and instantiation points that are propagated along these connections. This part of our method is not specific for the integers but can be applied to the free part of our language as well. For integer variables, we investigate additional criteria to filter out unnecessary instances, inspired by the Loos-Weispfenning quantifier elimination procedure [START_REF] Loos | Applying Linear Quantifier Elimination[END_REF]. We elaborate on this in Sections 3.1 -3.3.

Instantiation of Integer Variables

We first summarize the overall approach for the instantiation of integer variables in an intuitive way. To keep the informal exposition simple, we pretend that all LIA terms are constants from Z. We even occasionally refer to the improper values -∞ / +∞ -"sufficiently small/large" integers. A formal treatment with proper definitions will follow.

Given a finite BSR(SLI) clause set N in normal form, we intend to partition Z into a set P of finitely many subsets p ∈ P such that satisfiability of N necessarily leads to the existence of a uniform hierarchic model.

Definition 4 (Uniform Interpretations). A hierarchic interpretation

A is uniform with respect to a partition P of the integers if and only if for every free predicate symbol Q occurring in N , every part p ∈ P, and all integers r 1 , r 2 ∈ p we have . . . , r 1 , . . .

∈ Q A if and only if . . . , r 2 , . . . ∈ Q A .
As soon as we have found such a finite partition P, we pick one integer value r p ∈ p as representative from each and every part p ∈ P. Given a clause C that contains a base-sort variable x, and given constant symbols d 1 , . . . , d k whose values cover all these representatives, i.e. {d A 1 , . . . ,

d A k } = {r p | p ∈ P}, we observe A |= C if and only if A |= C x/d i 1 ≤ i ≤ k .
This equivalence claims that we can transform universal quantification over the integer domain into finite conjunction over all representatives of subsets in P. Formulated differently, we can extrapolate a model for a universally quantified clause set, if we can find a model of finitely many instances of this clause set. The formal version of this statement is given in Lemma 12. Uniform hierarchic models play a key role in its proof.

When we extract the partition P from the given clause set N , we exploit three aspects to increase efficiency: (E-i) We group argument positions of free predicate symbols in such a way that the instantiation points relevant for these argument positions are identical. This means the variables that are associated to these argument positions, e.g. because they occur in such a place in some clause, need to be instantiated only with terms that are relevant for the respective group of argument positions. This is illustrated in Example 5. (E-ii) Concerning the relevant integer constraints, i.e. the ones that produce instantiation points, one can choose to either stick to lower bounds exclusively, use -∞ as a default (the lowest possible lower bound), and ignore upper bounds. Alternatively, one can focus on upper bounds, use +∞ as default, and ignore lower bounds. This idea goes back to the Loos-Weispfenning quantifier elimination procedure over the reals [START_REF] Loos | Applying Linear Quantifier Elimination[END_REF]. Example 8 gives some intuition. (E-iii) The choice described under (E-ii) can be made independently for every integer variable that is to be instantiated. See Examples 8 and 13.

Example 5. Consider the following clauses:

C 1 := 1 ≤ x 1 , x 2 ≤ 0 → T (x 1 ), Q(x 1 , x 2 ) , C 2 := y 3 ≤ 7, y 1 ≤ y 3 Q(y 1 , y 2 ) → R(y 3 ) , C 3 := 6 ≤ z 1 T (z 1 )
→ . The variables x 1 , x 2 , y 1 , y 2 , y 3 , and z 1 are affected by the constraints in which they occur explicitly. Technically, it is more suitable to speak of the argument position T, 1 instead of variables x 1 and z 1 that occur as the first argument of the predicate symbol T in C 1 and C 3 , respectively. Speaking in such terms, argument position T, 1 is directly affected by the constraints 1 ≤ x 1 and 6 ≤ z 1 , argument position Q, 1 is directly affected by 1 ≤ x 1 and y 1 ≤ y 3 , Q, 2 is affected by x 2 ≤ 0, and, finally, R, 1 is affected by y 3 ≤ 7 and y 1 ≤ y 3 . Besides such direct effects, there are also indirect effects that have to be taken into account. For example, the argument position Q, 1 is indirectly affected by the constraint 6 ≤ z 1 , because C 1 establishes a connection between argument positions T, 1 and Q, 1 via the simultaneous occurrence of x 1 in both argument positions and T, 1 is affected by 6 ≤ z 1 . This is witnessed by the fact that C 1 and C 3 together logically entail the clause D := 6 ≤ x, y ≤ 0 → Q(x, y). D can be obtained by a hierarchic superposition step from C 1 and C 3 , for instance. Another entailed clause is 6 ≤ z, z ≤ 7 → R(z), the (simplified) result of hierarchically resolving D with C 2 . Hence, R, 1 is affected by the constraints 6 ≤ z and z ≤ 7. Speaking in terms of argument positions, this effect can be described as propagation of the lower bound 6 ≤ y 1 from Q, 1 to R, 1 via the constraint y 1 ≤ y 3 in C 2 .

One lesson learned from the example is that argument positions can be connected by variable occurrences or constraints of the form x ≤ y. Such links in a clause set N are expressed by the relation ⇒ N . Definition 6 (Connections Between Argument Positions and Argument Position Closures). Let N be a BSR(SLI) clause set in normal form. We define ⇒ N to be the smallest preorder (i.e. a reflexive and transitive relation) over Π ×N such that Q, j ⇒ N P, i whenever there is a clause Λ Γ → ∆ in N containing free atoms Q(. . . , u, . . .) and P (. . . , v, . . .) in which the variable u occurs at the j-th and the variable v occurs at the i-th argument position and

(1) either u = v, (2) or u = v, both are of sort Z and there are constraints u = v or u ≤ v in Λ, (3) or u = v, both are of sort S and there is an atom u ≈ v in Γ or in ∆. 3 ⇒ N induces downward closed sets ⇓ N P, i of argument positions, called argument position closures: ⇓ N P, i := Q, j Q, j ⇒ N P, i . Consider a variable v that occurs at the i-th argument position of a free atom P (. . . , v, . . .) in N . We denote the argument position closure related to v's argument position in N by ⇓ N (v), i.e. ⇓ N (v) := ⇓ N P, i . If v is a free-sort variable that exclusively occurs in equations, we set ⇓ N (v) := ⇓ False v , 1 (cf. footnote 3 ). To simplify notation a bit, we write ⇒, ⇓ P, i , and ⇓(v) instead of ⇒ N , ⇓ N P, i , and ⇓ N (v), when the set N is clear from the context.

Notice that ⇒ confined to argument position pairs of the free sort is always symmetric. Asymmetry is only introduced by atomic constraints x ≤ y.

While the relation ⇒ indicates how instantiation points are propagated between argument positions, the set ⇓ P, i comprises all argument positions from which instantiation points are propagated to P, i . For a variable v the set ⇓(v) contains all argument positions that may produce instantiation points for v.

Next, we collect the instantiation points that are necessary to eliminate base-sort variables by means of finite instantiation.

Definition 7 (Instantiation Points for Base-Sort Argument Positions).

Let N be a BSR(SLI) clause set in normal form and let P : ξ 1 × . . . × ξ m be a free predicate symbol occurring in N . For every i with ξ i = Z we define I P,i to be the smallest set satisfying the following condition. We have d ∈ I P,i for any constant symbol d for which there exists a clause C in N that contains an atom P (. . . , x, . . .) in which x occurs as the i-th argument and that contains a constraint x = d or x ≥ d.

The most apparent peculiarity about this definition is that LIA constraints 3 For any free-sort variable v that occurs in a clause (Λ Γ → ∆) ∈ N exclusively in equations, we pretend that ∆ contains an atom Falsev(v), for a fresh predicate symbol Falsev : S. This is merely a technical assumption. Without it, we would have to treat such variables v as a separate case in all definitions. The atom Falsev(v) is not added "physically" to any clause.

of the form x ≤ d are completely ignored when collecting instantiation points for x's argument position. This is one of the aspects that makes this definition interesting from the efficiency point of view, because the number of instances that we have to consider might decrease considerably in this way. The following example may help to develop an intuitive understanding. But there are other interesting possibilities, for instance, the more coarsegrained partition {(-∞, 2], [3, +∞)} together with the predicate T A = [3, +∞). This latter candidate partition completely ignores the constraints x ≤ 0 and x ≤ 5 that constitute upper bounds on x and in this way induces a simpler partition. Dually, we could have concentrated on the upper bounds instead (completely ignoring the lower bounds). This would have led to the partition {(-∞, 0], [START_REF] Abadi | Decidable Fragments of Many-Sorted Logic[END_REF][START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF], [6, +∞)} and the candidate predicate

T A = [1, 5] (or T A = [1, +∞))
. Both ways are possible, but the former yields a coarser partition and is thus more attractive, as it will cause fewer instances in the end.

The example reveals quite some freedom in choosing an appropriate partition of the integers. A large number of parts directly corresponds to a large number of instantiation points-one for each interval-, and therefore leads to a large number of instances that need to be considered by a reasoning procedure. Hence, regarding efficiency, it is of great importance to keep the partition P of Z coarse.

It remains to address the question of why it is sufficient to consider lower bounds only. At this point, we content ourselves with an informal explanation. Let ϕ(x) be a satisfiable ∧-∨-combination of upper and lower bounds on some integer variable x. For the sake of simplicity, we assume that every atom in ϕ is of the form c ≤ x or x ≤ c with c ∈ Z. When we look for some value of x that satisfies ϕ, we start from some "sufficiently small value" -∞. If -∞ yields a solution for ϕ, we are done. If [x → -∞] |= ϕ, there must be some lower bound in ϕ that prevents -∞ from being a solution. In order to find a solution, we successively increase the value of x until a solution is found. Interesting test points r ∈ Z for x are those where r -1 violates some lower bound c ≤ x in ϕ and r satisfies the bound, i.e. r = c. Consider two lower bounds c 1 ≤ x and c 2 ≤ x in ϕ such that c 1 < c 2 and ϕ contains no further bound d ≤ x with c 1 < d < c 2 . Any assignment [x →r] with c 1 < r < c 2 satisfies exactly the same lower bounds as the assignment [x →c 1 ] does. Moreover, any such assignment satisfies at most the upper bounds that [x →c 1 ] satisfies. In fact, it may violate some of them. Consequently, if neither [x →c 1 ] nor [x →c 2 ] satisfy ϕ, then [x →r] with c 1 < r < c 2 cannot satisfy ϕ either. In other words, it suffices to test only values induced by lower bounds. The abstract value -∞ serves as the default value, which corresponds to the implicit lower bound -∞ < x.

Definition 9 (Instantiation Points for Base-Sort Argument Position

Closures and Induced Partition). Let N be a BSR(SLI) clause set in normal form and let A be a hierarchic interpretation. For every base-sort argument position closure ⇓ P, i induced by ⇒ we define the following:

The set I ⇓ P,i of instantiation points for ⇓ P, i is defined by I ⇓ P,i := {c -∞ } ∪ Q,j ∈⇓ P,i I Q,j , where we assume c -∞ to be a distinguished base-sort constant symbol that may occur in N .

Let the sequence r 1 , . . . , r k comprise all integers in the set c A c ∈ I ⇓ P,i \ {c -∞ } ordered so that r 1 < . . . < r k . The partition P A ⇓ P,i of the integers into finitely many intervals is defined by

P A ⇓ P,i := (-∞, r 1 -1], [r 1 , r 2 -1], . . . , [r k-1 , r k -1], [r k , +∞) .
Please note that partitions as described in the definition do always exist, and do not contain empty parts.

Lemma 10. Let N be a BSR(SLI) clause set in normal form and let A be a hierarchic interpretation. Consider two argument position pairs Q, j , P, i for which Q, j ⇒ P, i holds in N . Then I ⇓ Q,j ⊆ I ⇓ P,i . Moreover, P A ⇓ P,i is a refinement of P A ⇓ Q,j , i.e. for every p ∈ P A ⇓ P,i there is some p ∈ P A ⇓ Q,j such that p ⊆ p . Lemma 11. Let N be a BSR(SLI) clause set in normal form and let A be a hierarchic interpretation. For every part p ∈ P A ⇓ P,i of the form p = [r , r u ] or p = [r , +∞) we find some constant symbol c ⇓ P,i ,p ∈ I ⇓ P,i with c A ⇓ P,i ,p = r .

Note that the lemma did not say anything about the part (-∞, r u ] which also belongs to every P A ⇓ P,i . Our intention is that the constant symbol c -∞ shall be interpreted by a value from this interval. Hence, we add the set of clauses Ψ -∞ N := (c -∞ ≥ c → ) c ∈ bconsts(N ) \ {c -∞ } whenever necessary. Note that if A is a hierarchic model of a given BSR(SLI) clause set N , then A can be turned into a model of Ψ -∞ N just by changing the interpretation of c -∞ . After this modification A is still a model of N , if c -∞ does not occur in N .

The next lemma shows that we can eliminate base-sort variables x from clauses C in a finite BSR(SLI) clause set N by replacing C with finitely many instances in which x is substituted with the instantiation points that we computed for x. In addition, the axioms that stipulate the meaning of c -∞ need to be added. Iterating this instantiation step for every base-sort variable in N eventually leads to a clause set that is essentially ground with respect to the constraint parts of the clauses it contains (free-sort variables need to be treated separately, of course, see Section 3.3).

Lemma 12 (Finite Integer-Variable Elimination).

Let N be a finite BSR(SLI) clause set in normal form such that, if the constant symbol c -∞ occurs in N , then Ψ -∞ N ⊆ N . Suppose there is a clause C in N which contains a base-sort variable x. Let N x be the clause set

N x := N \ {C} ∪ C x/c c ∈ I ⇓ N (x) ∪ Ψ -∞ N . N is satisfiable if and only if N x is satisfiable.
Proof sketch. The "only if"-part is trivial.

The "if"-part requires a more sophisticated argument. In what follows, the notations ⇒ and ⇓ always refer to the original clause set N . Let A be a hierarchic model of N x . We use A to construct the hierarchic model B |= N as follows. For the domain S B we reuse A's free domain S A . For every base-sort or free-sort constant symbol c ∈ consts(N ) we set c B := c A . For every predicate symbol P : ξ 1 × . . . × ξ m that occurs in N , for every argument position i, 1 ≤ i ≤ m, with ξ i = Z, and for every interval p ∈ P A ⇓ P,i Lemma 11 and the extra clauses in Ψ -∞ N guarantee the existence of a base-sort constant symbol c ⇓ P,i ,p ∈ I ⇓(x) , such that c A ⇓ P,i ,p ∈ p. Based on this observation, we define the family of projection functions π ⇓ P,i :

Z ∪ S B → Z ∪ S A by π ⇓ P,i (a) :=      c A ⇓ P,i ,p if ξ i = Z and p ∈ P A ⇓ P,i
is the interval a lies in, a if ξ i = S. Using the projection functions π ⇓ P,i , we define the sets P B in such a way that for all domain elements a 1 , . . . , a m of appropriate sorts a 1 , . . . , a m ∈ P B if and only if π ⇓ P,1 (a 1 ), . . . , π ⇓ P,m (a m ) ∈ P A . We next show B |= N . Consider any clause C := Λ Γ → ∆ in N and let β : V Z ∪ V S → Z ∪ S B be some variable assignment. From β we derive a special variable assignment β π for which we shall infer A, β π |= C as an intermediate step:

β π (v) := π ⇓(v) (β(v)) for every variable v. If C = C,

Independent Bound Selection

By now we have mainly focused on lower bounds as sources for instantiation points. However, as we have already pointed out (cf. (E-ii) and (E-iii) in Section 3.1 and Example 8), there is also a dual approach in which upper bounds on integer variables play the central role. It turns out that the choice between the two approaches can be made independently for every variable that is to be instantiated. In the interest of efficiency, it makes sense to always choose the approach that results in fewer non-redundant instances or, more abstractly speaking, a set of instances whose satisfiability is easier to decide. Example 13 illustrates the overall approach.

Given a clause set N in normal form, the relation ⇒ N is defined as before. Dually to the sets ⇓ N P, i , we define the sets ⇑ N P, i := Q, j P, i ⇒ N Q, j , which constitute upwards closed sets with respect to ⇒ N rather than downwards closed sets. Regarding instantiation points, only LIA constraints x = d and x ≤ d lead to d ∈ I ⇑ N (x) . In addition, c +∞ is by default added to every set I ⇑ N P,i . In order to fix the meaning of c +∞ , we introduce the set of axioms

Ψ +∞ N := (c +∞ ≤ c → ) c ∈ bconsts(N ) \ {c +∞ } .
The dual versions of Definitions 7 and 9 and Lemma 12 can be found in [START_REF] Horbach | On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic[END_REF].

In both, Lemma 12 and its dual version, the equisatisfiable instantiation can be applied to the respective variable independently of the instantiation steps that have already been done or are still to be done in the future. This means, we can choose independently, whether to stick to the lower or upper bounds for instantiation. This choice can, for example, be made depending on the number of non-redundant instances that have to be generated.

Example 13. Consider the following BSR(SLI) clause set N :

1 ≤ x1, x2 ≤ 0 → T (x1), Q(x1, x2) , y3 ≤ 7, y1 ≤ y3 Q(y1, y2) → R(y3) , 6 ≤ z1, z1 ≤ 9 T (z1) → .
We intend to instantiate the variables y 3 , y 1 , x 1 , z 1 in this order. For y 3 we can choose between

I ⇓ N (y3) = {c -∞ , 1, 6} and I ⇑ N (y3) = {7, c +∞ }.
Using the latter option, we obtain the instances

7 ≤ 7, y1 ≤ 7, y3 = 7 Q(y1, y2) → R(y3) c+∞ ≤ 7, y1 ≤ c+∞, y3 = c+∞ Q(y1, y2) → R(y3)
plus the clauses in Ψ +∞ N . The constraint 7 ≤ 7 can be removed, as it is redundant. The second instance can be dropped immediately, since the constraint c +∞ ≤ 7 is false in any model satisfying Ψ +∞ N . Dual simplifications can be applied to constraints with c -∞ . Let N contain the clauses in Ψ +∞ N and the clauses

1 ≤ x1, x2 ≤ 0 → T (x1), Q(x1, x2) , y1 ≤ 7, y3 = 7 Q(y1, y2) → R(y3) , 6 ≤ z1, z1 ≤ 9 T (z1) → .
For y 1 we use I ⇓ N (y1) = {c -∞ , 1, 6} rather than I ⇑ N (y1) = {7, 9, c +∞ } for instantiation and obtain N (after simplification):

1 ≤ x1, x2 ≤ 0 → T (x1), Q(x1, x2) , y3 = 7, y1 = c-∞ Q(y1, y2) → R(y3) , y3 = 7, y1 = 1 Q(y1, y2) → R(y3) , y3 = 7, y1 = 6 Q(y1, y2) → R(y3) , 6
I ⇑ N (x1) = {c -∞ , 1, 6, 9, c +∞ }.
The latter set nicely illustrates how instantiation sets for particular variables can evolve during the incremental process of instantiation. We take the set with fewer instantiation points and obtain N :

x2 ≤ 0, x1 = 1 → T (x1), Q(x1, x2) , x2 ≤ 0, x1 = 6 → T (x1), Q(x1, x2) , y3 = 7, y1 = c-∞ Q(y1, y2) → R(y3) , y3 = 7, y1 = 1 Q(y1, y2) → R(y3) , y3 = 7, y1 = 6 Q(y1, y2) → R(y3) , 6 ≤ z1, z1 ≤ 9 T (z1) → , plus Ψ -∞ N ∪ Ψ +∞ N ∪ {c -∞ ≥ c +∞ → }.
We instantiate z 1 using the set

I ⇓ N (z1) = {c -∞ , 1, 6} and not I ⇑ N (z1) = {c -∞ , 1, 6, 9, c +∞ }: x2 ≤ 0, x1 = 1 → T (x1), Q(x1, x2) , x2 ≤ 0, x1 = 6 → T (x1), Q(x1, x2) , y3 = 7, y1 = c-∞ Q(y1, y2) → R(y3) , y3 = 7, y1 = 1 Q(y1, y2) → R(y3) , y3 = 7, y1 = 6 Q(y1, y2) → R(y3) , z1 = 6 T (z1) → , plus Ψ -∞ N ∪ Ψ +∞ N ∪ {c -∞ ≥ c +∞ → }.
Until now, we have introduced 6 non-redundant instances. A completely naive instantiation approach where x 1 , y 1 , y 3 , z 1 are instantiated with all occurring constant symbols 0, 1, 6, 7, 9 leads to 17 non-redundant instances. This corresponds to the originally proposed method for the array property fragment, cf. [START_REF] Bradley | What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation[END_REF]. A more sophisticated instantiation approach where x 1 , y 1 , y 3 , z 1 are instantiated with 1, 6, 7, 9 (as there is no connection from 0 to x 1 , y 1 , y 3 , z 1 ) leads to 13 non-redundant instances. For instance, the methods described in [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF] produce this set of instances.

Instantiation of Free-Sort Variables

We can also follow an instantiation approach for free-sort variables. In a nutshell, we collect only relevant instantiation points for a given argument position (cf. (E-i)). A similar approach is taken in [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF]. Consult [START_REF] Horbach | On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic[END_REF] for details.

Stratified Clause Sets

In this section we treat certain clause sets with uninterpreted non-constant function symbols. By a transformation into an equisatisfiable set of BSR clauses, we show that our instantiation methods are also applicable in such settings. Definition 14. Let N be a finite set of variable-disjoint first-order clauses in which also non-constant function symbols occur. By Π N and Ω N we denote the set of occurring predicate symbols and function symbols (including constants), respectively. N is considered to be stratified if we can define a mapping lvl N : (Π N ∪ Ω N ) × N → N that maps argument position pairs (of predicate and function symbols) to nonnegative integers such that the following conditions are satisfied.

(a) For every function symbol f : ξ 1 × . . . × ξ m → ξ m+1 and every i ≤ m we have lvl N f, i > lvl N f, m + 1 . (b) For every (sub)term g(s 1 , . . . , s k-1 , f (t 1 , . . . , t m ), s k+1 , . . . , s m ) occurring in N we have lvl N f, m + 1 = lvl N g, k . This includes the case where f is a constant symbol and m = 0. Moreover, this also includes the case where g is replaced with a predicate symbol P . (c) For every variable v that occurs in two (sub)terms f (s 1 , . . . , s k-1 , v, s k+1 , . . . , s m ) and

g(t 1 , . . . , t k -1 , v, t k +1 , . . . , t m ) in N we have lvl N f, k = lvl N g, k .
The same applies, if f or g or both are replaced with predicate symbols. (d) For every equation f (s 1 , . . . , s m ) ≈ g(t 1 , . . . , t m ) we have lvl N f, m + 1 = lvl N g, m + 1 . This includes the cases where f or g or both are constant symbols (with m = 0 or m = 0 or both, respectively).

Several known logic fragments fall into this syntactic category: many-sorted clauses over stratified vocabularies as described in [START_REF] Abadi | Decidable Fragments of Many-Sorted Logic[END_REF][START_REF] Korovin | Non-cyclic Sorts for First-Order Satisfiability[END_REF], and clauses belonging to the finite essentially uninterpreted fragment (cf. Proposition 2 in [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF]).

Lemma 15. Let C = Γ → ∆ be a first-order clause and let f 1 , . . . , f n be a list of all uninterpreted non-constant function symbols occurring in C. Let R 1 , . . . , R n be distinct predicate symbols that do not occur in C and that have the sort

R i : ξ 1 × . . . × ξ m × ξ m+1 , if and only if f i has the sort ξ 1 × . . . × ξ m → ξ m+1 .
Let Φ 1 and Φ 2 be the following sets of sentences:

Φ 1 := ∀x 1 . . . x m uv. R i (x 1 , . . . , x m , u) ∧ R i (x 1 , . . . , x m , v) → u ≈ v 1 ≤ i ≤ n and Φ 2 := ∀x 1 . . . x m ∃v. R i (x 1 , . . . , x m , v) 1 ≤ i ≤ n .
There is a clause D that does not contain non-constant function symbols and for which the set

{D} ∪ Φ 1 ∪ Φ 2 is equisatisfiable to C.
Proof sketch. We apply the following flattening rules. v stands for a fresh variable that has not occurred yet. P ranges over predicate symbols different from ≈. s and t stand for tuples of arguments.

Γ, f i (s) ≈ f j ( t ) → ∆ (fun-fun left) Γ, R i (s, v), R j ( t, v) → ∆ Γ → ∆, f i (s) ≈ f j ( t ) (fun-fun right) Γ, R i (s, v) → ∆, R j ( t, v) Γ, f i (s) ≈ c → ∆ (fun-const left) Γ, R i (s, c) → ∆ Γ → ∆, f i (s) ≈ c (fun-const right) Γ → ∆, R i (s, c) Γ, f i (s) ≈ x → ∆ (fun-var left) Γ, R i (s, x) → ∆ Γ → ∆, f i (s) ≈ x (fun-var right) Γ → ∆, R i (s, x) Γ, P (. . . , f i (s), . . .) → ∆ (fun left) Γ, R i (s, v), P (. . . , v, . . .) → ∆ Γ → ∆, P (. . . , f i (s), . . .) (fun right) Γ,R i (s, v) → ∆,P (. . . , v, . . .)
Given a BSR clause Γ → ∆, we consider an atom R j ( t, v) in ∆ to be guarded, if there is also an atom R i (s, v) in Γ . With the exception of the rule (fun-var right) the flattening rules presented in the proof of Lemma 15 preserve guardedness of atoms in ∆ and introduce atoms R j ( t, v) on the right-hand side of a clause only if at the same time a corresponding guard is introduced on the left-hand side of the clause.

Hence, if we are given a stratified clause set in which the atoms x ≈ t in the consequents of implications are subject to certain restrictions (e.g. t = f (. . .) and guardedness of atoms u ≈ c and u ≈ v), then the above flattening rules yield clauses that belong to the following class of BSR(SLI) clauses-after necessary purification and normalization steps. In the definition we mark certain predicate symbols that are intended to represent uninterpreted functions. By adding suitable axioms later on, these will be equipped with the properties of function graphs.

Definition 16 (Stratified and Guarded BSR(SLI)). Consider a BSR(SLI) clause set N in normal form. Let R 1 , . . . , R n be a list of predicate symbols that we consider to be marked in N . We call N stratified and guarded with respect to R 1 , . . . , R n , if and only if the following conditions are met.

(a) There is some function lvl N : Π × N → N that assigns to each argument position pair P, i a nonnegative integer lvl N P, i such that (a.1) P, i ⇒ N Q, j entails lvl N P, i = lvl N Q, j , and (a.2) for every marked predicate symbol R j : ξ 1 × . . . × ξ m × ξ m+1 we have lvl N R j , i > lvl N R j , m + 1 for every i ≤ m. (b) In every clause Λ Γ → ∆ in N any occurrence of an atom R j (s 1 , . . . , s m , v) in ∆ entails that Γ contains some atom R (t 1 , . . . , t m , v). (c) For every atom u ≈ t in N , where t is either a free-sort variable v or a free-sort constant symbol, at least one of two cases applies: (c.1) u ≈ t, which must occur in the consequent of a clause, is guarded by some atom R j (t 1 , . . . , t m , u) occurring in the antecedent of the same clause. (c.2) For every marked predicate symbol R j : ξ 1 × . . . × ξ m × ξ m+1 and every argument position closure

⇓ N R j , i with 1 ≤ i ≤ m we have ⇓ N R j , i ∩ ⇓ N (u) = ∅. If t = v, we in addition have ⇓ N R j , i ∩ ⇓ N (v) = ∅.
Notice that any atom u ≈ v over distinct variables requires two guards R(s, u) and R( t, v) in order to be guarded in accordance with Condition (c.1).

Let N be a finite BSR(SLI) clause set in normal form that is stratified and guarded with respect to R 1 , . . . , R n . Let R i : ξ 1 × . . . × ξ m × ξ m+1 be marked in N and let P : ζ 1 × . . . × ζ m be any predicate symbol occurring in N (be it marked or not). We write R i P if and only if lvl N R i , m + 1 ≥ min 1≤ ≤m lvl N P, . Without loss of generality, we assume R

1 N . . . N R n . Let Φ 1 := {∀x 1 . . . x m uu .(R i (x 1 , . . . , x m , u) ∧ R i (x 1 , . . . , x m , u )) → u u | R i has arity m + 1} and Φ 2 := {∀x 1 . . . x m ∃u. R i (x 1 , . . . , x m , u) | R i has arity m + 1}
, where " " is a placeholder for "≈" in free-sort equations and for "=" in base-sort equations.

Given a set M of BSR(SLI) clauses and an (m + 1)-ary predicate symbol R that is marked in M , we define the set Φ(R, M where

I [m] ⇓ M R,
• is used as an abbreviation for I ⇓ M R,1 × . . . × I ⇓ M R,m and the d Rc1...cm are assumed to be fresh constant symbols. It is worth noticing that the clauses corresponding to Φ(R, M ) are stratified and guarded BSR(SLI) clauses.

We construct the sequence M 0 , M 1 , . . . , M n of finite clause sets as follows: M 0 := N , every M +1 with ≥ 0 is an extension of M by the BSR(SLI) clauses that correspond to the sentences in Φ(R +1 , M ).

Lemma 17. The set N ∪ Φ 1 ∪ Φ 2 is satisfiable if and only if M n is satisfiable.
This lemma entails that all the instantiation methods developed in Section 3 can be used to decide satisfiability of stratified and guarded BSR(SLI) clause sets.

We can add another background theory to the stratified and guarded fragment of BSR(SLI) while preserving compatibility with our instantiation approach. Let Π T and Ω T be finite sets of sorted predicate symbols and sorted function symbols, respectively, and let T be some theory over Π T and Ω T . We assume that Π T is disjoint from the set Π of uninterpreted predicate symbols. For any set X of variables, let T T (X) be the set of all well-sorted terms constructed from the variables in X and the function and constant symbols in Ω T .

Definition 18 (BSR(SLI+T )). A clause set N belongs to BSR(SLI+T ) if it complies with the syntax of a BSR(SLI) clause set that is stratified and guarded with respect to certain predicate symbols R 1 , . . . , R n with the following exceptions. Let C := Λ Γ → ∆ be a clause in N . We allow atoms P (s 1 , . . . , s m ) with P ∈ Π T and s 1 , . . . , s m ∈ T T (V Z ∪ V S )-including equations s 1 ≈ s 2 -, if for every variable u occurring in any of the s i there is either a LIA guard of the form u = t in Λ with t being ground, or there is a guard R j (t 1 , . . . , t m , u) in Γ .

The instantiation methods presented in Section 3 are also applicable to BSR(SLI+T ), since Lemma 17 can be extended to cover finite BSR(SLI+T ) clause sets. When computing instantiation points for BSR(SLI+T ) clause sets, we ignore T -atoms. For example, a clause R(t, u), P (s, c) → P (s , u), Q(u) where P (s, c) and P (s , u) are T -atoms, does not lead to an instantiation point c for ⇓ Q, 1 . If we stick to this approach, the proof of Lemma 17 can easily be adapted to handle additional T -atoms. The involved model construction remains unchanged. T -atoms are basically treated like guarded free-sort atoms u ≈ d. Proposition 19. BSR(SLI+T ) allows an (un)satisfiability-preserving embedding of the array property fragment with integer-indexed arrays and element theory T (cf. [START_REF] Bradley | What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation[END_REF]) and of the finite essentially uninterpreted fragment extended with simple integer arithmetic literals (cf. [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF]) into BSR(SLI+T ).

Example 20. The following formula ϕ belongs to the array property fragment with integer indices and the theory of bit vectors as the element theory T . The operator ∼ stands for bitwise negation of bit vectors and the relations and ≈ are used as the "at most" and the equality predicate on bit vectors, respectively. Moreover, a[i] denotes a read operation on the array a at index i.

ϕ

:= c ≥ 1 ∧ ∀ij. 0 ≤ i ≤ j → a[i] a[j] ∧ ∀i. 0 ≤ i ≤ c -1 → a[i] ∼ a[0] ∧ → a[c] ≈ ∼ a[0] ∧ ∀i. i ≥ c + 1 → a[i] ∼ a[0]
Translating ϕ into BSR(SLI+T ) yields the following clause set N , in which we consider P a to be marked.

c < 1 → e = c -1 → f = c + 1 →
0 ≤ i, i ≤ j P a (i, u), P a (j, v) → u v 0 ≤ i, i ≤ e, y = 0 P a (i, u), P a (y, v) → u ∼ v x = c, y = 0 P a (x, u), P a (y, v) → u ≈ ∼ v i ≥ f, y = 0 P a (i, u), P a (y, v) → u ∼ v In order to preserve (un)satisfiability, functional axioms have to be added for P a (cf. the sets Φ 1 and Φ 2 that we used earlier). Doing so, we leave BSR(SLI+T ).

The clause set N induces the set I ⇓ Pa,1 = {c -∞ , 0, c, f } of instantiation points for the index of the array. An adaptation of Lemma 17 for BSR(SLI+T ) entails that adding the clause set N corresponding to the following set of sentences yields a BSR(SLI+T ) clause set N ∪ N that is equisatisfiable to ϕ.

Discussion

We have demonstrated how universally quantified variables in BSR(SLI) clause sets can be instantiated economically. In certain cases our methods lead to exponentially fewer instances than a naive instantiation with all occurring integer terms would generate. Moreover, we have sketched how defining suitable finitedomain sort predicates instead of explicitly instantiating variables can avoid immediate blow-ups caused by explicit instantiation. It is then left to the theorem prover to actually instantiate variables as needed.

We have shown that our methods are compatible with uninterpreted, nonconstant functions under certain restrictions. Even another background theory T may be added, leading to BSR(SLI+T ). This entails applicability of our instantiation approach to known logic fragments, such as the array property fragment [START_REF] Bradley | What's Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation[END_REF], the finite essentially uninterpreted fragment with arithmetic literals [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF], and many-sorted first-order formulas over stratified vocabularies [START_REF] Abadi | Decidable Fragments of Many-Sorted Logic[END_REF][START_REF] Korovin | Non-cyclic Sorts for First-Order Satisfiability[END_REF].

The instantiation methodology that we have described specifically for integer variables can also be adapted to work for universally quantified variables ranging over the reals [START_REF] Voigt | Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete[END_REF]. Our computation of instantiation points considers all argument positions in predicate atoms independently. This can be further refined by considering dependencies between argument positions and clauses. For example, this refinement idea was successfully applied in first-order logic [START_REF] Claessen | Sort It Out with Monotonicity -Translating between Many-Sorted and Unsorted First-Order Logic[END_REF][START_REF] Korovin | Non-cyclic Sorts for First-Order Satisfiability[END_REF].

Once all the integer variables are grounded by successive instantiation, we are left with a clause set where for every integer variable x in any clause there is a defining equation x = c for some constant c. Thus, the clause set can actually be turned into a standard first-order BSR clause set by replacing the integer constants with respective fresh uninterpreted constants. Then, as an alternative to further grounding the free-sort variables, any state-of-the-art BSR decision procedure can be applied to test satisfiability [START_REF] Piskac | Deciding Effectively Propositional Logic Using DPLL and Substitution Sets[END_REF][START_REF] Korovin | Inst-Gen -A Modular Approach to Instantiation-Based Automated Reasoning[END_REF][START_REF] Alagi | NRCL -A Model Building Approach to the Bernays-Schönfinkel Fragment[END_REF]. It is even sufficient to know the instantiation sets for the base sort variables. Then, instead of explicit grounding, by defining respective finite-domain sort predicates for the sets, the worst-case exponential blow-up of grounding can be prevented.

Example 8 .

 8 Consider two clauses C := 3 ≤ x, x ≤ 5 → T (x) and D := x ≤ 0 T (x) → . Recall that we are looking for a finite partition P of Z such that we can construct a uniform hierarchic model A of {C, D}, i.e. for every subset p ∈ P and all integers r 1 , r 2 ∈ p we want r 1 ∈ T A to hold if and only if r 2 ∈ T A . A natural candidate for P is {(-∞, 0],[START_REF] Abadi | Decidable Fragments of Many-Sorted Logic[END_REF][START_REF] Alagi | NRCL -A Model Building Approach to the Bernays-Schönfinkel Fragment[END_REF],[START_REF] Althaus | Superposition Modulo Linear Arithmetic SUP(LA)[END_REF][START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF], [6, +∞)}, which takes every LIA constraint in C and D into account. Correspondingly, we find the candidate model A with T A =[START_REF] Althaus | Superposition Modulo Linear Arithmetic SUP(LA)[END_REF][START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF]. Obviously, A is uniform with respect to P.

  then N x already contains C , and thus A, β π |= C must hold. In case of C = C, let p * be the interval in P A ⇓(x) containing the value β(x), and let c * be an abbreviation for c ⇓(x),p * . Due to β π (x) = c A * and since A is a model of the clause C x/c * in N x , we conclude A, β π |= C. Hence, in any case we can deduce A, β π |= C . By case distinction on why A, β π |= C holds, we may use this result to infer B, β |= C . It follows that B |= N .

  ≤ z1, z1 ≤ 9 T (z1) → , plus the clauses in Ψ -∞ N and Ψ +∞ N and plus the clause c -∞ ≥ c +∞ → . The sets of instantiation points for x 1 in N are I ⇓ N (x1) = {c -∞ , 1, 6} and

  ) := R(c 1 , . . . , c m , d Rc1...cm ) c 1 , . . . , c m ∈ I [m] ⇓ M R,• ∪ ∀x 1 . . . x m . c1,...,cm ∈I [m] ⇓ M R,• R(x 1 , . . . , x m , d Rc1...cm ) ∪ ∀x 1 . . . x m u. R(x 1 , . . . , x m , u) → c1,...,cm ∈I [m] ⇓ M R,• u d Rc1...cm ∪ ∀x 1 . . . x m . R(x 1 , . . . , x m , d Rc1...cm ), R(x 1 , . . . , x m , d Rc 1 ...c m ) → d Rc1...cm d Rc 1 ...c m c 1 , . . . , c m , c 1 , . . . , c m ∈ I [m] ⇓ M R,•

  P a (c , d Pac ) c ∈ {c -∞ , 0, c, f } ∪ ∀i. c ∈{c-∞,0,c,f } P a (i, d Pac ) ∪ ∀iu. P a (i, u) → c ∈{c-∞,0,c,f } u ≈ d Pac ∪ ∀i. P a (i, d Pac ), P a (i, d Pac ) → d Pac ≈ d Pac c , c ∈ {c -∞ , 0, c, f }Using the instantiation methods that we have developed in Sections 3.1 -3.3, the set N ∪ N can be turned into an equisatisfiable quantifier-free clause set.One possible (uniform) modelA |= N ∪ N assigns c A -∞ = -1, e A = 2, c A = 3, f A = 4, d A Pac-∞ =00, d A Pa0 = 01, d A Pae = 01, d A Pac = 10, d A Paf = 11, and yields the array 01, 01, 01, 10, 11, 11, 11, . . . .

  The variables occurring in clauses are implicitly universally quantified. Therefore, given a clause C, we call A a hierarchic model of C, denoted A |= C, if and only if A, β |= C holds for every variable assignment β. For clause sets N , A |= N holds if and only if A |= C holds true for every clause C ∈ N . We call a clause C (a clause set N ) satisfiable if and only if there exists a hierarchic model A of C (of N ). Two clauses C, D (clause sets N, M ) are equisatisfiable if and only if C (N ) is satisfiable whenever D (M ) is satisfiable and vice versa.