Paula Chocron

Pascal Fontaine

Christophe Ringeissen

A Gentle Non-Disjoint Combination of Satisfiability Procedures (Extended Version)

Keywords: Satisfiability problem, combination method, union of non-disjoint theories

A satisfiability problem is often expressed in a combination of theories, and a natural approach consists in solving the problem by combining the satisfiability procedures available for the component theories. This is the purpose of the combination method introduced by Nelson and Oppen. However, in its initial presentation, the Nelson-Oppen combination method requires the theories to be signature-disjoint and stably infinite (to guarantee the existence of an infinite model). The notion of gentle theory has been introduced in the last few years as one solution to go beyond the restriction of stable infiniteness, but in the case of disjoint theories. In this paper, we adapt the notion of gentle theory to the non-disjoint combination of theories sharing only unary predicates (plus constants and the equality). Like in the disjoint case, combining two theories, one of them being gentle, requires some minor assumptions on the other one. We show that major classes of theories, i.e. Löwenheim and Bernays-Schönfinkel-Ramsey, satisfy the appropriate notion of gentleness introduced for this particular non-disjoint combination framework.

Une douce et non-disjointe combinaison de procédures de satisfiabilité

Résumé :

Un problème de satisfiabilité est souvent exprimé dans un mélange de théories, et une approche naturelle consiste à résoudre le problème en combinant les procédures de satisfiabilité disponibles dans les théories composantes. C'est l'objet de la méthode de combinaison introduite par Nelson et Oppen. Toutefois, dans sa présentation initiale, la méthode de combinaison de Nelson-Oppen impose aux théories d'être à signatures disjointes et stablement infinies (pour garantir l'existence d'un modèle infini). La notion de théorie douce a été introduite ces dernières années comme une solution pour relacher la contrainte de stable infinité, mais uniquement dans le cas de théories disjointes. Dans ce papier, nous adaptons la notion de théorie douce à la combinaison non-disjointe de théories partageant les prédicats unaires (plus les constantes et l'égalité). Comme dans le cas disjoint, combiner deux théories, l'une d'elles étant douce, nécessite des hypothèses mineures sur l'autre théorie. On montre que les théories de Löwenheim et les théories de Bernays-Schönfinkel-Ramsey sont douces au sens introduit dans ce cadre particulier de combinaison non-disjointe.

Mots-clés : Problème de satisfiabilité, méthode de combinaison, mélange de théories nondisjointes

Introduction

The design of satisfiability procedures has attracted a lot of interest in the last decade due to their ubiquity in SMT (Satisfiability Modulo Theories [START_REF] Barrett | Satisfiability modulo theories[END_REF]) solvers and automated reasoners. A satisfiability problem is very often expressed in a combination of theories, and a very natural approach consists in solving the problem by combining the satisfiability procedures available for each of them. This is the purpose of the combination method introduced by Nelson and Oppen [START_REF] Nelson | Simplification by cooperating decision procedures[END_REF]. In its initial presentation, the Nelson-Oppen combination method requires the theories in the combination to be (1) signature-disjoint and (2) stably infinite (to guarantee the existence of an infinite model). These are strong limitations, and many recent advances aim to go beyond disjointness and stable infiniteness. Both corresponding research directions should not be opposed. In both cases, the problems are similar, i.e. building a model of T 1 ∪ T 2 from a model of T 1 and a model of T 2 . This is possible if and only if there exists an isomorphism between the restrictions of the two models to the shared signature [START_REF] Tinelli | Unions of non-disjoint theories and combinations of satisfiability procedures[END_REF]. The issue is to define a framework to enforce the existence of this isomorphism. In the particular case of disjoint theories, the isomorphism can be obtained if the domains of the models have the same cardinality, for instance infinite; several classes of kind theories (shiny [START_REF] Tinelli | Combining non-stably infinite theories[END_REF], polite [START_REF] Ranise | Combining data structures with nonstably infinite theories using many-sorted logic[END_REF], gentle [START_REF] Fontaine | Combinations of theories for decidable fragments of first-order logic[END_REF]) have been introduced to enforce a (same) domain cardinality on both sides of the combination. For extensions of Nelson-Oppen to non-disjoint cases, e.g. in [START_REF] Tinelli | Unions of non-disjoint theories and combinations of satisfiability procedures[END_REF][START_REF] Zarba | Combining sets with cardinals[END_REF], cardinality constraints also arise. In this paper, we focus on non-disjoint combinations for which the isomorphism can be simply constructed by satisfying some cardinality constraints. More precisely, we extend the notion of gentle theory to the non-disjoint combination of theories sharing only unary predicates (plus constants and the equality). Some major classes of theories fit in our non-disjoint combination framework.

Contributions. The first contribution is to introduce a class of P-gentle theories, to combine theories sharing a finite set of unary predicates symbols P. The notion of P-gentle theory extends the one introduced for the disjoint case [START_REF] Fontaine | Combinations of theories for decidable fragments of first-order logic[END_REF]. Roughly speaking, a P-gentle theory has nice cardinality properties not only for domains of models but also more locally for all Venn regions of shared unary predicates. We present a combination method for unions of P-gentle theories sharing P. The proposed method can also be used to combine a P-gentle theory with another arbitrary theory for which we assume the decidability of satisfiability problems with cardinality constraints. This is a natural extension of previous works on combining non-stably infinite theories, in the straight line of combination methods à la Nelson-Oppen. Two major classes of theories are P-gentle, namely the Löwenheim and Bernays-Schönfinkel-Ramsey (BSR) classes.

