Keywords: procédure de décision, satisfiabilité, complétude de déduction, explication de l

Combinaison de théories convexes: modularité, complétude de déduction et explication

Résumé : Les procédures sont des composants essentiels des prouveurs de théorèmes et des systèmes permettant de décider la satisfiabilité de contraintes.

Leur combinaison modulaire est du plus grand intérêt pour construire des systèmes efficaces, mais leur utilisation est souvent limitée par une interface pauvre se limitant à une réponse de la forme "sat/unsat". Dans ce papier, nous développons un cadre à base de règles pour la conception de schémas de coopération de telles procédures tout en maintenant la modularité de leurs interfaces.

Dans un premier temps, nous utilisons ce cadre à base de règles pour spécifier et prouver la correction des schémas de combinaison classiques de Nelson-Oppen et Shostak. Ensuite, nous introduisons le concept de procédures de satisfiabilité complètes vis-à-vis de la déduction, nous montrons comment les construire pour une large classe de théories et nous donnons un schéma pour les combiner de façon modulaire. Finalement, nous considérons le problème de la construction modulaire d'explications en cas d'insatisfiabilité, pour des mélanges de théories, grâce à la réutilisation de procédures engendrant des preuves pour les théories composant le mélange.

Introduction

Decision procedures and constraint solvers are key components in many systems, such as automated theorem provers, expert systems, and constraint logic programming (CLP) environments. Their interest is to significantly augment the degree of automation of the overall system, thereby reducing user's interaction. Indeed, integrating such reasoning components requires some ingenuity as the problems tackled by complex systems are usually (i) large, (ii) expressed over several domains, and (iii) the computed solutions may require some form of certification (e.g., for safety critical applications). In order to overcome these difficulties, we consider in this paper the following two issues:

1. the combination of decision procedures for signature-disjoint and convex theories, to address (ii), 2. the modularity of the computation of conflict sets or explanations of the results for such decision procedures, to address (i) and (iii).

In this work, we restrict our attention to convex theories, i.e. theories for which it is not necessary to derive disjunctions of equalities to ensure the completeness of the combination schemas. 1 The reason for this choice is twofold. On one hand, restricting to convex theories simplifies the technical developments and allows us to present the key ideas in a straightforward way. On the other hand, the recent trend to develop decision procedures for non-convex theories consists of integrating several complex reasoning modules. This is illustrated by the works of [START_REF] Bradley | What's decidable about arrays?[END_REF] or [START_REF] Ghilardi | Decision procedures for extensions of the theory of arrays[END_REF] for the (non-convex) theory of arrays where suitable instantiation strategies are used to reduce the satisfiability problem for arrays to several satisfiability problems in the theory of equality, which is again convex. In the light of this observation, we believe that focusing on convex theories is not too restrictive.

Let us explain in more details our contributions to each issue.

Issue 1: combination. Research on the combination of decision procedures has been independently started in the early 80's by [START_REF] Nelson | Simplification by cooperating decision procedures[END_REF] and [START_REF] Shostak | Deciding combinations of theories[END_REF] for unions of theories with disjoint signatures. Each combination schema makes different assumptions on the properties the theories to be combined should satisfy. The former requires NO theories to have a satisfiability procedure and to be such that a satisfiable formula in a component theory T is also satisfiable in an infinite model of T (stable-infiniteness). The latter assumes that SH theories admit procedures for reducing terms to canonical form (canonizers) and algorithms for solving equations (solvers). A series of papers ( [START_REF] Cyrluk | On Shostak's decision procedure for combinations of theories[END_REF][START_REF] Rueß | Deconstructing Shostak[END_REF][START_REF] Barrett | A generalization of Shostak's method for combining decision procedures[END_REF][START_REF] Kapur | A rewrite rule based framework for combining decision procedures[END_REF][START_REF] Ganzinger | Shostak light[END_REF][START_REF] Conchon | Canonization for disjoint unions of theories[END_REF][START_REF] Rueß | Combining shostak theories[END_REF][START_REF] Conchon | Strategies for combining decision procedures[END_REF][START_REF] Manna | Combining decision procedures[END_REF]) have clarified the subtle issues of combining SH theories by studying their relationships with NO theories. Some of them use pseudo-code to describe the combination algorithms while others adopt a more abstract rule-based presentation.

The first contribution of this paper (Section 3) is to provide a synthesis of Nelson-Oppen and Shostak approaches to disjoint combination by using a rule-based approach in which many recent results are recast and proved correct in a uniform, rigorous, and simple way. Our rational reconstruction proceeds as follows. First, we recall that SH theories are contained in the class of convex NO theories. According to this abstract classification, three possible scenarios are to be considered when combining two theories: (a) both are NO theories (Section 3.1), (b) both are SH theories (Section 3.2), and (c) one is a SH and the other is a NO theory (Section 3.3). We formalize the combination schema for each scenario as an inference system. The applicability conditions of the inference rules are derived from the properties of the theories being combined. Along the lines of [START_REF] Ganzinger | Shostak light[END_REF][START_REF] Manna | Combining decision procedures[END_REF][START_REF] Conchon | Strategies for combining decision procedures[END_REF], the combination schema for (b) is obtained as a refinement of that for (a). The inference system formalizing the combination schema for (c), already considered in [START_REF] Barrett | A generalization of Shostak's method for combining decision procedures[END_REF], is obtained by modularly reusing those for (a) and (b) in a natural and straightforward way. Our synthesis of combination schemas serves two purposes. First, although the results are not new, we believe that presenting them in a uniform framework can provide a valuable reference for people interested in combination problems, especially for non-experts of the field. Second, it can serve as starting point for further investigations. As an example, a problem of great importance when combining SH theories is the lack of modularity for solvers (see [START_REF] Conchon | Canonization for disjoint unions of theories[END_REF]): no general method exists to produce a solver for the union of SH theories from the solvers of the component theories. Furthermore, as it is well known (see e.g. [START_REF] Detlefs | Simplify: a theorem prover for program checking[END_REF]), to implement the Nelson-Oppen combination method efficiently, the satisfiability procedure for the component theories must be capable of deriving the formulas to exchange with other procedures. This is not obvious for satisfiability procedures in general since they may be incomplete for consequence finding, i.e. there is no guarantee that a formula which is a logical consequence of a set of literals will be eventually derived without resorting to guessing and refutation 2 . The lack of modularity for SH theories, together with the observation that the theory of equality (ubiquitous in virtually any application where combinations of decision procedures are needed) is not a SH theory, but admits an efficient algorithm to derive entailed equalities, seem to suggest a possible line of investigation. Any ad hoc combination schema for scenario (c) constitutes a reasonable trade-off between efficiency and generality: solvers and canonizers for SH theories efficiently derive new equalities and cooperate à la Nelson-Oppen. By investigating this question in our framework, we propose the concept of deduction completeness which constitutes the second contribution of this paper (Section 4). Intuitively, a deduction complete satisfiability procedure is a satisfiability procedure defined as an inference-based system with the capability of computing all the entailed elementary equalities with no overhead. We show that deduction complete inference-based satisfiability procedures can be constructed in a modular way (Section 4.2). Another interesting feature is that they can be efficiently built by reusing a wealth of existing techniques such as canonizers and solvers for SH theories and rewriting techniques, as advocated in [START_REF] Kapur | Shostak's congruence closure as completion[END_REF][START_REF] Bachmair | Abstract Congruence Closure[END_REF][START_REF] Armando | A Rewriting Approach to Satisfiability Procedures[END_REF][START_REF] Marché | Normalized rewriting: An alternative to rewriting modulo a set of equations[END_REF] for theories which do not admit a solver (Section 4.1).

Issue 2: modular computation of explanations. To efficiently and correctly incorporate decision procedures into deduction systems or constraint programming environments, the capability of explaining the results of the decision procedures is crucial. For example, conflict sets (explanation of unsatisfiability) are useful to prune the search space of Satisfiability Modulo Theories (SMT) solvers (see, e.g., [START_REF] Sebastiani | Lazy Satisfiability Modulo Theories[END_REF]) or to direct backtracking in CLP systems ( [START_REF] Burg | Intelligent Backtracking in CLP(R)[END_REF]), whereas explanations can be used to safely import the results of external reasoning modules (e.g., decision procedures for selected theories or unification algorithms) in skeptical proof assistants ([19]). While there has been some work on extending decision procedures for some theories, mainly equality, ( [START_REF] Fontaine | Techniques for Verification of Concurrent Systems with Invariants[END_REF][START_REF] De Moura | Justifying equality[END_REF][START_REF] Nieuwenhuis | Proof-Producing Congruence Closure[END_REF][START_REF] Stump | The Algebra of Equality Proofs[END_REF]), there is no paper, to the best of our knowledge, on the modular construction of conflict sets in unions of theories. Many SMT systems have implemented this capability somehow, but no one has offered a high level description of how this is done. So, implementors, when they want to build such a capability in their own SMT tool, are required to understand the code of other systems (and in many cases the code is not even available), abstract away unimportant implementation details, and finally adapt the ideas to their architecture.

The third contribution of this paper (Section 5) is to provide an abstract account of how to extend the Nelson-Oppen combination schema to build a satisfiability procedure capable of producing conflict sets in the union of theories T 1 and T 2 , whenever the satisfiability procedures for T 1 and T 2 provide some interface capabilities. To this end, we first introduce the concept of explanation graph (Section 5.2), a data structure which compactly encodes the fact that a certain equality between variables (called elementary equality) is a logical consequence of a set of elementary equalities. Explanation graphs can be easily implemented by using efficient algorithms based on the Union-Find data structure of [START_REF] Tarjan | Efficiency of a good but not linear set union algorithm[END_REF][START_REF] Downey | Variations on the common subexpression problem[END_REF]. Then we show how to derive explanation engines from satisfiability procedures that produce conflict sets in the union of the component theories. We also introduce the concept of quasi-conflict set, which allows us to precisely characterize a (weak) form of minimality satisfied by the explanations computed by our combination method.

Background

First-order theories

We assume the usual first-order syntactic notions of signature, term, position, and substitution. Let Σ be a first-order signature containing only function symbols with their arity and X a set of variables. A 0-ary function symbol is called a constant. A Σ-term is a first-order term built out of the symbols in Σ and the variables in X . We use the standard notion of substitution and denote them by the greek letter σ. We write substitution applications in postfix notation, i.e. tσ for a term t and a substitution σ. The set of variables occurring in a term t is denoted by V ar(t). If l and r are two Σ-terms, then l = r is a Σ-equality and ¬(l = r) (also written as l = r) is a Σ-disequality. If p is an n-ary predicate in Σ and t 1 , . . . , t n are Σ-terms, then p(t 1 , . . . , t n ) is a Σ-atom. A Σ-literal is either a Σ-equality or a Σ-disequality or a Σ-atom or a negation of a Σ-atom. A Σ-formula is built in the usual way out of the universal and existential quantifiers, Boolean connectives, and symbols in Σ. A clause is a disjunction of literals. A unit clause is a clause with only one disjunct, equivalently a literal. The empty clause is the clause with no disjunct, equivalently an unsatisfiable formula. If ϕ is a formula, then V ar(ϕ) denotes the set of free variables in ϕ. We call a formula ground if it has no variable, and a sentence if it has no free variables. Substitution applications are extended to arbitrary first-order formulas, and are written in postfix notation, i.e. ϕσ for a formula ϕ and a substitution σ. A term is flat if its depth is 0 or 1. For a literal, depth(l ⊲⊳ r) = depth(l) + depth(r), where ⊲⊳∈ {=, =}. A positive literal is flat if its depth is 0 or 1. A negative literal is flat if its depth is 0. A (dis)equality between two free constants is called elementary. A literal which is neither an elementary equality nor an elementary disequality is called non-elementary. In the following, ϕ or Φ denotes an arbitrary set of literals, Ω denotes a set of nonelementary literals, E denotes a set of elementary equalities, and ∆ denotes a set of elementary disequalities. E * is the set of all equalities derived from E by reflexivity, symmetry and transitivity. The set E of elementary equalities is