We characterize precisely the cardinality properties satisfied by Löwenheim theories. As a side contribution, bounds on cardinalities given in [START_REF] Dreben | The Decision Problem: Solvable Classes of Quantificational Formulas[END_REF] have been improved, and we prove that our bounds are optimal. Our new result establishes that Löwenheim theories are P-gentle.

We prove that BSR theories are also P-gentle. This result relies on a non-trivial extension of Ramsey's Theorem on hypergraphs. This extension should be considered as another original contribution, since it may be helpful as a general technique to construct a model preserving the regions.

Related Work. Our combination framework is a way to combine theories with sets. The relation between (monadic) logic and sets is as old as logic itself, and this relation is particularly clear for instance considering Aristotle Syllogisms. It is however useful to again study monadic logic, and more particularly the Löwenheim class, and more particularly with the recent advances in combinations with non-disjoint and non-stably infinite theories.

In [START_REF] Wies | Combining theories with shared set operations[END_REF], the authors focus on the satisfiability problem of unions of theories sharing set operations. The basic idea is to reduce the combination problem into a satisfiability problem in a fragment of arithmetic called BAP A (Boolean Algebra and Presburger Arithmetic). Löwenheim and BSR classes are also considered, but infinite cardinalities were somehow defined out of their reduction scheme, whilst infinite cardinalities are smoothly taken into account in our combination framework. In [START_REF] Wies | Combining theories with shared set operations[END_REF], BSR was shown to be reducible to Presburger. We here give a detailed proof. We believe such a proof is useful since it is more complicated that it may appear. In particular, our proof is based on an original (up to our knowledge) extension of Ramsey's Theorem to accommodate a domain partitioned into (Venn) regions. Finally, the notion of P-gentleness defined and used here is stronger than semi-linearity of Venn-cardinality, and allows non-disjoint combination with more theories, e.g. the guarded fragment.

In [START_REF] Sofronie-Stokkermans | Locality results for certain extensions of theories with bridging functions[END_REF][START_REF] Sofronie-Stokkermans | On combinations of local theory extensions[END_REF], a locality property is used to properly instantiate axioms connecting two disjoint theories. Hence, the locality is a way to reduce (via instantiation) a non-disjoint combination problem to a disjoint one. In that context, cardinality constraints can occur with bridging functions over a data structure having some cardinality constraints on the underlying theory of elements [START_REF] Zhang | Decision procedures for term algebras with integer constraints[END_REF][START_REF] Sofronie-Stokkermans | Locality results for certain extensions of theories with bridging functions[END_REF][START_REF] Suter | Decision procedures for algebraic data types with abstractions[END_REF].

In [START_REF] Ghilardi | Model-theoretic methods in combined constraint satisfiability[END_REF], Ghilardi proposed a very general model-theoretic combination framework to obtain a combination method à la Nelson-Oppen when T 1 and T 2 are two compatible extensions of the some shared theory T 0 (satisfying some properties). This framework relies on an application of the Robinson Joint Consistency Theorem (roughly speaking, the union of theories is consistent if the intersection is complete). Using this framework, several shared fragments of arithmetic have been successfully considered [START_REF] Ghilardi | Model-theoretic methods in combined constraint satisfiability[END_REF][START_REF] Nicolini | Combinable extensions of Abelian groups[END_REF][START_REF] Nicolini | Combining satisfiability procedures for unions of theories with a shared counting operator[END_REF]. Due to its generality, Ghilardi's approach is free of cardinality constraints.

It is also possible to consider a general semi-decision procedure for the unsatisfiability problem modulo T 1 ∪T 2 , e.g a superposition calculus. With the rewrite-based approach initiated in [START_REF] Armando | A rewriting approach to satisfiability procedures[END_REF], the problem reduces to proving the termination of this calculus. General criteria have been proposed to get modular termination results for superposition, when T 1 and T 2 are either disjoint [START_REF] Armando | New results on rewrite-based satisfiability procedures[END_REF] or non-disjoint [START_REF] Ringeissen | Modular termination and combinability for superposition modulo counter arithmetic[END_REF]. Notice that the superposition calculus can also be used as a deductive engine to entail some cardinality constraints, as shown in [START_REF] Bonacina | Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures[END_REF].

Structure of the paper. Section 2 introduces some classical notations and definitions. In Section 3, we introduce the notion of P-gentle theory and we present the related combination method for unions of theories sharing a (non-empty finite) set P of unary predicate symbols. All the theories in the Löwenheim class and in the BSR class are P-gentle, as shown respectively in Section 4 and in Section 5. A simple example is given in Section 6. The conclusion (Section 7) discusses the current limitations of our approach and mentions some possible directions to investigate. Our extension of Ramsey's Theorem can be found in Appendix A.

Notation and Basic Definitions

A first-order language is a tuple L = V, F, P such that V is an enumerable set of variables, while F and P are sets of function and predicate symbols. Every function and predicate symbol is assigned an arity. Nullary predicate symbols are called proposition symbols, and nullary function symbols are called constant symbols. A first-order language is called relational if it only contains function symbols of arity zero. A relational formula is a formula in a relational language. Terms, atomic formulas and first-order formulas over the language L are defined in the usual way. In particular an atomic formula is either an equality, or a predicate symbol applied to the right number of terms. Formulas are built from atomic formulas, Boolean connectives (¬, ∧, ∨, ⇒, Inria ≡), and quantifiers (∀, ∃). A literal is an atomic formula or the negation of an atomic formula. Free variables are defined in the usual way. A formula with no free variables is closed, and a formula without variables is ground. A universal formula is a closed formula ∀x 1 . . . ∀x n .ϕ where ϕ is quantifier-free. A (finite) theory is a (finite) set of closed formulas. Two theories are disjoint if no predicate symbol in P or function symbol in F appears in both theories, except constants and equality.

An interpretation I for a first-order language L provides a non empty domain D, a total function I[f ] : D r → D for every function symbol f of arity r, a predicate I[p] ⊆ D r for every predicate symbol p of arity r, and an element I[x] ∈ D for every variable x. The cardinality of an interpretation is the cardinality of its domain. The notation I x1/d1,...,xn/dn for x 1 , . . . , x n different variables stands for the interpretation that agrees with I, except that it associates d i ∈ D to the variable x i , 1 ≤ i ≤ n. By extension, an interpretation defines a value in D for every term, and a truth value for every formula. We may write I |= ϕ whenever I[ϕ] = ⊤. Given an interpretation I on domain D, the restriction I ′ of I on D ′ ⊆ D is the unique interpretation on D ′ such that I and I ′ interpret predicates, functions and variables the same way on D ′ . An extension I ′ of I is an interpretation on a domain D ′ including D such that I ′ restricted to D is I.

A model of a formula (or a theory) is an interpretation that evaluates the formula (resp. every formula in the theory) to true. A formula or theory is satisfiable if it has a model, and it

is unsatisfiable otherwise. A formula G is T -satisfiable if it is satisfiable in the theory T , that is, if T ∪ {G} is satisfiable. A T -model of G is a model of T ∪ {G}. A formula G is T -unsatisfiable if it has no T -models.
In our context, a theory T is decidable if the T -satisfiability problem for sets of ground literals in the language of T is decidable.

Consider an interpretation I on a language with unary predicates p 1 , . . . , p n and some elements D in the domain of this interpretation. Every element d ∈ D belongs to a Venn region v(d) = v 1 . . . v n ∈ {⊤, ⊥} n where v i = I[p i ](d). We denote by D v ⊆ D the set of elements of D in the Venn region v. Notice also that, for a language with n unary predicates, there are 2 n Venn regions. Given an interpretation I, D c denotes the subset of elements in D associated to constants by I. Naturally, D c v denotes the set of elements associated to constants that are in the Venn region v.

Gentle Theories Sharing Unary Predicates

From now on, we assume that P is a non-empty finite set of unary predicates. A P-union of two theories T 1 and T 2 is a union sharing only P, a set of constants and the equality. There are only a finite number of arrangements for given sets S and P.

Given a theory T whose signature includes P and a model M of T on domain D, the Pcardinality κ is the tuple of cardinalities of all Venn regions of P in M (κ v will denote the cardinality of the Venn region v). The following theorem (specialization of general combination lemmas in e.g. [START_REF] Tinelli | Unions of non-disjoint theories and combinations of satisfiability procedures[END_REF][START_REF] Tinelli | Combining non-stably infinite theories[END_REF]) states the completeness of the combination procedure for P-unions of theories:

Theorem 1 Consider a P-union of theories T 1 and T 2 whose respective languages L 1 and L 2 share a finite set S of constants, and let L 1 and L 2 be sets of literals, respectively in L 1 and L 2 .

Then L 1 ∪ L 2 is T 1 ∪ T 2 -satisfiable if and only if there exist an arrangement A for S and P, and a T i -model M i of A ∪ L i with the same P-cardinality for i = 1, 2.

The spectrum of a theory T is the set of P-cardinalities of its models. The above theorem can thus be restated as:

Corollary 1 The T 1 ∪ T 2 -satisfiability problem for sets of literals is decidable if, for any sets of literals A∪L 1 and A∪L 2 it is possible to decide if the intersection of the spectrums of T 1 ∪A∪L 1 and of T 2 ∪ A ∪ L 2 is non-empty.

To characterize the spectrum of the decidable classes considered in this paper, we introduce the notion of cardinality constraint. A finite cardinality constraint is simply a P-cardinality with only finite cardinalities. An infinite cardinality constraint is given by a P-cardinality κ with only finite cardinalities and a non-empty set of Venn regions V , and stands for all the P-cardinalities

κ ′ such that κ ′ v ≥ κ v if v ∈ V , and κ ′ v = κ v otherwise.
The spectrum of a finite set of cardinality constraints is the union of all P-cardinalities represented by each cardinality constraint. It is now easy to define the class of theories we are interested in: Definition 2 A theory T is P-gentle if, for every set L of literals in the language of T , the spectrum of T ∪ L is the spectrum of a computable finite set of cardinality constraints.

Notice that a P-gentle theory is (by definition) decidable. To relate the above notion with the gentleness in the disjoint case [START_REF] Fontaine | Combinations of theories for decidable fragments of first-order logic[END_REF], observe that if p is a unary predicate symbol not occurring in the signature of the theory T , then T ∪ {∀x.p(x)} is {p}-gentle if and only if T is gentle.

If a theory is P-gentle, then it is P ′ -gentle for any non-empty subset P ′ of P. It is thus interesting to have P-gentleness for the largest possible P. Hence, when P is not explicitly given for a theory, we assume that P denotes the set of unary predicates symbols occurring in its signature. In the following sections we show that the Löwenheim theories and the BSR theories are P-gentle.

The union of two P-gentle theories is decidable, as a corollary of the following modularity result:

Theorem 2 The class of P-gentle theories is closed under P-union.

Proof. If we consider the P-union of two P-gentle theories with respective spectrums S 1 and S 2 , then we can build some finite set of cardinality constraints whose spectrum is S 1 ∩ S 2 .

⊓ ⊔ Some very useful theories are not P-gentle, but in practical cases they can be combined with P-gentle theories. To define more precisely the class of theories T ′ that can be combined with a P-gentle one, let us introduce the T ′ -satisfiability problem with cardinality constraints: given a formula and a finite set of cardinality constraints, the problem amounts to check whether the formula is satisfiable in a model of T whose P-cardinality is in the spectrum of the cardinality constraints. As a direct consequence of Corollary 1: Theorem 3 T ∪T ′ -satisfiability is decidable if T is P-gentle and T ′ -satisfiability with cardinality constraints is decidable.