minimal iff E ′ * ⊂ E * , for any E ′ ⊂ E.
We also assume the usual first-order notions of interpretation, satisfiability, validity, logical consequence, and theory, as given for instance in [START_REF] Enderton | A Mathematical Introduction to Logic[END_REF]. We write |= α M ϕ when the Σ-formula ϕ is true in the Σ-structure M under the variable assignment α. We also say that α satisfies ϕ in M. A Σ-formula ϕ is valid in a Σ-structure M, denoted by M |= ϕ, if |= α M ϕ for any assignment of variables α. A first-order theory is a set of first-order sentences. A Σ-theory is a theory all of whose sentences have signature Σ. All theories we consider are firstorder theories with equality, which means that the equality symbol = is always interpreted as the identity relation. A Σ-structure M is a model of a Σ-theory T if every sentence in T is true in M. A theory is consistent if it admits a model and trivial if the cardinality of each of its models is one. In this paper, we restrict ourselves to non-trivial and consistent theories and will consider a few particular theories: the theory of equality E whose signature contains a finite set of function and constant symbols, and the equality symbol =; the quantifierfree fragment of Linear Rational Arithmetic denoted LA ≤ and its restriction to equalities or disequalities denoted LA. A Σ-formula ϕ is valid in T , denoted by T |= ϕ, if it is valid in any model of T . A Σ-formula is T -satisfiable if it is satisfiable in a model of T . Two Σ-formulas ϕ and ψ are equisatisfiable in T if for every model M of T , ϕ is satisfiable in M iff ψ is satisfiable in M. The satisfiability problem for a theory T amounts to establishing whether any given finite quantifier-free conjunction of literals (or equivalently, any given finite set of literals) is T -satisfiable or not. A satisfiability procedure for T is any algorithm that solves the satisfiability problem for T . 3 Note that we can use free constants instead of variables to equivalently redefine the satisfiability problem for T as the problem of establishing the consistency of T ∪ S for a finite set S of ground literals.

Given an inference system R composed of inference rules, the binary relation ⊢ R is defined on formulas as follows:

Φ ⊢ R Φ ′ if Φ ′ can be derived from Φ by applying a rule in R. A formula Φ ′ is said T -equivalent to Φ if V ar(Φ ′ ) ⊇ V ar(Φ) and T |= (Φ ⇔ ∃ỹ.Φ ′ ) where ỹ = V ar(Φ ′ )\V ar(Φ). The reflexive and transitive closure of ⊢ R , denoted by ⊢ * R , is called the derivation relation of R. Also, a derivation in R is a sequence Φ ⊢ R Φ ′ ⊢ R Φ ′′ ⊢ R • • • . A formula Φ is in normal form w.r.t. ⊢ R if there is no derivation in R starting from Φ. The relation ⊢ * R is terminating if there is no infinite derivation.
With such inference systems, it is convenient to identify a conjunctive formula with the set of its conjuncts and to group together specific literals. So the inference rules in the following will be applied on so-called configurations which are sets of formulas of the form Φ; Φ ′ where Φ and Φ ′ are unions of literals (identified with their conjunction). Whenever needed, Φ may be written as Γ, ∆ in order to emphasize that Γ is a set (a conjunction) of equalities, and ∆ is a set (conjunction) of disequalities.

Combination of theories

Let Σ 1 and Σ 2 be two disjoint signatures (i.e. Σ 1 ∩Σ 2 = ∅) and T i be a Σ i -theory for i = 1, 2. A Σ 1 ∪ Σ 2 -term t is an i-term if it is a variable or it has the form f (t 1 , ..., t n ), where f is in Σ i (for i = 1, 2 and n ≥ 0). Notice that a variable is both a 1-term and a 2-term. A non-variable subterm s of an i-term is alien if s is a j-term, and all superterms of s are i-terms, where i, j ∈ {1, 2} and i = j. An i-term is i-pure if it does not contain alien subterms. A literal is i-pure if it contains only i-pure terms. A formula is said to be pure if there exists i ∈ {1, 2} such that every term occurring in the formula is i-pure.

In this paper, we consider the problem of solving the satisfiability problem for T 1 ∪T 2 (i.e. the problem of checking the T 1 ∪T 2 -satisfiability of conjunctions of Σ 1 ∪ Σ 2 -literals) by using the satisfiability procedures for T 1 and T 2 . For certain theories, more basic algorithms exist which can be used to build satisfiability procedures, e.g. canonizers and solvers for the class of Shostak theories (see below for a formal definition). When such algorithms exist for either T 1 , T 2 , or both, we are interested in using them to solve the satisfiability problem for T 1 ∪ T 2 . In order to know which basic algorithms are available for T 1 and T 2 and what are the assumptions on T 1 and T 2 , the following notions and results are useful.

Let us remind that a conjunction Φ of Σ-literals is convex in a Σ-theory T iff for any disjunction n i=1 x i = y i (where x i , y i are variables and i = 1, ..., n) we have: T ∪ Φ |= n i=1 x i = y i iff T ∪ Φ |= x i = y i , for some i ∈ {1, ..., n}. A Σ-theory T is convex iff all conjunctions of Σ-literals are convex.

A Σ-theory T is stably-infinite (and called a SI-theory, for short) iff for any T -satisfiable Σ-formula ϕ, there exists a model of T whose domain is infinite and which satisfies ϕ. A Nelson-Oppen theory is a stably-infinite theory which admits a satisfiability algorithm. A C-theory is a convex theory. A CSI-theory is a convex stably-infinite theory. The class of C-theories (resp. SI-theories, CSI-theories) is denoted by C (resp. SI, CSI).

A solver for a Σ-theory T is a function (denoted solve) which takes as input a Σ-equality s = t and such that (a) solve(s = t) returns f alse, if T |= s = t, or (b) solve(s = t) returns a substitution σ = {x 1 → t 1 , ..., x n → t n } such that (b.1) x i is a variable occurring in s or t for i = 1, ..., n, (b.2) x i does not occur in any t j for i, j = 1, ..., n, and (b.3) T |= s = t ⇔ ∃ỹ. n i=1 x i = t i , where ỹ denotes the "fresh" variables y 1 , ..., y m (m ≥ 0) such that y k does not occur in s or t, for all k = 1, ..., m. A conjunction of Σ-equalities is in solved form iff it has the form n i=1 x i = t i , which will be denoted by σ, where σ = {x 1 → t 1 , ..., x n → t n } is the substitution returned by solve.

A canonizer for a Σ-theory T is an idempotent function (denoted canon) from Σ-terms to Σ-terms such that T |= a = b iff canon(a) = canon(b).

A Shostak theory is a convex theory which admits a solver and a canonizer. A SH-theory is a stably-infinite Shostak theory. The class of SH-theories is denoted by SH. Notice that LA is a SH-theory. We assume SH-theories to be stably-infinite since this is necessary to combine them with other theories as suggested by many recent papers (see e.g. [START_REF] Manna | Combining decision procedures[END_REF]). This is not too restrictive since, as shown in [START_REF] Barrett | A generalization of Shostak's method for combining decision procedures[END_REF], any convex theory with no trivial models is stably-infinite.

Proposition 1 SH ⊆ CSI ⊆ SI.

Rational reconstruction of combination schemas

Let T i be a Σ i -theory (i = 1, 2) such that Σ 1 ∩ Σ 2 = ∅. We consider the problem of building a satisfiability procedure for T 1 ∪ T 2 . As a preliminary step, we consider a purification process converting any conjunction Φ of Σ 1 ∪ Σ 2 -literals into a conjunction of pure literals. Such a process is achieved by replacing each alien subterm t by a new variable x and adding the equality x = t to Φ. This mechanism, called variable abstraction, is repeatedly applied to Φ until no more alien subterms t can be abstracted away. Obviously, the purification process always terminates yielding Φ 1 ∧ Φ 2 , where Φ i is a conjunction of Σ i -literals (i = 1, 2) such that Φ 1 ∧ Φ 2 and Φ are equisatisfiable in T 1 ∪ T 2 . Without loss of generality, we consider the satisfiability of formulas of the form Φ 1 ∧ Φ 2 (or, equivalently, of configurations Φ 1 ; Φ 2 ), where Φ i is a conjunction of i-pure literals.

Our combination schemas are specified by inference systems. To prove that an inference system R yields a satisfiability procedure, we follow a three steps methodology. First, we show that the derivation relation ⊢ R induced by R is terminating. Second, we prove that ⊢ R preserves (un-)satisfiability. Finally, we check that the normal forms defined by ⊢ R (i.e. configurations to which no rule in R can be applied) distinct from f alse must be satisfiable. The proof of the last step proceeds by contradiction showing that a normal form distinct from f alse cannot be unsatisfiable by using the following (technical) lemmas from which the proof of correctness of Nelson-Oppen schema in [START_REF] Tinelli | Unions of non-disjoint theories and combinations of satisfiability procedures[END_REF] essentially depends.

Let V be a set of variables and E be equivalence relation over V . We define the arrangements of V with respect to E, noted arr(V, E), to be the following set of equalities and disequalities:

{x = y | (x, y) ∈ E} ∪ {x = y | (x, y) ∈ (V × V ) \ E}.

Lemma 1 ([40]

). If T 1 and T 2 are two signature-disjoint theories, then any conjunction Φ 1 ∧ Φ 2 of pure quantifier-free formulas is T 1 ∪ T 2 -satisfiable if and only if there exists some equivalence relation E over shared variables in

V = V ar(Φ 1 ) ∩ V ar(Φ 2 ) such that Φ i ∪ arr(V, E) is T i -satisfiable in a model M i (for i = 1, 2)
and the two models have the same cardinality.

When the two theories are stably infinite, we get a specialisation of the previous result which is more operational since the requirement on the models cardinality is clearly satisfied.

Lemma 2 ([40]

). If T 1 and T 2 are two signature-disjoint stably-infinite theories, then any conjunction Φ 1 ∧ Φ 2 of pure quantifier-free formulas is T 1 ∪ T 2satisfiable if and only if there exists some equivalence relation E over shared variables in

V = V ar(Φ 1 ) ∩ V ar(Φ 2 ) such that Φ i ∪ arr(V, E) is T i -satisfiable for i = 1, 2. INRIA Contradiction 1 Φ 1 ; Φ 2 f alse if Φ 1 is T 1 -unsatisfiable Deduction 1 Φ 1 ; Φ 2 Φ 1 ; Φ 2 ∪ {x = y} if        Φ 1 is T 1 -satisfiable, Φ 1 ∧ x = y is T 1 -unsatisfiable, Φ 2 ∧ x = y is T 2 -satisfiable, and x, y ∈ V ar(Φ 1 ) ∩ V ar(Φ 2 )
Figure 1: The Inference System NO 1