Notice that T -satisfiability with cardinality constraints is decidable for most common theories, e.g. the theories handled in SMT solvers. This gives the theoretical ground to add to the SMT solvers any number of P-gentle theories sharing unary predicates.

From the results in the rest of the paper, it will also follow that the non-disjoint union (sharing unary predicates) of BSR and Löwenheim theories, with one decidable theory accepting further Inria constraints of the form ∀x . ((¬)p 1 (x) ∧ . . . (¬)p n (x)) ⇒ (x = a 1 ∨ . . . x = a m ) is decidable. For instance, the guarded fragment with equality accepts such further constraints and the superposition calculus provides a decision procedure [START_REF] Ganzinger | A superposition decision procedure for the guarded fragment with equality[END_REF]. Thus any theory in the guarded fragment can be combined with Löwenheim and BSR theories sharing unary predicates.

In the disjoint case, any decidable theory expressed as a finite set of first-order axioms can be combined with a gentle theory [START_REF] Fontaine | Combinations of theories for decidable fragments of first-order logic[END_REF]. Here this is not the case anymore. Indeed, consider the theory ψ = ϕ ∨ ∃x p(x) where p does not occur in ϕ; any set of literals is satisfiable in the theory ψ if and only if it is satisfiable in the theory of equality. If the satisfiability problem of literals in the theory ϕ is undecidable, the P-union of ψ and the Löwenheim theory ∀x ¬p(x) will also be undecidable.

The Löwenheim Class

We first review some classical results about this class and refer to [START_REF] Börger | The Classical Decision Problem[END_REF] for more details. A Löwenheim theory is a finite set of closed formulas in a relational language containing only unary predicates (and no functions except constants). This class is also known as first-order relational monadic logic. Usually one distinguishes the Löwenheim class with and without equality. The Löwenheim class has the finite model property (and is thus decidable) even with equality. Full monadic logic without equality, i.e. the class of finite theories over a language containing symbols (predicates and functions) of arity at most 1, also has the finite model property. Considering monadic logic with equality, the class of finite theories over a language containing only unary predicates and just two unary functions is already undecidable. With only one unary function, however, the class remains decidable [START_REF] Börger | The Classical Decision Problem[END_REF], but does not have the finite model property anymore. Since the spectrum for this last class is significantly more complicated [START_REF] Gurevich | Spectra of monadic second-order formulas with one unary function[END_REF] than for the Löwenheim class we will here only focus on the Löwenheim class with equality (only classes with equality are relevant in our context), that is, without functions. More can be found about monadic first-order logic in [START_REF] Börger | The Classical Decision Problem[END_REF][START_REF] Dreben | The Decision Problem: Solvable Classes of Quantificational Formulas[END_REF]. In particular, a weaker version of Corollary 2 (given below) can be found in [START_REF] Dreben | The Decision Problem: Solvable Classes of Quantificational Formulas[END_REF].

Previously [START_REF] Fontaine | Combinations of theories for decidable fragments of first-order logic[END_REF][START_REF] Areces | Combining theories: The Ackerman and Guarded fragments[END_REF], combining theories with non-stably infinite theories took advantage of "pumping" lemmas, allowing -for many decidable fragments -to build models of arbitrary large cardinalities. The following theorem is such a pumping lemma, but it considers the cardinalities of the Venn regions and not only the global cardinality.

Lemma 1 Assume T is a Löwenheim theory with equality. Let q be the number of variables in T . If there exists a model M on domain D with |D v \ D c | ≥ q, then, for each cardinality q ′ ≥ q, there is a model extension or restriction

M ′ of M on domain D ′ such that |D ′ v \ D c | = q ′ and D ′ v ′ = D v ′ for all v ′ = v. Proof.
Two interpretations I (on domain D) and I ′ (on domain D ′ ) for a formula ψ are similar if

• |(D v ∩ D ′ v ) \ D c | ≥ q; • D v ′ = D ′ v ′ for each Venn region v ′ distinct from v; • I[a] = I ′ [a]
for each constant in ψ;

• I[x] = I ′ [x]
for each variable free in ψ.

Considering M as above, we can build a model M ′ as stated in the theorem, such that M and M ′ are similar. Indeed similarity perfectly defines a model with respect to another, given the cardinalities of the Venn regions.

We now prove that, given a Löwenheim formula ψ (or a set of formulas), two similar interpretations for ψ give the same truth value to ψ and to each sub-formula of ψ.

The proof is by induction on the structure of the (sub-)formula ψ. It is obvious if ψ is atomic, since similar interpretations assign the same value to variables and constants. If ψ is ¬ϕ 1 , ϕ 1 ∨ϕ 2 , ϕ 1 ∧ ϕ 2 or ϕ 1 ⇒ ϕ 2 , the result holds if it also holds for ϕ 1 and ϕ 2 .

Assume I makes true the formula ψ = ∃x ϕ(x). Then there exists some d ∈ D such that

I x/d is a model of ϕ(x). If d ∈ D ′ , then I ′
x/d is similar to I x/d and, by the induction hypothesis, it is a model of ϕ(x);

I ′ is thus a model of ψ. If d / ∈ D ′ , then d ∈ D v and |(D v ∩ D ′ v ) \ D c | ≥ q.
Furthermore, since the whole formula contains at most q variables, ϕ(x) contains at most q -1 free variables besides x. Let x 1 , . . . , x m be those variables. There exists some