Combining CSI-theories

We assume that T 1 and T 2 are in CSI, which requires satisfiability procedures for both T 1 and T 2 . Let us consider the inference system NO obtained as the union of NO 1 presented in Figure 1 and NO 2 obtained from NO 1 by symmetry. 4 NO takes configurations of the form Φ 1 ; Φ 2 where Φ i is a set of Σ i -literals (i = 1, 2). Rule Contradiction 1 reports the T 1 -unsatisfiability of Φ 1 (and hence of Φ 1 ∧ Φ 2 ), detected by the available satisfiability procedure. Rule Deduction 1 propagates equalities between shared variables detected in T 1 to T 2 (if they are not already known). The problem of checking whether the equality x = y is a logical consequence of T 1 ∪ Φ 1 is transformed into the problem of checking the T 1unsatisfiability of Φ 1 ∪ {x = y} in order to exploit the available satisfiability procedure.

Theorem 1 Let T 1 , T 2 be two signature-disjoint CSI-theories. Let NO be the inference system defined as the union NO 1 ∪ NO 2 , where NO 1 is depicted in Figure 1 and NO 2 is obtained from NO 1 by symmetry. The relation ⊢ *

NO is terminating and

Φ 1 ; Φ 2 ⊢ * NO f alse iff Φ 1 ∧ Φ 2 is T 1 ∪ T 2 -unsatisfiable.
Proof: Direct consequence of the three following Lemmas.

Lemma 3 (Termination) The relation ⊢ * NO is terminating.

Proof: If the rule Contradiction applies, the procedure terminates. The rule Deduction strictly decreases the number of equivalence classes of shared variables.

Lemma 4 (Soundness) The relation

⊢ NO preserves equisatisfiability in T 1 ∪ T 2 .
Proof: The soundness of the rule Contradiction is straightforward. Let us consider the rule Deduction.

If |= α M (Φ 1 ∪ Φ 2 ), the application conditions guarantee that T 1 ∪ Φ 1 |= x = y, implying α(x) = α(y). Thus |= α M (Φ 1 ∪ Φ 2 ∪ {x = y}). The converse is trivial Lemma 5 (Completeness) If Φ 1 ; Φ 2 is a normal form w.r.t. ⊢ NO different from f alse, then Φ 1 ∧ Φ 2 is T 1 ∪ T 2 -satisfiable.
Proof: If the procedure terminates without reporting f alse, the final configuration must be of the form Φ 1 ; Φ 2 such that:

❼ Φ i is T i -satisfiable for i = 1, 2 (otherwise Contradiction applies), ❼ ∀x, y ∈ V ar(Φ 1 ) ∩ V ar(Φ 2 ), T 1 |= Φ 1 ⇒ x = y iff T 2 |= Φ 2 ⇒ x = y (otherwise Deduction applies). Assume Φ 1 ∧ Φ 2 is T 1 ∪ T 2 -unsatisfiable. Consider the equivalence relation E over variables in V ar(Φ 1 ) ∩ V ar(Φ 2 ) such that (x, y) ∈ E iff T 1 |= Φ 1 ⇒ x = y and T 2 |= Φ 2 ⇒ x = y. By Lemma 2, if Φ 1 ∧ Φ 2 is T 1 ∪ T 2 -unsatisfiable, there exists i ∈ {1, 2} such that Φ i ∪ arr(V, E) is T i -unsatisfiable.
Then two cases must be distinguished:

❼ arr(V, E) contains at least a disequality. By convexity hypothesis, there exist some i and some disequality

x k = y k such that Φ i ∪ E ∪ {x k = y k } is T i -unsatisfiable, or equivalently T i ∪ Φ i ∪ E |= x k = y k . Therefore (x k , y k ) is in E, which is a contradiction. ❼ arr(V, E) contains no disequalities. Then Φ i ∪ arr(V, E) is Φ i ∪ E which is T i -equivalent to Φ i . Thus Φ i is T i -unsatisfiable, which is again a con- tradiction.
NO specifies only the essence of the Nelson-Oppen schema. Such a schema can be refined to increase efficiency. In the following, we will consider refinements of NO based on the separation of the input set of literals into disequalities and equalities and other literals. The convexity assumption allows us to have a theory-independent handling of disequalities. In addition, considering disequalities is useless to obtain the entailed elementary equalities needed in NO. This property paves the way of incorporating solvers and canonizers for theories in SH.

Lemma 6 Let T be a convex theory, Φ a T -satisfiable set of literals, and ∆ a set of elementary disequalities. Then

Φ ∧ ∆ is T -unsatisfiable iff there exists x = y ∈ ∆ such that T |= Φ ⇒ x = y.
Proof: (⇐) Trivial. (⇒) By expressing the convexity definition in terms of unsatisfiability.

Lemma 7 Let T be a convex theory, Φ a set of T -literals, and

∆ a set of T - disequalities. If Φ ∧ ∆ is T -satisfiable, then T |= (Φ ∧ ∆) ⇒ x = y iff T |= Φ ⇒ x = y. Proof: (⇐) Trivial. (⇒) Assume that T ∪Φ∪∆ |= x = y. Then T ∪Φ∪(∆∪{x = y}) is unsatisfiable. By convexity of T , either T ∪ Φ ∪ {x = y} is unsatisfiable or there exists a disequality s = t ∈ ∆ such that T ∪ Φ ∪ {s = t} is unsatisfiable.
In the first case, the Lemma is proved. In the second one, we obtain that Φ ∧ ∆ is T -unsatisfiable, and so we get a contradiction.

INRIA Solve -fail 1 Γ 1 , ∆ 1 ; Γ 2 , ∆ 2 f alse if solve 1 (Γ 1 ) = f alse Solve -success 1 Γ 1 , ∆ 1 ; Γ 2 , ∆ 2 σ 1 , ∆ 1 ; Γ 2 , ∆ 2 if Γ 1 is not in solved form, σ 1 = solve 1 (Γ 1 ) = f alse Contradiction 1 σ 1 , ∆ 1 ∪ {s = t}; Γ 2 , ∆ 2 f alse if canon 1 (sσ 1 ) = canon 1 (tσ 1 ) Deduction 1 σ 1 , ∆ 1 ; σ 2 , ∆ 2 σ 1 , ∆ 1 ; σ 2 ∪ {x = y}, ∆ 2 if    canon 1 (xσ 1 ) = canon 1 (yσ 1 ), canon 2 (xσ 2 ) = canon 2 (yσ 2 ), x, y ∈ V ar(σ 1 ) ∩ V ar(σ 2 )
Figure 2: The Inference System SH 1

Combining SH-theories

Let us assume that T 1 and T 2 are in SH, which requires a canonizer canon i and a solver solve i for each theory T i (i = 1, 2). Preliminary to the combination schema, we extend solvers to handle sets of equalities as follows: solve(∅) returns the identity substitution ǫ; solve

(Γ ∪ {s = t}) = f alse, if solve(s = t) = f alse; and solve(Γ ∪ {s = t}) = σ • solve(Γσ), if solve(s = t) = σ, where • denotes composition of substitutions.
Let us consider the inference system SH obtained as the union of SH 1 presented in Figure 2 and SH 2 obtained from SH 1 by symmetry. SH takes configurations of the form

Γ 1 , ∆ 1 ; Γ 2 , ∆ 2 , where Γ i is a set of Σ i -equalities and ∆ i is a set of Σ i -disequalities for i = 1, 2. Rule Solve -fail 1 reports the T 1 -unsatisfiability of Γ 1 (and hence of Γ 1 ∧ ∆ 1 ∧ Γ 2 ∧ ∆ 2 )
detected by solve 1 . Rule Solvesuccess 1 replaces the Σ 1 -equalities Γ 1 with their solved form which is obtained again by using solve 1 . This is important for the next two rules. Dealing with solved forms allows us to simply determine entailed equalities (possibly between shared variables, see Deduction 1 ) using canonizers. Hence, it is possible to lazily report unsatisfiability as soon as we find a disequality whose corresponding equality is entailed (see Contradiction 1 ). Indeed, convexity allows us to handle disequalities one by one.

Theorem 2 Let T 1 , T 2 be two signature-disjoint SH-theories. Let SH be the inference system defined as the union SH 1 ∪ SH 2 , where SH 1 is depicted in Figure 2 and SH 2 is obtained by symmetry. The relation ⊢ * SH is terminating and

Γ 1 , ∆ 1 ; Γ 2 , ∆ 2 ⊢ * SH f alse iff Γ 1 ∧ ∆ 1 ∧ Γ 2 ∧ ∆ 2 is T 1 ∪ T 2 -unsatisfiable.

RR n➦ 6688

Proof: Direct consequence of the following Lemmas.

Lemma 8 Let σ = {x 1 → t 1 , ..., x n → t n } be a substitution such that x i ∈ V ar(t j ) for all i, j. For every theory T and every conjunction Γ of literals we have:

T ∪ Γ ∪ {x 1 = t 1 , ..., x n = t n } |= x = y iff T ∪ Γσ |= xσ = yσ Proof: (⇒) Assume that T ∪ Γ ∪ {x 1 = t 1 , ..., x n = t n } |= x = y and let M, α be such that |= α M T ∪ Γσ. By the fact that x i does not appear in T ∪ Γσ, one can redefine α such that α(x i ) = α(t i ), for all i. It is easy to see that α satisfies T ∪ Γ ∪ {x 1 = t 1 , ..., x n = t n } in M. It implies α satisfies x = y in M too, thus xσ = yσ evaluates to true in M by using α. (⇐) Assume that T ∪ Γσ |= xσ = yσ and let M, α be such that |= α M T ∪ Γ ∪ {x 1 = t 1 , ..., x n = t n }. It is straightforward that α satisfies T ∪ Γσ in M. Hence α satisfies xσ = yσ in M.
In addition, α(x i ) = α(t i ), for all i, which implies x = y evaluates to true in M by using α.

Lemma 9 (Termination) The relation ⊢ * SH is terminating.

Proof: If rules Solve-fail and Contradiction apply, the procedure terminates.

For other rules, we must show that rules Solve-success and Deduction can not be applied infinitely. Indeed, Solve-success can only be applied if Γ 1 is not in solved form. Only Deduction may likely modify a solved form into a non-solved form by integrating an equality between variables. The set of shared variables is finite and Deduction integrates equalities detected in T 1 to T 2 only if they have not been detected in T 2 (canon 1 (xσ 1 ) = canon 1 (yσ 1 ) and canon 2 (xσ 2 ) = canon 2 (yσ 2 )). This guarantees that Deduction can only be applied finitely many times.

Lemma 10 (Soundness) The relation ⊢ SH preserves equisatisfiability in

T 1 ∪ T 2 .
Proof: The soundness is straightforward for rules Solve-fail and Contradiction.

❼ For Solve-success:

-(⇒) Assume that |= α M Γ 1 ∧∆ 1 ∧Γ 2 ∧∆ 2 . Let σ 1 = {x 1 → t 1 , ..., x n → t n } = solve(Γ 1 ). By definition of solve, the equivalence (Γ 1 ⇔ ∃ỹ. n i=1 x i = t i ) is T 1 ∪ T 2 -valid. We can extend α to ỹ such that α(x i ) = α(t i ). It is easy to see that |= α M σ 1 ∧ ∆ 1 ∧ Γ 2 ∧ ∆ 2 . -(⇐) Assume that |= α M σ 1 ∧ ∆ 1 ∧ Γ 2 ∧ ∆ 2 ,
where σ 1 = solve(Γ 1 ). Due to the above equivalence, we clearly have

|= α M Γ 1 ∧ ∆ 1 ∧ Γ 2 ∧ ∆ 2 . ❼ For Deduction: -(⇒) Assume that |= α M σ 1 ∧∆ 1 ∧ σ 2 ∧∆ 2 . We have α(x) = α(xσ 1 ) and α(y) = α(yσ 1 ). By Lemma 8, T 1 ∪ σ 1 |= x = y iff T 1 |= xσ 1 = yσ 1 . But then T 1 |= xσ 1 = yσ 1 implies T 1 ∪ T 2 |= xσ 1 = yσ 1 , thus α(xσ 1 ) = α(yσ 1 ). Hence α(x) = α(y) and |= α M σ 1 ∧ ∆ 1 ∧ σ 2 ∧ x = y ∧ ∆ 2 . -(⇐) Trivial. INRIA Lemma 11 (Completeness) If Γ 1 , ∆ 1 ; Γ 2 , ∆ 2 is a normal form w.r.t. ⊢ SH different from f alse, then Γ 1 ∧ ∆ 1 ∧ Γ 2 ∧ ∆ 2 is T 1 ∪ T 2 -satisfiable.
Proof: If the procedure terminates without reporting f alse, the final configuration must be of the form ( σ 1 , ∆ 1 ); ( σ 2 , ∆ 2 ) such that:

❼ σ i ∧ ∆ i is T i -satisfiable for i = 1, 2 (otherwise Contradiction applies), ❼ ∀x, y ∈ V ar(Φ 1 )∩V ar(Φ 2 ), canon 1 (xσ 1 ) = canon 1 (yσ 1 ) iff canon 2 (xσ 2 ) = canon 2 (yσ 2 ) (otherwise Deduction applies). Since σ i ∧ ∆ i is T i -satisfiable we have T i |= ( σ i ∧ ∆ i ) ⇒ x = y iff canon i (xσ i ) = canon i (yσ i )
in NO to Γ 1 ∪ ∆ 1 ; Γ 2 ∪ ∆ 2 .
Similarly, the application of rules Solvesuccess 1 and Deduction 1 in SH simulates the application of Deduction 1 in NO; showing that equalities between shared variables can be derived by invoking a solver (and a canonizer) rather than resorting to guessing as for NO when applying the rule Deduction i (i = 1, 2). This is one of the key insights underlying Shostak's schema.

Combining a CSI-theory with a SH-theory

Without loss of generality, let us assume that T 1 is in CSI and that T 2 is in SH. This situation frequently arises in practical verification problem, e.g. the union of a theory in SH and E (which is not in SH). We consider the inference system NS obtained as the union of NO 1 in Figure 1 and SH 2 , the symmetric of SH 1 in Figure 2. NS takes configurations of the form Φ 1 ; Γ 2 , ∆ 2 where Φ 1 is a set of Σ 1 -literals, Γ 2 is a set of Σ 2 -equalities, and ∆ 2 is a set of Σ 2disequalities. We furtherly assume that when a rule of NO is applied, Φ 1 ; Γ 2 , ∆ 2 stands for Φ 1 ; Γ 2 ∪ ∆ 2 and when a rule of SH is applied, Φ

1 ; Γ 2 , ∆ 2 is considered as Γ 1 , ∆ 1 ; Γ 2 ∪ ∆ 2 , where Φ 1 = Γ 1 ∪ ∆ 1 and Γ 1 (∆ 1
) is a set of Σ 1 -equalities (-disequalities, respectively). NS can be seen as an abstract version of the one proposed in [START_REF] Barrett | A generalization of Shostak's method for combining decision procedures[END_REF].

Theorem 3 Let T 1 , T 2 be two signature-disjoint theories such that T 1 is in CSI and T 2 is in SH. Let NS be the inference system defined as the union NO 1 ∪SH 2 , where NO 1 is in Figure 1 and SH 2 is obtained from SH 1 in Figure 2 by symmetry. The relation ⊢ * NS is terminating and

Φ 1 ; Γ 2 , ∆ 2 ⊢ * NS f alse iff Φ 1 ∧ Γ 2 ∧ ∆ 2 is T 1 ∪ T 2 -unsatisfiable.
Let T 1 , ..., T k and T k+1 , ..., T k+n be k theories in CSI and n theories in SH, respectively, and such that Σ i ∩ Σ j = ∅ for i, j = 1, . . . , k + n, i = j, and n, k ≥ 1. It is possible to modularly build a satisfiability procedure for T = k+n j=1 T j as follows. Repeatedly use NO to obtain a satisfiability procedure for U 0 = k j=1 T j , then repeatedly use NS to build satisfiability procedures for U 1 = U 0 ∪ T k+1 , . . . , U n = U n-1 ∪ T k+n , where U n is T . An alternative would be to repeatedly use SH to construct satisfiability procedures for unions of two theories in SH, followed by a repeated use of NO on the resulting theories. Also, let us mention still another possibility to combine k theories in CSI and n theories in SH. It is possible to slightly modify our inference rules to take into account k + n theories and configurations of the form Φ 1 ; . . . ; Φ k ; Γ k+1 , ∆ k+1 ; . . . ; Γ k+n , ∆ k+n .

The rule Deduction would propagate an equality between shared variables, deduced in one theory, to the other (k + n) -1 theories. At this point, it is not difficult to modify the proof of correctness for NS to show that the resulting rules (taken from NO 1 , . . . , NO k , SH k+1 , . . . , SH k+n ) yield a satisfiability procedure for T . The resulting proof would be a bit more involved because of the more complex notation.

Combining Non Stably Infinite Convex Theories

So far, we have only considered stably infinite convex theories. However we can sometimes drop the requirement of stable infiniteness and replace it with a somewhat more natural requirement, i.e. the decidability for the (convex) theory to admit a trivial model.

The following simple fact will be useful for the completeness of the satisfiability problem in combination of (convex) non stably infinite theories.

Proposition 2 Let T be a C-theory. If T has a non trivial model, then T has an infinite model.

Proof: If T does not have infinite models, then T must entail the formula 1≤j =k≤n x j = x k for some positive integer n. Then, T entails x k = x k ′ since T is convex. Therefore, T has only trivial models, which leads to a contradiction.

It turns out that by studying the existence of trivial models for (convex) theories, we are able to decide the satisfiability in the combination of non stably infinite theories.

Proposition 3 Let T 1 and T 2 be decidable C-theories such that we know whether T i has a trivial model, for i = 1, 2. If the signatures of T 1 and T 2 are disjoint, then T 1 ∪ T 2 is a decidable C-theory.

Proof: Let Σ 1 (resp. Σ 2 ) be the signature of T 1 (resp. T 2 ). Let Φ be a set of quantifier free Σ 1 ∪ Σ 2 -literals. By variable abstraction, Φ is

T 1 ∪ T 2 - equisatisfiable to Φ 1 ∪Φ 2 such that Φ i contains only Σ i -literals (i = 1, 2). Thanks to Lemma 1, Φ 1 ∪ Φ 2 is T 1 ∪ T 2 -satisfiable iff there exists an arrangement Φ 0 such that Φ 1 ∪ Φ 0 is satisfiable in a model M 1 of T 1 and Φ 2 ∪ Φ 0 is satisfiable in a model M 2 of T 2
and the domains of M 1 and M 2 have the same cardinality. We show that such models exist if we know whether T i (for i = 1, 2) has a trivial model. We have to consider the following cases:

❼ Φ 1 ∪ Φ 0 is T 1 -satisfiable in a model M 1 and Φ 2 ∪ Φ 0 is T 2 -satisfiable in
a model M 2 such that M 1 and M 2 are both non trivial. This can be checked by deciding

for i = 1, 2, if Φ i ∪ Φ 0 ∪ {x = y} is T i -satisfiable,
where x, y are new variables. By Proposition 2, we know that there exists a model

M ′ 1 of T 1 satisfying Φ 1 ∪ Φ 0 and a model M ′ 2 of T 2 satisfying Φ 2 ∪ Φ 0 such that M ′ 1 and M ′ 2 have the same infinite cardinality. As a consequence, Φ 1 ∪ Φ 2 is T 1 ∪ T 2 -satisfiable. INRIA ❼ Φ i ∪ Φ 0 is T i -satisfiable but only in a trivial model, for i = 1, 2. In this case, it is sufficient to check that for i = 1, 2, if Φ i ∪ Φ 0 ∪ {x = y} is T i -unsatisfiable, where x, y are new variables. Thus Φ 1 ∪ Φ 2 is T 1 ∪ T 2 -
satisfiable in a trivial model.

❼ Φ 1 ∪Φ 0 is T 1 -satisfiable only in a trivial model and Φ 2 ∪Φ 0 is T 2 -satisfiable in a non trivial model. This can be checked by testing if

Φ 1 ∪ Φ 0 ∪ {x = y} is T 1 -unsatisfiable, and Φ 2 ∪ Φ 0 ∪ {x = y} is T 2 -satisfiable,

Combining Deduction Complete Theories

In order to find a suitable trade-off between modularity (of the Nelson-Oppen approach) and efficiency (by using canonizers and solvers), we introduce in this Section the concepts of deduction completeness and inference-based satisfiability procedure. Such procedures can be flexibly built by adapting the rewriting approach of [START_REF] Armando | A Rewriting Approach to Satisfiability Procedures[END_REF] (cf. Section 4.1) and modularly combined by reusing the ideas underlying both Nelson-Oppen and Shostak approaches (cf. Section 4.2).

Informally, an inference-based procedure is a satisfiability procedure defined via an inference system whose inference rules have fixed arity and perform validity preserving transformations on sets of clauses. We also assume that the (fair) application of the inference rules is terminating for any input, and that the final set of clauses contains f alse iff the input is T -unsatisfiable. When it is T -satisfiable, the final set of clauses does not contain f alse but the socalled deduction complete set of elementary equalities representing all entailed elementary equalities.

Definition 1 Let T be a convex theory and Φ be a T -satisfiable set of literals. A set of elementary equalities E is deduction complete (for Φ modulo

T ) if ∀x, y ∈ V ar(Φ), T |= Φ ⇒ x = y iff E |= x = y A deduction complete T -satisfiability procedure is a T -satisfiability procedure, denoted by DC T , such that if Φ is T -satisfiable,
then it returns f alse, otherwise it returns true{E} where E is deduction complete for Φ modulo T .