d ′ ∈ (D v ∩ D ′ v ) \ D c such that d ′ = I[x i ]
for all i ∈ {1, . . . , m}. By structural induction, it is easy to show that I x/d and I x/d ′ give the same truth value to ϕ(x). Furthermore I x/d ′ and I ′

x/d ′ are similar. I ′ is thus a model of ψ. To summarize, if I is a model of ψ, I ′ is also a model of ψ. By symmetry, if I ′ is a model of ψ, I is also a model of ψ. The proof for formulas of the form ∀x ϕ(x) is dual. ⊓ ⊔ Lemma 1 has the following consequence on the acceptable cardinalities for the models of a Löwenheim theory:

Corollary 2 Assume T is a Löwenheim theory with equality with n distinct unary predicates. Let r and q be respectively the number of constants and variables in T . If T has a model of some cardinality κ strictly larger than r + 2 n max(0, q -1), then T has models of each cardinality equal or larger than min(κ, r + q 2 n ).

Proof. If a model with such a cardinality exists, then there are Venn regions v such that |D v \ D c | ≥ q. Then the number of elements in these Venn regions can be increased to any arbitrary larger cardinality, thanks to Lemma 1. If κ > r + q 2 n , it means some Venn regions v are such that |D v \ D c | > q, and by eliminating elements in such Venn regions (using again Lemma 1), it is possible to obtain a model of cardinality r + q 2 n . ⊓ ⊔

In [START_REF] Dreben | The Decision Problem: Solvable Classes of Quantificational Formulas[END_REF], the limit is q 2 n , q being the number of constants plus the maximum number of nested quantifiers. Now q is more precisely set to the number of variables, and the constants are counted separately. Moreover, max(0, q -1) replaces the factor q.

The case where q and r are both 0 corresponds to pure propositional logic (Löwenheim theories without variables and constants), where the size of the domain is not relevant. With q = 1 (one variable), there is no way to compare two elements (besides the ones associated to constants) and enforce them to be equal. It is still possible to constrain the domain to be of size at most r, using constraints like ∀x . x = c 1 ∨ . . . ∨ x = c r , but any model with one element not associated to a constant can be extended to a model of arbitrary cardinality (by somehow duplicating any number of time this element). Notice also that it is possible to set a lower bound on the size of the domain that can be r + 2 n . Consider for instance a set of sentences of the form ∃x.(¬)p 1 (x) ∨ . . . (¬)p n (x); there are 2 n such formulas, each enforcing one Venn region to be non-empty.

Using several variables, a Löwenheim formula can enforce upper bounds larger than r on cardinalities. For q = 2, it is indeed easy to build a formula that has only models of cardinality at most (q -1) 2 n = 2 n : ∀x∀y .

0<i<j≤n p i (x) = p j (y) ⇒ x = y.

Inria

With a larger number of variables, the following formula (q ≥ 2)

∀x 1 . . . ∀x q . 0<i<j≤n 0<i ′ <j ′ ≤q p i (x i ′ ) = p j (x j ′ ) ⇒ 0<i ′ <j ′ ≤q x i ′ = x j ′
enforces the cardinality of the domain to be at most (q-1) 2 n . To obtain a formula with constants that accepts only models of cardinality up to r + 2 n max(0, q -1), it suffices to add as a guard in the above formula the conjunctive sets of atoms expressing that the variables are disjoint from the r constants. So the above condition in Corollary 2 is the strongest one.

Besides the finite model property and the decidability of Löwenheim theories, Corollary 2 also directly entails the P-gentleness: Theorem 4 Löwenheim theories on a language with unary predicates in P are P-gentle.

The Bernays-Schönfinkel-Ramsey Class

A Bernays-Schönfinkel-Ramsey (BSR for short) theory is a finite set of formulas of the form ∃ * ∀ * ϕ, where ϕ is a first-order formula which is function-free (but constants are allowed) and quantifier-free. Bernays and Schönfinkel first proved the decidability of this class without equality; Ramsey later proved that it remains decidable with equality. More can be found about BSR theories in [START_REF] Börger | The Classical Decision Problem[END_REF]. Ramsey also gave some (less known) results about the spectrum of BSR theories [START_REF] Ramsey | On a Problem of Formal Logic[END_REF]. We here give a proof that BSR theories are P-gentle.

For simplicity, we will assume that existential quantifiers are Skolemized. In the following, a BSR theory is thus a finite set of universal function-free closed first-order formulas. ⊓ ⊔ Intuitively, this states that the elements not assigned to ground terms (i.e. the constants) can be eliminated from a model of a BSR theory. It is known [START_REF] Ramsey | On a Problem of Formal Logic[END_REF][START_REF] Fontaine | Combinations of theories for decidable fragments of first-order logic[END_REF] that for any BSR theory T there is a computable finite number k such that if T has a model of cardinality greater or equal to k, then it has a model of any cardinality larger than k. Later in this section, we prove that the same occurs locally for each Venn region.

The notion of n-repetitive models, which we now define, is instrumental for this. Informally, a model is n-repetitive if it is symmetric for those elements of its domain that are not assigned to constants in the theory.

-|{d 1 , . . . , d r } \ D c | ≤ n RR n°8529 -d ′ i = d i if d i or d ′ i ∈ D c ∪ v / ∈V D v -v(d ′ i ) = v(d i ) -d ′ i ≺ d ′ j iff d i ≺ d j , if for some v ′ ∈ V , d i , d j ∈ D v ′ \ D c we have I[p](d 1 , . . . , d r ) = I[p](d ′ 1 , . . . , d ′ r
). Notice that a same interpretation can be n-repetitive for several Venn regions at the same time. Also, the above definition allows D v \ D c to be empty for every v / ∈ V . Previously [START_REF] Fontaine | Combinations of theories for decidable fragments of first-order logic[END_REF] (without distinguishing regions) we showed that one can decide if a BSR theory T is n-repetitive by building another BSR theory that is satisfiable if and only if T is n-repetitive. The same occurs to n-repetitiveness for Venn regions.