Before being able to define the notion of inference system which is at the core of a deduction complete satisfiability procedure, we need to introduce some technical notions and notations. The set of elementary equalities occurring in a set S of clauses is denoted by E(S) and E(S) is S\E(S). If E is a finite set of elementary equalities over totally ordered constants, then E ↓ denotes the canonical form of E defined as the finite set of elementary equalities c = c↓ such that c↓ is the smallest constant such that c = E c↓ and c↓ = c. S ↓ E denotes the normal form of S with respect to the (canonical) rewrite system defined by orienting from left to right the equalities in

E ↓ . E is said in canonical form if E = E ↓ .
Definition 2 A basic inference system I for a theory T is an inference system working on sets of clauses such that each inference rule in I has a given arity k and transforms k clauses into a T -equivalent set of clauses. An I-transition is defined as follows: S → I S ′ if S ′ is obtained by applying a rule in I on E(S). A ξ-transition is defined as follows: S → ξ S ′ if S ′ = E(S) ↓ ∪ E(S)↓ E(S) . An Iderivation is a chain of I-transitions and ξ-transitions, denoted by * → ξ∪I , where ξ-transitions are applied eagerly. An I-normal form of a set of clauses S is a set of clauses S ′ such that S * → ξ∪I S ′ and there is no S ′′ satisfying S ′ → I S ′′ or S ′ → ξ S ′′ .

We are now ready to identify some interesting properties of inference-based satisfiability procedures.

Definition 3 Let T be a convex theory and I a basic inference system for T . Given a finite set of T -valid clauses Ax:

❼ (I,
❼ (I, Ax) is deduction complete if (I, Ax
) is refutation complete and terminating, and for any T -satisfiable set of ground equalities Γ and any I-normal form S of Ax ∪ Γ, E(S) is deduction complete for Γ modulo T .

The set of clauses Ax is omitted whenever it is clear from the context and the inference system I is said refutation complete (resp. terminating, deduction complete). A theory T is deduction complete if there exist a basic inference system I and a set of clauses Ax such that (I, Ax) is deduction complete. The class of deduction complete (resp. deduction complete and stably infinite) convex theories is denoted by DCC (resp. DCCSI).

Some remarks are in order. First, if (I, Ax) is deduction complete for T , then I provides a deduction complete satisfiability procedure. Second, by definition DCC ⊆ C and DCCSI ⊆ CSI. Third, the assumptions on basic inference systems prevent us to use guessing and a T -satisfiability procedure to derive entailed elementary equalities, since the rules in a deduction complete inference system may only perform "local" changes. Finally, it is possible to build a deduction complete satisfiability procedure by using the solver and the canonizer of a SH-theory.

Proposition 4 SH ⊆ DCCSI, i.e. each theory in SH admits a deduction complete decision procedure.

It is straightforward to prove this proposition by using the basic inference system SH depicted in Figure 3 and noticing that (SH, ∅) is deduction complete for any SH-theory.

Deduction completeness by superposition

We show in what follows how a Superposition Calculus (SP) can be used to build deduction complete decision procedures. This can be seen as a generalization of

INRIA Solve -fail s = t f alse if s = t is not in solved form, solve(s = t) = f alse Solve -success s = t σ if s = t is not in solved form, σ = solve(s = t) = f alse Replace u = v ∧ x = t (u = v){x → t} ∧ x = t if x = t is in solved form, x occurs in u = v Canon x = t x = canon(t) if x does not occur in t t = canon(t) Deduction x = t ∧ y = t x = t ∧ y = t ∧ x = y if x, y do not occur in t
Figure 3: The basic inference system SH the rewriting approach to flexibly build satisfiability procedures proposed in [START_REF] Armando | A Rewriting Approach to Satisfiability Procedures[END_REF].

We explore this problem for the subclass of Horn theories axiomatized by a finite set of Horn clauses. 5The Superposition Calculus SP. A fundamental feature of SP is the usage of a reduction ordering ≻ which is total on ground terms, for example the lexicographic path ordering ( [START_REF] Dershowitz | Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 6: Rewrite Systems[END_REF]). We also assume that if a term t is not a variable or constant, then for any constant c we have that t ≻ c. The ordering ≻ is extended to positive literals by considering them as multisets of terms, and then to the clauses by considering them as multisets of positive literals. A clause C is redundant with respect to a set S of clauses if either C ∈ S or S can be obtained from S ∪ {C} by a sequence of application of the contraction rules of Figure 5. An inference is redundant with respect to a set S of clauses if its conclusion is redundant with respect to S. A set S of clauses is saturated with respect to SP if every inference of SP with a premise in S is redundant with respect to S. A derivation in this inference system is a sequence

Right paramodulation Γ ⇒ ∆, l[u ′ ] = r Π ⇒ Σ, u = t σ(Γ, Π ⇒ ∆, Σ, l[t] = r) (i -iv) Left paramodulation Γ, l[u ′ ] = r ⇒ ∆ Π ⇒ Σ, u = t σ(l[t] = r, Γ, Π ⇒ ∆, Σ) (i -iv) Reflection Γ, u ′ = u ⇒ ∆ σ(Γ ⇒ ∆) (v) Eq. Factoring Γ ⇒ ∆, u = t, u ′ = t ′ σ(Γ, t = t ′ ⇒ ∆, u = t ′ ) (i), (vi)
where a clause

¬A 1 ∨ • • • ∨ ¬A n ∨ B 1 ∨ • • • ∨ B n is
(i) σ(u) σ(t), (ii) u = t is selected in its clause, (iii) σ(l[u ′ ]) σ(r), (
iv) l = r is selected in its clause, (v) u ′ = u is selected in its clause, (vi) u = t is selected in its clause and σ(t) σ(t ′ ) and σ(u ′ ) σ(t ′ ).

Figure 4: Expansion Rules of SP. S 0 , S 1 , . . . , S i , . . . of sets of clauses where at each step an inference of SP is applied to generate and add a clause (cf. expansion rules in Figure 4) or to delete or reduce a clause (cf. contraction rules in Figure 5). A derivation is characterized by its limit, defined as the set of persistent clauses S ∞ = j≥0 i>j S i . A derivation S 0 , S 1 , ..., S i , ... with limit S ∞ is fair with respect to SP if for every inference in SP with premises in S ∞ , there is some j ≥ 0 such that the inference is redundant in S j .

Orientation S ∪ {c = c ′ } S[c → c ′ ] if c ≻ c ′ Simplification S ∪ {C[l ′ ], l = r} S ∪ {C[θ(r)], l = r} if l ′ ≡ θ(l), θ(l) ≻ θ(
Theorem 4 ( [START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF]) If S 0 , S 1 , . . . is a fair derivation of SP, then ( i) its limit S ∞ is saturated with respect to SP, ( ii) S 0 is unsatisfiable iff the empty clause is in S j for some j, and ( iii) if such a fair derivation is finite, i.e. it is of the form S 0 , . . . , S n , then S n is saturated and logically equivalent to S 0 .

The saturation-based methodology [START_REF] Armando | A Rewriting Approach to Satisfiability Procedures[END_REF] for T -satisfiability consists of two phases:

INRIA 1.
Flattening: all ground literals are flattened by introducing new constants, yielding an equisatisfiable flat problem.

2.

Ordering selection and termination: any fair derivation of SP is shown to be finite when applied to a flat problem together with the axioms of T , provided that ≻ satisfies a few properties depending on T .

Variable inactivity and combination. In [START_REF] Armando | New results on rewrite-based satisfiability procedures[END_REF], the notion of variable inactive theory has been identified as the key (sufficient) condition to obtain the modularity of termination of the fair and exhaustive application of the rules of SP on the union of (presentations of) theories. A theory T axiomatized by Ax(T ) is variable inactive when any fair derivation of SP on Ax(T ) ∪ S, for some set of clauses S, does not contain a maximal literal (w.r.t. the ordering ≻) of the form X = t and X ∈ Var (t). The absence of such (maximal) literals ensures that no inference on variables may involve clauses derived from different axiomatizations of theories and so termination is preserved. It turns out that the variable inactivity property of a theory is a key requirement also for deduction completeness, as stated in the following theorem.

Theorem 5 Let T be a theory axiomatized by a finite set Ax(T ) of Horn clauses. Assume that for every set S of ground flat literals, any saturation S ′ of Ax(T ) ∪ S by SP is finite and contains no equality of the form X = t, where X ∈ V ar(t). Then T is stably infinite and (SP, Ax(T )) is deduction complete for T or, equivalently, T is a DCCSI-theory.

Proof: Stable infiniteness of T follows from the variable inactivity as proved in [START_REF] Kirchner | Automatic Combinability of Rewriting-Based Satisfiability Procedures[END_REF]. Consider now the deduction completeness problem. Let E be the set of elementary equalities in S ′ . Assume that there is some equality c = c ′ between constants such that T ∪ S |= c = c ′ . By refutation, T ∪ S |= c = c ′ iff S ∧ c = c ′ is T -unsatisfiable. Hence, it must be possible to derive the empty clause by applying SP to the set S ′ ∪ {c = c ′ }. Since S ′ is T -satisfiable and saturated, only inferences involving both clauses from (or inferred from) S ′ and c = c ′ can yield the empty clause. If there is an inference between c = c ′ and C ′ in S ′ , then C ′ must be an equality between constants or variables. This is because the ordering used in SP is defined in such a way that a disequality is always bigger than an equality and hence an equality is maximal in a clause only if the latter contains no disequalities. If C ′ contains a variable, then C ′ must have the form X = t, where X ∈ V ar(t). That would contradict the assumption of the lemma. If C ′ only contains constants, then C ′ is an equality between constants and the clause inferred from c = c ′ and C ′ must be a disequality between constants. This means that an inference between c = c ′ and a clause in S ′ is possible only if the latter is an equality between constants and derives a disequality between constants. Therefore, E ∪ {c = c ′ } suffices to infer the empty clause. Or, equivalently,

E |= c = c ′ .
Let us consider a few theories in which this approach can be successfully applied.

Example 1 Consider the theory of equality E, axiomatized by an empty set of axioms. Let Φ be a set of ground flat literals. It is easy to see that the saturation of Φ w.r.t. SP contains only ground and flat literals (see, e.g., [START_REF] Armando | A Rewriting Approach to Satisfiability Procedures[END_REF]). By Theorem 5, E is stably infinite and (SP, ∅) is deduction complete for E.

Example 2 Let L be the theory of lists, axiomatized by the following set Ax(L) of axioms:

car(cons(X, Y )) = X (1) cdr(cons(X, Y )) = Y (2) cons(car(X), cdr(X)) = X (3)
By induction on the length of the derivation w.r.t. SP, we can show (see [START_REF] Armando | A Rewriting Approach to Satisfiability Procedures[END_REF]) that for any set of ground flat literals S, the saturation of Ax(L) ∪ S w.r. Example 3 Let SC be the theory finitely presented by the following set Ax(SC) of axioms:

(Sel) : s 1 (c(X 1 , . . . , X n )) = X 1 . . . s n (c(X 1 , . . . , X n )) = X n (Inj) : c(X 1 , . . . , X n ) = c(Y 1 , . . . , n ) ⇒ X 1 = Y 1 . . . c(X 1 , . . . , X n ) = c(Y 1 , . . . , Y n ) ⇒ X n = Y n
(a 1 = c(Y 1 , . . . , Y n ) ⇒ a ′ 1 = Y 1 ), . . . , (a n = c(Y 1 , . . . , Y n ) ⇒ a ′ n = Y n ) where a 1 , a ′ 1 .
. . , a n , a ′ n are constants. By Theorem 5, SC is stably infinite and (SP, Ax(SC)) is deduction complete for SC.

Combining DCCSI theories

So far, we have introduced the concept of deduction complete satisfiability procedures and shown that such procedures can be flexibly built for an interesting class of theories. We are left with the problem of showing that deduction complete procedures can be modularly combined, taking thereby advantage of both Shostak (derivation of entailed equalities) and Nelson-Oppen (modularity) schemas. The combination algorithm for deduction complete satisfiability procedures is depicted in Figure 6, where DC Ti (Φ) denotes the deduction complete satisfiability procedure in the theory T i applied to the set of literals Φ. Its correctness is stated in the next theorem.

Theorem 6 Let T 1 and T 2 be two signature-disjoint convex and stably infinite theories such that for each i = 1, 2, a deduction complete T i -satisfiability procedure is available. Let Ω i be a set of non-elementary T i -literals for i = 1, 2, let E be a set of elementary equalities and let ∆ be a set of elementary disequalities. Let ϕ = (Ω 1 ∪Ω 2 ∪∆∪E) and S ′ be a final configuration obtained by the repeated

INRIA Unsat =1 Ω 1 ; ∆; E; Ω 2 f alse if DC T1 (Ω 1 ∪ E) = f alse Unsat = Ω 1 ; ∆; E; Ω 2 f alse if x = y ∈ ∆ and (x, y) ∈ E * Deduction 1 Ω 1 ; ∆; E; Ω 2 Ω 1 ; ∆; E ′ ; Ω 2 if DC T1 (Ω 1 ∪ E) = true{E ′ } E ′ * = E *
❼ if S ′ is f alse, then ϕ is T 1 ∪ T 2 -unsatisfiable; ❼ otherwise, S ′ is of the form Ω 1 ; ∆; E ′ ; Ω 2 and ϕ is T 1 ∪ T 2 -satisfiable. Furthermore, E ′ is deduction complete for ϕ modulo T 1 ∪ T 2 .
Proof: Similar to the proof of Theorem 1. Let us consider the rules of Figure 6.

Termination. The rules return f alse or strictly decrease the number of pairs of shared variables which are not equal modulo E.

Soundness. The rules are clearly sound.

Completeness. Similarly to Lemma 5, we proceed by contradiction. Consider a final configuration S ′ of the form (Ω 1 ; ∆; E ′ ; Ω 2 ). According to the rules,

Φ i = (Ω i ∪ ∆ ∪ E) is necessarily T i -satisfiable for i = 1, 2,

otherwise either

Unsat =1 or Unsat = would apply according to Lemma 6. Assuming Φ 1 ∪ Φ 2 is T 1 ∪ T 2 -unsatisfiable, we can apply Lemma 1 to exhibit a contradiction with the fact that S ′ is a final configuration.

Deduction Completeness. It remains to show that, if

S ′ = (Ω 1 ; ∆; E ′ ; Ω 2 ) is a final configuration, E ′ is deduction complete. By contradiction, assume that E ′ is not deduction complete. There exists x = y such that T 1 ∪ T 2 ∪ S ′ |= x = y and E ′ |= x = y. Therefore S ′′ = (Ω 1 ; ∆ ∪ {x = y}; E ′ ; Ω 2 ) is
unsatisfiable, and so S ′′ is reducible with combination rules of Figure 6. But if S ′′ is reducible, then S ′ is also reducible, which contradicts that S ′ is a final configuration.

Corollary 1 DCCSI is closed under disjoint union.

Proof: Let (I k , Ax k ) be a deduction complete inference system for T k (k = 1, 2). Consider the basic inference system I for T 1 ∪ T 2 defined as the union of I 1 and I 2 plus the classical rules to purify heterogeneous equalities. We assume that rules in I k are only applied to pure non-elementary equalities. Clauses in Ax = Ax 1 ∪ Ax 2 are T 1 ∪ T 2 -valid. We show below that (I, Ax) is terminating, refutation complete, and deduction complete for

T 1 ∪ T 2 .
Termination. We assume that a set of ground equalities Γ is split into a set Γ H of impure equalities, a set E of elementary equalities, and a set Γ i of i-pure equalities (for i = 1, 2). The termination of I can be proved by using a lexicographic combination of complexity measures defined and ordered as follows:

(H) the number of alien positions occurring in Γ H , (0) the number of E-equivalence classes,

(1) the number of steps to reach a I 1 -normal form of Ax 1 ∪ Γ 1 , and

(2) the number of steps to reach a

I 2 -normal form of Ax 2 ∪ Γ 2 .
Termination follows from the facts that any I-transition strictly decreases the complexity measure defined above, and any ξ-transition does not increase (H) and strictly decreases (0).

Soundness. When f alse is derived by I, this result is correct since any Itransition transforms a set of clauses into a T 1 ∪ T 2 -equivalent one.

Completeness. Consider a I-normal form S of Γ such that f alse / ∈ S. Let E ′ = E(S). S is also a I-normal form of Γ 1 ∪ Γ 2 ∪ E, where Γ 1 , Γ 2 , E are obtained from Γ by applying the purification rules. The configuration Γ 1 ; ∅; E ′ ; Γ 2 is necessarily a final configuration w.r.t. the combination rules depicted in Figure 6, otherwise this would contradict the assumption that (I k , Ax k ) is deduction complete for T k (k = 1, 2). According to Theorem 6, Γ 1 ∪ Γ 2 ∪ E ′ is T 1 ∪ T 2 -satisfiable (and so is Γ). Moreover, E ′ is deduction complete for Γ 1 ∪Γ 2 ∪E ′ , and so for Γ. Consequently, (I, Ax) is deduction complete for T 1 ∪ T 2 .

Explaining Combination

Although combining decision procedures is already a crucial activity for their effective use in large systems, this is seldom sufficient: procedures should also provide the capability of explaining their results in order to be correctly integrated. In this Section, we study how to augment the interface capabilities of available decision procedures to compute such explanations and to modularly combine them. The decision procedures that we want to combine can conclude either unsatisfiability or satisfiability and can produce entailed elementary equalities in case of satisfiability. So explaining these results involves both the production of an unsatisfiability witness, called conflict set, given by a small set of unsatisfiable literals, and the production of explanations for entailed elementary equalities. So a first step in Section 5.1 is to precisely define conflict sets, explanations, and the minimality property in each case. Then in order to build the deductive part of the justification in case of satisfiability, the notion of explanation graph is proposed in Section 5.2. Such graphs record the successive justifications used in the construction of entailment proofs. For decision INRIA procedures we are interested in, the notion of quasi-conflict sets is proposed in Section 5.3 to represent proofs of unsatisfiability integrating both conflict sets and explanation graphs. Then, in Section 5.4, we propose to use explanation engines instead of decision procedures. Such engines return either an explanation graph in case of satisfiability or a quasi-conflict set in case of unsatisfiability. Eventually it is proved that explanation engines can be built in a modular way for signature-disjoint combination of convex and stably infinite theories.

Conflict sets and explanations

The starting point of our development is the notion of conflict set, commonly used in the context of unsatisfiability. Informally, a conflict set is a subset of an unsatisfiable set of literals which is already unsatisfiable. For efficiency, a suitable notion of minimality for conflict sets is introduced.

A T -conflict set CS of literals is minimal if there is no CS ′ ⊂ CS such that CS ′ is a T -conflict set.
In the context of satisfiability, the dual notion of conflict set is the concept of explanation. A T -explanation of an equality e is a T -satisfiable set ϕ of literals such that T |= ϕ ⇒ e. A T -explanation of e is minimal if there is no ϕ ′ ⊂ ϕ such that T |= ϕ ′ ⇒ e. We omit the theory T when it is clear from the context. The next proposition states the duality between the two notions and follows directly from the definitions.

Proposition 5 A T -satisfiable set of literals ϕ is a minimal T -explanation for an equality e iff ϕ ∪ {¬e} is a minimal T -conflict set.

The convexity assumption allows us to further characterize conflict sets.

Proposition 6 If T is a convex theory, then any minimal conflict set contains at most one disequality. If T is a convex theory axiomatized by a set of equalities, then any minimal conflict set contains exactly one disequality.

For example, E is a convex theory such that any minimal conflict set contains exactly one disequality. Notice that LA, and hence also LA ≤ , does not satisfy this property (e.g, {x = 3, x = 2} is a minimal LA-conflict set). We now explain how to store explanations by using undirected and acyclic graphs.

Explanation Graphs

We use some standard notions as undirected graph, acyclic graph, subgraph, connected graph, path, simple path, elementary path, and connected components. In the rest of the paper, we only consider acyclic undirected graphs, often called graphs for the sake of simplicity. An undirected graph G is a pair (V, E) where V (also written as Vertex (G)) is a finite set of vertices and E (also written as Edge(G)) is a set of unordered pairs written as (v, w) for v, w in V . G V ∅ denotes the graph whose vertices in V are connected by no edge, i.e. G V ∅ = (V, ∅). The subgraph relation is denoted by ⊆. Let G = (V, E) be an acyclic undirected graph. The set ElemP ath(G, x, y) denotes the set of edges in an elementary path between x and y in G, i.e. if v 0 , ..., v n is an elementary path where v 0 is x and v n is y, then ElemP ath(G, x, y) is the set of edges (v i-1 , v i ) ∈ Edge(G), for i = 1, ..., n. Given two distinct vertices x and y, ElemP ath(G, x, y) is empty iff x and y are not in the same connected component of G. The set of pairs of connected vertices in G is CP (G) = {(x, y) | x, y ∈ V and ElemP ath(G, x, y) = ∅}.

Notice that

E * = CP (G) ∪ {(x, x) | x ∈ V }.
Two preliminary remarks about the relationship between an acyclic undirected graph G = (V, E) and a set of elementary equalities are useful. First, let us observe that an elementary equality can be regarded as an unordered pair and edges of G are unordered pairs. So, we write (x, y) ∈ E as x = y and define the set of elementary equalities of the graph G as Eq(G) = (x,y)∈E {x = y}. Second, it is easy to see that a set of elementary equalities E is minimal iff there exists an acyclic undirected graph G such that Eq(G) = E.

Definition 4 Let T be a theory, ϕ be a set of T -literals, and G = (V, E) be an acyclic undirected graph such that E is a set totally ordered by some ordering < E . G is an explanation graph of ϕ if (i) V is the set of constants occurring in ϕ, (ii) there exists a labelling function L G with domain E and co-domain 2 ϕ∪CP (G)6 , (iii) the following properties are satisfied for any v 1 = v 2 ∈ E:

(iii.a) L G (v 1 = v 2 ) is T -satisfiable and T |= L G (v 1 = v 2 ) ⇒ v 1 = v 2 , (iii.b) for each v ′ 1 = v ′ 2 in L G (v 1 = v 2 )\ϕ we have that e < E (v 1 = v 2 ), for any e in ElemP ath(G, v ′ 1 , v ′ 2 ). The set of literals of ϕ in G is Lit(G) = ϕ ∩ ( e∈E L G (e)). An edge v 1 = v 2 ∈ E is minimally explained if L G (v 1 = v 2 ) is a minimal T -explanation for v 1 = v 2 .
A explanation graph is minimally explained if all its edges are minimally explained. An explanation graph G ′ is smaller than an explanation graph G, denoted by G ′ ⊑ G, if Edge(G ′ ) ⊆ Edge(G) and ∀e ∈ Edge(G ′ ), L G ′ (e) ⊆ L G (e). An explanation graph G is minimal for E if E ⊆ CP (G) and there is no explanation graph G ′ such that G ′ ❁ G and E ⊆ CP (G ′ ). An explanation graph G of a T -satisfiable set ϕ of literals is deduction complete (modulo T ) if Eq(G) is deduction complete for ϕ (modulo T ). In both cases, a = c is the smallest edge of the graph, and is used in the explanation of another edge.

In the definition above, edges are ordered to express the fact that explanation graphs are built dynamically. The ordering < E on edges corresponds to the order of insertion of edges in the graph. Adding an edge x = y to the explanation graph G = (V, E) of the set ϕ of literals is defined as follows: if x and y are two distinct vertices in V such that x = y / ∈ CP (G), and L is a set of T -literals in ϕ ∪ CP (G) such that L is T -satisfiable and T |= L ⇒ x = y, then Insert(G, x = y, L) denotes the explanation graph G ′ = (V, E ′ ), where

E ′ = E ∪ {x = y}, L G ′ is such that L G ′ (x = y) = L, ∀e ∈ E, L G ′ (e) = L G (e),
and < E ′ is the smallest ordering containing < E such that ∀e ∈ E, e < E ′ x = y. From now on, we assume that < E ′ and < E coincide on elements of E whenever G = (V, E) and G ′ = (V ′ , E ′ ) are two explanation graphs such that E ⊆ E ′ .

We now consider the case of an explanation graph G obtained by adding a set of elementary equalities in a given order. (This will be important for our combination schema described in Section 5.4 below.) For the sake of conciseness, we write U F (E) to abbreviate the graph obtained by the sequence of insertions above. 7 If V is a set of variables, U F V (E) is the explanation graph obtained by adding V to the set of vertices of U F (E). It is not difficult to see that for any set E of elementary equalities, U F (E) is a minimally explained explanation graph of E such that Eq(U F (E)) is a minimal set of elementary equalities (included in E). Moreover, U F (E) is a deduction complete explanation graph of E. More generally, it is possible to construct (deduction complete) explanation graphs when a (deduction complete) satisfiability procedure is known. For a (deduction complete) inference-based satisfiability procedure, an explanation graph of a satisfiable formula can be constructed by collecting the literals used in each rule application of the derivation. For the particular case of the theory of equality E, a congruence closure with explanation leads to a minimally explained and deduction complete explanation graph for any set of flat equalities, as shown in [START_REF] Ranise | Combining Proof-Producing Decision Procedures[END_REF]. In that case, the explanation of an edge x = y is either {x = y} or {x = f (x 1 , . . . , x n ), y = f (y 1 , . . . , y n ), x 1 = y 1 , . . . , x n = y n }, and so is minimal.

Quasi-conflict sets

Let us now concentrate on unsatisfiability proofs. The notion of conflict set is not sufficiently structured to take into account the deduction steps in the proof and their explanation. This is why we consider a richer structure called quasi-conflict sets.

Definition 5 (Quasi-conflict sets) Let ϕ be an unsatisfiable set of literals, ψ a subset of ϕ, G an explanation graph of ϕ, and E a set of equalities. The triplet

(ψ, E, G) is a quasi-conflict set of ϕ if E ⊆ CP (G), ψ ∪ E is unsatisfiable, and E = ∅ implies that ψ is satisfiable. A quasi-conflict set (ψ ′ , E ′ , G ′ ) is smaller than a conflict set (ψ, E, G), de- noted by (ψ ′ , E ′ , G ′ ) (ψ, E, G), if ψ ′ ⊆ ψ, E ′ ⊆ E and G ′ ⊑ G. A quasi- conflict set (ψ, E, G) is minimal if there is no quasi-conflict (ψ ′ , E ′ , G ′ ) such that (ψ ′ , E ′ , G ′ ) ≺ (ψ, E, G). Notice that if (ψ, E, G) is a quasi-conflict set, then E = ∅ iff ψ is satisfiable. Also, if ϕ is a conflict set, then (ϕ, ∅, G V ar(ϕ) ∅
) is a quasi-conflict set.

Example 5 Let us consider the theory LA and the set of literals ϕ

= {z = x + y, x -y = 1, x = y + u, u = 0}. Let G denote the explanation graph ({x, y}, {x = y}) such that L G (x = y) = {x = y + u, u = 0}. Then ({x -y = 1}, {x = y}, G) is a quasi-conflict set of ϕ. Proposition 7 If (ψ, E, G) is a quasi-conflict set of ϕ, then ψ ∪ Lit(G) is a conflict set of ϕ. Proof: If (ψ, E, G) is a quasi-conflict set of ϕ, then ψ ∪ E is unsatisfiable. By definition, Lit(G) ⊆ ϕ and Lit(G) entails E. Consequently, ψ ∪ Lit(G) is unsatisfiable and ψ ∪ Lit(G) ⊆ ϕ. So ψ ∪ Lit(G) is a conflict set of ϕ. Given a quasi-conflict set (ψ, E, G) of ϕ, ψ ∪ Lit(G) is called the conflict set associated to (ψ, E, G). Example 6 (Example 5 continued). The conflict set associated to ({x -y = 1}, {x = y}, G) is {x -y = 1, x = y + u, u = 0}.
The set Lit(G) provides an explanation of equalities in E, but it is a superset of what we need: it is sufficient to consider the subgraph of G obtained by focusing only on the paths in G "connecting" the equalities in E.

Definition 6 Let G be an explanation graph of ϕ, x = y ∈ CP (G) and E ⊆ CP (G). The set of explanation edges of x = y in G is the subset of Edge(G) defined as follows:

Exe(G, x = = ElemP ath(G, x, y) ∪ ( e∈ElemP ath(G,x,y) e ′ ∈L G (e)\ϕ Exe(G, e ′ )). The set of explanation edges of E in G is ExE(G, E) = e∈E Exe(G, e).
The restriction of

G to E is the subgraph G |E of G such that Edge(G |E ) = ExE(G, E) and ∀e ∈ Edge(G |E ), L G |E (e) = L G (e). Proposition 8 G |E is minimal for E iff G |E is minimally explained. Proof: (⇐) Let us assume that G |E is not minimal for E. There exists G ′ ❁ G |E such that E ⊆ CP (G ′ ). If G ′ ⊂ G |E , then this would contradict the fact that E ⊆ CP (G ′ ). Therefore, Edge(G ′ ) = Edge(G) and there exists an edge e of G ′ such that L G ′ (e) ⊂ L G |E (e). So G |E is not minimally explained. (⇒) If G |E is not minimally explained, then it is possible to construct a graph G ′ ❁ G |E such that E ⊆ CP (G ′ ). Consequently, G |E is not minimal for E.
We are now ready to give a characterization of minimal quasi-conflict sets.

Theorem 7 A quasi-conflict set (ψ, E, G) is minimal iff ψ ∪ E is a minimal conflict set and G is minimal for E.
Proof: (⇐) By contradiction, assuming that there exists a quasi-conflict set

(ψ ′ , E ′ , G ′ ) such that (ψ ′ , E ′ , G ′ ) ≺ (ψ, E, G). If ψ ′ ⊂ ψ or E ′ ⊂ E, then this would contradict that ψ ∪ E is a minimal conflict set. Therefore ψ ′ = ψ, E ′ = E and G ′ ❁ G, where E ⊆ CP (G ′ ). This contradicts that G is minimal for E. (⇒) If ψ ∪ E is not a minimal conflict set or G is not minimal for E, then it is possible to construct a quasi-conflict set (ψ ′ , E ′ , G ′ ) such that (ψ ′ , E ′ , G ′ ) ≺ (ψ, E, G).
Example 7 (Example 5 continued). The quasi-conflict set ({xy = 1}, {x = y}, G) is minimal since {xy = 1, x = y} is a minimal conflict set and G is minimal for {x = y}.

INRIA

Explanation Engines and Their Combination

We now adapt the combination algorithm depicted in Figure 6 for deduction complete satisfiability procedures in order to generate T 1 ∪T 2 -conflict sets. More generally, the goal is to built an explanation for each truth value returned by a satisfiability procedure. To develop our main combination result, we introduce the notion of explanation engine: this is a component capable of computing (1) an explanation graph in case of satisfiability and (2) a quasi-conflict set in case of unsatisfiability.

Definition 7 (Explanation engine) Let T be a theory and L be a set of (finite) sets of non-elementary T -literals closed under union. A T -explanation engine for L is a T -satisfiability procedure, denoted by µEX T , such that, for any Ω ∈ L and any minimal set of elementary equalities E:

1. If Ω∪E is T -satisfiable, then µEX T returns true{G} where G is deduction complete for Ω ∪ E. 2. If Ω ∪ E is T -unsatisfiable, then µEX T returns f alse{(Ω ′ , E ′ , G)} where (Ω ′ , E ′ , G) is a quasi-conflict set of Ω ∪ E.
If µEX T computes minimal quasi-conflict sets and minimally explained explanation graphs, then µEX T is said minimal.

Remark 1 As shown in [START_REF] Ranise | Combining Proof-Producing Decision Procedures[END_REF], the Gauss elimination algorithm can be adapted to build minimal LA-conflict sets and minimal LA-explanations of elementary equalities, and so minimal quasi-conflict sets and minimally explained explanation graphs. This allows us to obtain a minimal LA-explanation engine. As another example, a congruence closure algorithm computing a minimally explained explanation graph for any given set of flat equalities (see end of Section 5.2) provides a minimal E-explanation engine for all sets of flat equalities.

Figure 7 presents a variant of the Nelson-Oppen combination method for the union of two arbitrary signature-disjoint, stably infinite, and convex theories where explanation engines are used in place of satisfiability procedures, and where explanation graphs are used to encode the entailment of elementary equalities together with their explanations.

Theorem 8 Let T 1 and T 2 be two signature-disjoint convex and stably infinite theories such that for each i = 1, 2, a T i -explanation engine for L i , E be a set of elementary equalities and ∆ a set of elementary disequalities. Let

Ω i ∈ L i for i = 1, 2, ϕ = m(Ω 1 ∪ Ω 2 ∪ ∆ ∪ E)
and S ′ be a final configuration obtained by the repeated application of the rules of Figure 7 on the initial configuration

S = Ω 1 ; ∆; U F V ar(ϕ) (E); Ω 2 . ❼ If S ′ is of the form f alse{(Ω ′ , E ′ , G)}, then ϕ is T 1 ∪ T 2 -unsatisfiable and (Ω ′ , E ′ , G) is a quasi-conflict set of ϕ.
❼ Otherwise, S ′ is of the form Ω 1 ; ∆; G; Ω 2 and ϕ is T 1 ∪ T 2 -satisfiable. Furthermore, G is deduction complete for ϕ modulo T 1 ∪ T 2 .

Proof: It follows directly from Theorem 6. The rules depicted in Figure 7 can be seen as a refinement of rules in Figure 6, where an explanation graph a T 1 ∪ T 2 -explanation engine. Given two explanation engines respectively for L 1 and L 2 , as defined in Definition 7, we get an explanation engine for L 1 ∪ L 2 , where L 1 ∪ L 2 denotes the smallest set closed under union including L 1 and L 2 .

Corollary 2 (Modular construction of explanation engines) Let T 1 and T 2 be two signature-disjoint, convex, and stably infinite theories such that a T 1explanation engine for L 1 and a T 2 -explanation engine for L 2 are known. The combination rules depicted in Figure 7 provide a T 1 ∪ T 2 -explanation engine for L 1 ∪ L 2 . Moreover, this T 1 ∪ T 2 -explanation engine is minimal if the T 1explanation engine and the T 2 -explanation engine are minimal.

Proof: The preservation of minimality follows from Proposition 8 and Theorem 7.

Conclusion and Related Work

Rational reconstruction. Our presentation of combination schemas for disjoint unions of theories in various classes highlights the key ideas underlying each combination and allows proofs of correctness which are easy to grasp.

Similarly to [START_REF] Ganzinger | Shostak light[END_REF], the abstract schema presented in Section 3.2 for combining SH theories seems to emphasize the importance of the solver w.r.t. the canonizer. In fact, if the solved form returned by the solver is also canonical, the canonizer can be trivially implemented as the identity function. Nonetheless, we believe that the concept of canonizer is quite important mainly for two reasons. First, it offers the entry point to refinements of the proposed schema to increase efficiency. In fact, solving a set of equalities in "one-shot", as done when applying rule Solvesuccess 1 , may not be as efficient as solving equalities incrementally, as e.g. in [START_REF] Rueß | Deconstructing Shostak[END_REF][START_REF] Kapur | A rewrite rule based framework for combining decision procedures[END_REF]. This can be incorporated in our schema by refining the inference system SH along the lines described in [START_REF] Conchon | Strategies for combining decision procedures[END_REF] so that the solver is applied to only one equality at a time and the canonizer needs to return a canonical form for arbitrary terms. The second reason is that the concept of canonizer is a useful basic building block, together with solvers, for constructing what we have called deduction complete satisfiability procedures (cf. Section 4).

The particular case of combining a SI-theory (e.g., the theory of equality E) and one in SH considered in Section 3.3 has been extensively studied by many researchers following [START_REF] Shostak | Deciding combinations of theories[END_REF]. It is possible to derive the correctness of such combination schemas in our framework by using the following observations: (i) NO, SH, NS are correct, (ii) the class of theories CSI is closed under disjoint union, and (iii) the class SH is contained in CSI. Similar results are given in [START_REF] Manna | Combining decision procedures[END_REF]. As an additional remark, we mention the possibility of refining the abstract inference systems presented here with strategies as done in [START_REF] Conchon | Strategies for combining decision procedures[END_REF], so to get a more fine-grained rule-based implementation which mimics a Shostak procedure as described in [START_REF] Rueß | Combining shostak theories[END_REF]. We have not done this here, since we were more focused on modularity rather than efficiency.

Non-stably infinite theories. In [START_REF] Barrett | A generalization of Shostak's method for combining decision procedures[END_REF], the authors have shown that all convex theories with no trivial models are stably infinite, and therefore they can be combined using the NO combination schema. In Section 3.4, we go a step further by showing that arbitrary convex theories can be combined provided that we know whether component theories admit a trivial model or not. In practice this requirement is not restrictive as almost all useful theories enjoy this property. Our result is along the line of [START_REF] Bonacina | Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures[END_REF] in which the class of ∃ n -decidable and ∃ ∞decidable theories is defined and shown to be modular. Basically ∃ n -decidability (resp. ∃ ∞ -decidability) allows us to check the existence of a model of finite (resp. infinite) cardinality. The combination method proposed in Section 3.4 exploits the hypothesis of convexity and the fact that we know whether or not component theories have a trivial model. It can be seen as an instance with a more operational flavour of the non-deterministic method of [START_REF] Bonacina | Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures[END_REF].

Deduction completeness. We have introduced the notion of deduction complete satisfiability procedure and defined the class of theories DCCSI. Basically they have satisfiability procedures defined as inference-based systems with the capability of computing all entailed elementary equalities with no overhead. We have shown that the class of DCCSI theories is closed under disjoint union. The concept of deduction complete inference-based satisfiability procedures offers an interesting trade-off between modularity and efficiency for the problem of solving satisfiability in disjoint combinations of theories under a common interface.

There were some attempts in the development of SMT solving to extend decision procedures with the capability of deriving entailed facts while checking for satisfiability (see, e.g., [START_REF] Sebastiani | Lazy Satisfiability Modulo Theories[END_REF] for an overview on this and related issues). However, in such a line of work, deduced facts are used to prune the search space of a Boolean solver rather than to combine procedures and completeness is regarded as detrimental to performances. In this paper, we restrict our interest to inference-based satisfiability procedures for convex theories built over the equality predicate only. An interesting direction to explore is to consider inference-based satisfiability procedures for arbitrary convex theories involving other predicates than equality and generalize the deduction completeness approach in that case.

Modularity of conflict sets. We have also proposed a method to modularly build conflict sets in unions of theories by refining the Nelson-Oppen combination schema. The key concept of explanation graph allows us to encode the fact that a certain elementary equality is a logical consequence of a set of elementary equalities. Explanation engines formalize proof-producing procedures capable of computing explanation graphs. We have shown how to re-use efficient proofproducing procedures available in the literature to build explanation engines. Furthermore, explanation engines for unions of several theories can be obtained as a by-product of our combination method. A suitable notion of minimality related to quasi-conflict sets in unions of theories was also investigated.

An alternative approach to producing conflict sets in combinations of theories has been proposed in [START_REF] Bozzano | Efficient theory combination via boolean search[END_REF], which does not require the direct combination of the solvers for the component theories. While the technique of [START_REF] Bozzano | Efficient theory combination via boolean search[END_REF] may yield better performances for SMT problems, we believe our combination method could become a key ingredient in the certification of the results produced by solvers to be integrated in skeptical proof assistants (see, e.g., [START_REF] Fontaine | Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants[END_REF]). In a slightly different context, our techniques could also be used to build equational reasoners having the capability of computing a (small) witness of unsatisfiability for equational INRIA problems such as unification, matching, and word problems. For equational theories, there are satisfiability procedures with the property of deriving elementary equalities (like unification or matching algorithms) and deductive combination methods based on the propagation of elementary equalities [START_REF] Boudet | Combining unification algorithms[END_REF][START_REF] Nipkow | Combining matching algorithms: The regular case[END_REF]. Applying the techniques developed here to more general equational reasoners appears to be a promising line of research.

  r), and l = r is selected in its clauseSubsumption S ∪ {C, C ′ } S ∪ {C} if for some subs. θ, θ(C) ⊆ C ′ Deletion S ∪ {Γ ⇒ ∆, t = t} Swhere C and C ′ are clauses and S is a set of clauses.

Figure 5 :

 5 Figure 5: Contraction Rules of SP.

  t. SP contains only literals of the following forms: (a) the empty clause, (b) the axioms in Ax(L), (c) ground flat literals, and (d) equalities of the form cons(b, cdr(a)) = a or cons(car(a), b) = a, where a, b are constants. Again by Theorem 5, L is stably infinite and (SP, Ax(L)) is deduction complete for L.

  By induction on the length of the derivation w.r.t. SP, it is easy to show that for any set of ground flat literals S, the saturation of Ax(L) ∪ S w.r.t. SP contains only clauses of the following forms: (a) the empty clause, (b) the axioms in Ax(SC), (c) ground flat literals, (d) clauses of the form a = b ⇒ a ′ = b ′ , where a, b, a ′ , b ′ are constants, and clauses of the forms:

Figure 6 :

 6 Figure 6: Combination of deduction complete satisfiability procedures

Example 4

 4 Consider the theory of equality E and the set of literals ϕ = {a = f (a), b = f (c), c = f (a)}. Two explanation graphs of ϕ are depicted below: ), c=f(a) a=f(a), b=f(c),a=c a=f(a), c=f(a) b=f(c),c=f(a),a=c

  thanks to Lemma 7, Lemma 8, and the definition of canon. Then the proof can be continued by contradiction in a way similar to the proof of Lemma 5.It is easy to see that a strategy applying rules Solvefail 1 , Solvesuccess 1 , and Contradiction 1 in SH to a configuration Γ 1 , ∆ 1 ; Γ 2 , ∆ 2 yields the same result as that of applying rule Contradiction 1

  where x, y are new variables. Now, we only need to check if Φ 2 ∪ Φ 0 is satisfiable in a trivial model of T 2 . To this end, it is sufficient to verify whether Φ 2 ∪ Φ 0 contains a disequality. Indeed, Φ 2 ∪ Φ 0 is satisfiable in a trivial model of T 2 iff Φ 2 ∪ Φ 0 does not contain any disequalities and T 2 has a trivial model.

  The inference system SP uses a selection function sel such that for each clause C, sel(C) contains a negative literal in C if C contains one, otherwise all maximal literals in C w.r.t. ≻. SP contains two kind of rules: Expansion Rules and Contraction Rules. Expansion Rules are necessary for refutation completeness of SP. Contraction Rules are crucial for efficiency, and they are required to be performed eagerly whenever possible.

  written in sequent style as {A 1 , . . . , A n } ⇒ {B 1 , . . . , B m } (where the A i 's and B j 's are equalities), equality is the only predicate symbol, σ is the most general unifier of u and u

′ , u ′ is not a variable in Left paramodulation and Right paramodulation, L is a literal, and:

A set of literals S entails a formula φ iff S ∪ {¬φ} is unsatisfiable.INRIA

RR n➦ 6688

The satisfiability of any quantifier-free formula can be reduced to the satisfiability of sets of literals by converting to disjunctive normal form and then splitting on disjunctions, i.e. checking whether S 1 ∨ S 2 (where S 1 and S 2 are conjunction of literals) is T -satisfiable reduces to checking the T -satisfiability of either S 1 or S 2 .

A symmetric rule for T 2 is obtained from a rule for T 1 by swapping indexes 1 and 2. A symmetric inference system for T 2 is the set of symmetric rules for T 2 obtained from the rules for T 1 .RR n➦ 6688

Horn theories are known to be convex.RR n➦

Let X be a set, 2 X denotes the power-set of X.INRIA

U F abbreviates Union-Find since the sequence of insertions is typically implemented using this data structure (see[START_REF] Fontaine | Techniques for Verification of Concurrent Systems with Invariants[END_REF][START_REF] De Moura | Justifying equality[END_REF][START_REF] Nieuwenhuis | Proof-Producing Congruence Closure[END_REF]).RR n➦ 6688

∆ is a set of elementary disequalities. Symmetric rules are not depicted here for the sake of conciseness and they can be obtained by changing the subscript 1 into 2 in the rules above. The function M erge is defined as follows: G represents the set of elementary equalities E and explanation engines µEX T correspond to deduction complete satisfiability procedures DC T . Assuming E = Eq(G), there is an obvious correspondence between the two sets of rules:

Theorem 8 has an interesting consequence. If the previous combination algorithm is applied with an empty set of elementary disequalities ∆, it provides INRIA