Theorem 5 Consider a BSR theory T with n variables and a model M on domain D. If M is n-repetitive for the Venn regions V then, for any (finite or infinite) cardinalities

κ v ≥ |D v | (v ∈ V ), T has a model M ′ extension of M on domain D ′ such that |D ′ v | = κ v if v ∈ V and D ′ v ′ = D v ′ for all v ′ / ∈ V .
Proof. Assume that ≺ are the total orders mentioned in Definition 3. We first build an extension M ′ of M as specified in the theorem, and later prove it is a model of T . Let E be the set of new elements E = D ′ \ D, and fix arbitrary total orders (again denoted by ≺) on D ′ v \ D c for all v ∈ V that extend the given orders on D v \ D c . Since M ′ is an extension of M, the interpretation of the predicate symbols is already defined when all arguments belong to D. When some arguments belong to E, the truth value of an r-ary predicate p is defined as follows:

• (d ′ 1 , . . . , d ′ r ) ∈ M ′ [p] for |{d ′ 1 , . . . , d ′ r } \ D c | > n:
the interpretation of p over tuples with more than n elements outside D c is fixed arbitrarily. Indeed, such tuples are irrelevant for the evaluation of the formulas of T : terms occurring as arguments of a predicate are either variables or constants, and no more than n variables occur in any formula of T .

• otherwise, to determine

M ′ [p](d ′ 1 , . . . , d ′ r ), first choose d 1 , . . . d r ∈ D such that d ′ 1 , . . . , d ′ r
and d 1 , . . . d r are related to each other just like in Definition 3. This is possible since, for every Venn region v for which the interpretation is repetitive, there are at least n elements in

D v \ D c . Then (d ′ 1 , . . . , d ′ r ) ∈ M ′ [p] iff (d 1 , . . . , d r ) ∈ M[p].
Observe that all possible choices of d 1 , . . . , d n lead to the same definition because M is n-repetitive.

The construction is such that M ′ is also n-repetitive for the same regions. It is also a model of T : all formulas in T are of the form ∀x 1 . . . x m . ϕ(x 1 , . . . , x m ), with m ≤ n. For all d

′ 1 . . . , d ′ m ∈ D ′ , if {d ′ 1 , . . . , d ′ m } ⊆ D then M ′ x1/d ′ 1 ,...,xm/d ′ m [ϕ(x 1 , . . . , x m )] = M x1/d ′ 1 ,...,xm/d ′ m [ϕ(x 1 , . . . , x m )] since M ′ is an extension of M. Otherwise, let d 1 , . . . , d m ∈ D be some elements related to d ′ 1 , . . . , d ′ m like in Definition 3. Since M ′ is n-repetitive, M ′ x1/d ′ 1 ,...,xm/d ′ m [ϕ(x 1 , . . . , x m )] = M ′ x1/d1,...,xm/dm [ϕ(x 1 , . . . , x m )] = M x1/d1,...,xm/dm [ϕ(x 1 , . . . , x m )]. In both cases, M ′ x1/d ′ 1 ,...,xm/d ′ m
[ϕ(x 1 , . . . , x m )] evaluates to true, and therefore M ′ is a model of ∀x 1 . . . x n . ϕ(x 1 , . . . , x m ).

⊓ ⊔

Inria

Now it is possible to state that the full spectrum of a BSR theory only depends on (a finite set of) P-cardinalities κ such that, for all Venn region v, κ v ≤ k for some finite cardinality k only depending on the theory. The proof requires an extension of Ramsey's Theorem which can be found in the appendix A. The BSR class obviously has the finite model property, and is decidable. Lemma 2 and Theorems 5 and 6 above also prove that BSR theories are (gentle and) P-gentle: Corollary 3 BSR theories on a language including unary predicates in P are P-gentle.

A simple constructive proof of this corollary would consider the finite number of all P-cardinalities κ such that κ v ≤ k (where k comes from Theorem 6). All such P-cardinalities can be understood as cardinality constraints, the extendable Venn regions being the ones for which κ v > k. Of course this construction is highly impractical, since it uses some kind of Ramsey numbers, known to be extremely large. In practice, we believe there are much better constructions: the important elements of the domain are basically only the ones associated to constants, and theoretical upper bounds are not met in non-artificial cases.

Example: Non-Disjoint Combination of Order and Sets

To illustrate the kind of theories that can be handled in our framework, consider a very simple yet informative example with a BSR theory defining an ordering < and augmented with clauses connecting the ordering < and the sets p and q (we do not distinguish sets and their related predicates):

T 1 =        ∀x. ¬(x < x) ∀x, y. (x < y ∧ y < z) ⇒ x < z ∀x, y. (p(x) ∧ ¬p(y)) ⇒ x < y ∀x, y. (q(x) ∧ ¬q(y)) ⇒ x < y and a Löwenheim theory T 2 = {∀x. (p(x) ∧ q(x)) ≡ x = c}
stating that the intersection of the sets p and q is the singleton {c}.

The first theory imposes either p ∩ q or p ∩ q to be empty (we will assume that the domain is non-empty and simplify the cardinality constraints accordingly). The second theory obviously imposes the cardinality of p ∩ q to be exactly 1. Notice that both theories are actually P-gentle. The following table collects the cardinality constraints:

T 1 T 2 p ∩ q ≥ 0 ≥ 0 ≥ 0 p ∩ q 0 ≥ 0 ≥ 0 p ∩ q ≥ 0 0 ≥ 0 p ∩ q ≥ 0 ≥ 0 1
Assume now that we have two literals p(a), q(b) (these can again be considered as a further non-disjoint theory). Since either p ∩ q or p ∩ q is empty, either a or b belongs to the intersection p ∩ q. Hence, the set

T 1 ∪ T 2 ∪ {p(a), q(b), a = c, b = c} is unsatisfiable.
As a final comment, there could be theories using directly the Venn cardinalities as integer variables. Consider again T 1 ∪ T 2 , one could imagine a further constraint in another theory including linear arithmetic on integers that would state |p| > 1 and |q| > 1. This would of course be unsatisfiable with T 1 ∪ T 2 .

Conclusion

The notion of gentleness was initially presented as a tool to combine non-stably infinite disjoint theories. In this paper, we have introduced a notion of P-gentleness which is well-suited for combining theories sharing (besides constants and the equality) only unary predicates in a set P. The major contributions of this paper are that the Löwenheim theories and BSR theories are P-gentle. A corollary is that the non-disjoint union (sharing unary predicates) of Löwenheim theories, BSR theories, and decidable theories accepting further constraints of the form ∀x . ((¬)p 1 (x) ∧ . . . (¬)p n (x)) ⇒ (x = a 1 ∨ . . . x = a m ) is decidable.

Our combination method is limited to shared unary predicates. Unfortunately, the theoretical limitations are strong for a framework sharing predicates with larger arities: for instance even the guarded fragment with two variables and transitivity constraints is undecidable [START_REF] Ganzinger | The two-variable guarded fragment with transitive relations[END_REF], although the guarded fragment (or first-order logic with two variables) is decidable, and transitivity constraints can be expressed in BSR. The problem of combining theories with only a shared dense order has however been successfully solved [START_REF] Ghilardi | Model-theoretic methods in combined constraint satisfiability[END_REF][START_REF] Manna | Formal Methods at the Crossroads[END_REF]. In that specific case, there is again an implicit infiniteness argument that could be possibly expressed as a form of extended gentleness, to reduce the isomorphism construction problem into solving some appropriate extension of cardinality constraints. A clearly challenging problem is to identify an appropriate extended notion of gentleness for some particular binary predicates.

Also in future works, the reduction approach (Löwenheim and BSR theories can be simplified to a subset of Löwenheim) may be useful as a simplification procedure for sets of formulas that can be seen as non-disjoint (sharing unary predicates only) combinations of BSR, Löwenheim theories and an arbitrary first-order theory: this would of course not provide a decision procedure, but refutational completeness can be preserved. More generally we also plan to study how Inria superposition-based satisfiability procedures could benefit from a non-disjoint (sharing unary predicates) combination point of view. In particular, superposition-based satisfiability procedures could be used as deductive engines with the capability to exchange constraints la Nelson-Oppen.

The results here are certainly too combinatorially expensive to be directly applicable. However, this paper paves the theoretical grounds for mandatory further works that would make such combinations practical. There are important incentives since the BSR and Löwenheim fragments are quite expressive: for instance, it is possible to extend the language of SMT solvers with sets and cardinalities. Many formal methods are based on logic languages with sets. Expressive decision procedures (even if they are not efficient) including e.g. sets and cardinalities will help proving the often small but many verification conditions stemming from these applications.

• to build S i+1 , we first build a complete (n -1)-hypergraph on S i \ {e i } containing an (n -1)-hyperedge A for each hyperedge A ∪ {e i } of S i , and with the same color. Using the induction hypothesis, if |S i | R ≥ f (n -1, x), there is a subset S i+1 ⊆ S i \ {e i } such that |S i+1 | R ≥ x and the color of each hyperedge only depends on the number of its elements belonging to each region in the complete (n -1)-hypergraph on S i+1 .

The elements e i are chosen ordered by region. There are C(n + m -2, m) ways to put n -1 elements in m regions, so that there are 2 C(n+m-2,m) color patterns for (n -1)-hypergraphs with m regions. Consider the color patterns of the (n -1)-hypergraphs associated to the above elements e i . For each region, if there are 2 C(n+m-2,m) N elements e i above in this region, there will be one color pattern on which N elements agree. Let us select the N such elements for each region; by construction the n-subhypergraph on these elements is such that the color of each hyperedge containing an element in region R i only depends on the number of elements in each (other) region.

Consider two n-hyperedges or the same kind {e 1 , . . . e n }, {e ′ 1 , . . . e ′ n }. From the above construction, they have the same colors. Indeed take one element of the smallest region in both sets and assume (without loss of generality, it is e 1 and e ′ 1 . Since e 1 and e ′ 1 have been selected because they have the same color patterns for the (n -1)-hypergraph built from hyperedges containing e 1 and e ′ 1 , the two hyperedges should have the same color. It remains to give the size of S such that it is possible to pick 2 C(n+m-2,m) N elements e i for each of the m regions. Defining function g to be such that g( * ) = f (n -1, * ), it is sufficient to have |S 0 | R ≥ g mN 2 C(n+m-2,m) (n -1).

⊓ ⊔

Inria

Definition 1

 1 An arrangement A for finite sets of constant symbols S and unary predicates P is a maximal satisfiable set of equalities and inequalities a = b or a = b and literals p(a) or ¬p(a), with a, b ∈ S, p ∈ P.

Lemma 2

 2 Let T be a BSR theory, and M be a model of T on domain D. Then any restriction M ′ of M on domain D ′ with D c ⊆ D ′ ⊆ D is a model of T . Proof. Consider M and M ′ as above. Since M is a model of T , for each closed formula ∀x 1 . . . x n . ϕ in T (where ϕ is function-free and quantifier-free), and for all d 1 , . . . , d n ∈ D ′ ⊆ D, M x1/d1,...,xn/dn is a model of ϕ. This also means that, for all d 1 , . . . , d n ∈ D ′ , M ′ x1/d1,...,xn/dn is a model of ϕ, and finally that M ′ is a model of ∀x 1 . . . x n . ϕ.

Definition 3

 3 An interpretation I on domain D for a BSR theory T is n-repetitive for a set V of Venn regions if, for each v ∈ V , |D v \ D c | ≥ n and there exists a total order ≺ on elements in D v \ D c such that • for every r-ary predicate symbol p in T • for all d 1 , . . . , d r ∈ D, and d ′ 1 , . . . , d ′ r ∈ D with

Theorem 6

 6 Given a BSR theory T with n variables, there exists a number k computable from the theory, such that, if T has a model M on domain D such that |D v \ D c | ≥ k for Venn regions v ∈ V , then it has a model which is n-repetitive for Venn regions V .Proof. Using Lemma 2, we can assume that T has a (sufficiently large) finite model M on domain D. We can assume without loss of generality that M is such that, for every predicate p of the language, (d 1 , . . . d r ) / ∈ M[p] whenever there are more than n elements in {d 1 , . . . d r } \ D c ; indeed, these interpretations play no role in the truth value of a formula with n variables.Let ≺ be an order on D \ D c . Given two ordered (with respect to ≺) sequences e 1 , . . . , e n and e ′ 1 , . . . , e ′ n of elements inD \ D c such that v(e i ) = v(e ′ i ) (1 ≤ i ≤ n),we say that the configurations for e 1 , . . . , e n and e ′ 1 , . . . , e ′ n agree if for every r-ary predicate p, and for every d 1 , . . . , d r ∈ D c ∪ {e 1 , . . . , e n }, (d 1 , . . . , d r ) ∈ M[p] iff (d ′ 1 , . . . , d ′ r ) ∈ M[p], with d ′ i = e ′ j if d i = e j for some j, and d ′ i = d i otherwise. Notice that there are only a finite number of disagreeing configurations for n elements in D \ D c : more precisely a configuration is determined by at most b= p (n + |D c |)arity(p) Boolean values, where the sum ranges over all predicates in the theory.Thus the number of disagreeing configurations is bounded by C = 2 b . Interpreting configurations as colors, one can use the extension of Ramsey's Theorem given in Appendix A: according to Theorem 7, there is a computable function f such that, for anyN ∈ N, if |D \ D c | V ≥ f (n, N, C), then there exists a model on D ′ ⊆ D with |D ′ \ D c | V ≥ Nfor which configurations agree if they have the same number of elements in each Venn region of V . Taking N = n, this is actually building a n-repetitive restriction of M. ⊓ ⊔

  615 rue du Jardin Botanique CS20101 54603 Villers-lès-Nancy Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

RR n°8529

This work has been partially supported by the project ANR-13-IS02-0001-01 of the Agence Nationale de la Recherche, by the European Union Seventh Framework Programme under grant agreement no. 295261 (MEALS), and by the STIC AmSud MISMT

A An Extension of Ramsey's Theorem

We define an n-subset of S to be a subset of n elements of S. An n-hypergraph of S is a set of nsubsets of S. In particular, a 2-hypergraph is an (undirected) graph. The complete n-hypergraph of S is the set of all n-subsets of S, and its size is the cardinality of S. An n-hypergraph G is colored with c colors if there is a coloring function that assigns one color to every n-subset in G. In particular, a colored 2-hypergraph (that is, a colored graph), is a graph where all edges are assigned a color. Consider a set S of elements partitioned into disjoint regions R = {R 1 , . . . R m }. We say that a set S ′ ⊆ S has region size larger than x and note

x for all i ∈ {1, . . . , m}. We also say that an n-hypergraph is region-monochromatic if the color of each hyperedge only depends on the number of elements belonging to each region. Two hyperedges are said of the same kind if they have the same number of elements in each region; all hyperedges of the same kind of a region-monochromatic hypergraph thus have the same color. The following extension 1 of Ramsey's Theorem holds:

Theorem 7 There exists a computable function f such that,

• for every number of colors c

Proof. We proceed by induction on c and n. A suitable function is defined recursively. Notice first that f (n, N, 1) = N , since an n-hypergraph colored with a unique color is monochromatic. When c > 2, one can rely on the case for c = 2. Indeed, we consider the following series (0 ≤ i ≤ n)

• the colors c i (i < n), all different and in the set of original colors;

• the sets of colors b i and w i , with b 0 = ∅, w 0 is the set of original colors, b i+1 = b i ∪ {c i }, w i+1 = w i \ {c i };

• the set of nodes S i such that S 0 = S, S i+1 ⊆ S i . The set of nodes S i is the set of nodes of a region-monochromatic hypergraph, considering all colors in b i as one color, and all colors in w i as another.

To build the sets S i , it is only necessary to compute region-monochromatic hypergraphs with 2 colors (b i and w i ). Notice that, if a kind of hyperedge in S i has a color in b i , then this will also hold for S j with j > i. Since b n is the set of original colors, the hypergraph on S n is regionmonochromatic with the original colors. Defining function g to be such that g

In the rest of the proof, we just omit the last argument of f and consider there are only two colors b, w. We compute f (n, N ) (standing for f (n, N, 2) above).

We now proceed by induction on the first argument of f . Assume G is a complete nhypergraph of S colored by two colors. We build the sequences S i and e i such that

• e i is any element in S i 1 The classical Ramsey's Theorem is the case with only one region.

RR n°8529