Ali Hannouche

Chebbo Ghassan

Claude Joannis

Évaluation de la contribution des dépôts aux flux de matières en suspension par temps de pluie dans les réseaux d'assainissement unitaires

teaching and research institutions in France or abroad, or from public or private research centers.

Évaluation de la contribution des dépôts aux flux de matières en suspension par temps de pluie dans les réseaux d'assainissement unitaires

Ali Hannouche 1 ; Claude Joannis 2 , Ghassan Chebbo 1

1 Laboratoire eau environnement et système urbain, 6-8 avenue Blaise Pascal, Cité Descartes, Champs sur Marne 77 455 Marne-La-Vallée Cedex 2, France -Ali.hannouche@Leesu.enpc.fr 2 Institut Français des Sciences et Technologies des Transports, de l'Aménagement et des Réseaux, Route de Bouaye CS4, 44344 Bouguenais Cedex, France -nicolas.hemmerle@ifsttar.fr

Trois sources de polluants de temps de pluie ont été déterminées à l'exutoire des réseaux d'assainissement unitaires : les eaux usées, les eaux de ruissellement et le stock de dépôt contenu dans le réseau. Plusieurs études ont évalué la contribution de ces trois sources au moyen d'un bilan de masses à partir de quelques événements pluvieux [START_REF] Krejci | Contribution of different sources to pollutant loads in combined sewers[END_REF]Chebbo, 1992;[START_REF] Gromaire | Contribution of different sources to the pollution of wet weather flows in combined sewers[END_REF][START_REF] Soonthornnonda | Source apportionment of pollutants and flows of combined sewer wastewater[END_REF]Gasperi et al., 2010). Les résultats obtenus mettent en évidence le rôle important des dépôts comme une source significative de MES, voire majeure, lors des épisodes pluvieux. Ces contributions ont été évaluées pour des réseaux d'assainissement surdimensionnés pour les écoulements de temps sec, de faible pente, présentant des zones connues d'accumulation de dépôts (grossiers) (Ahyerre et al., 2001;[START_REF] Gromaire | Localisation, nature et dynamique des dépôts à l'interface eau-sédiments en réseau d'assainissement unitaire[END_REF] Paris, France (in French). Gasperi, J., Gromaire, M.C., Kafi, M., Moilleron, R., and Chebbo, G. (2010). Contributions of wastewater, runoff and sewer deposit erosion to wet weather pollutant loads in combined sewer systems. Water Research 44, 5875-5886.

  un événement pluvieux ne correspond pas à la somme des masses en provenance des eaux usées et des eaux de ruissellement, cette dernière composante étant minoritaire. La contribution des dépôts dans le réseau se situe entre 20 et 80% de la masse de MES observés à l'exutoire en temps de pluie. La robustesse de cette estimation a été établie par une étude de sensibilité aux incertitudes et aux hypothèses affectant le bilan. Ces résultats confirment et affinent les évaluations obtenues précédemment(Gasperi et al., 2010) sur le réseau d'assainissement parisien. De plus, à l'échelle d'un événement pluvieux le dépôt mobilisé ne représente qu'une faible épaisseur si on rapporte la masse érodée concernée à une surface de collecteur immergée par temps sec : de l'ordre de 1 à 3 mm le long de l'ensemble du collecteur du Clichy. Ils montrent aussi que cette contribution n'est pas spécifique au réseau parisien de faible pente et surdimensionné mais aussi elle est importante dans un réseau d'assainissement comme celui d'Ecully qui a une pente de 2.7% contre 0,14% pour le réseau de Clichy et il ne présente pas aussi de zones connues d'accumulation de sédiments. Solides des rejets pluviaux urbains. Caractérisation et traitabilité (Solids in urban wet weather discharges: characterization and treatment), PhD Thesis, Ecole Nationale des Ponts et Chaussées,

	Références
	Ahyerre, M., Chebbo, G., and Saad, M. (2001). Nature and dynamics of water sediment interface in combined
	sewers. Journal of Environmental Engineering-Asce 127, 233-239.
	Chebbo, G. (1992).

. Par ailleurs la quantification précise des différentes entrées (eaux usées, eaux de ruissellement) et de leur variabilité a souvent été abordée de manière simplifiée. En effet, ces études ont été menées sur un nombre restreint d'événements pluvieux en les comparant à quelques journées de temps sec, sur la base d'échantillons prélevés in situ à des intervalles de temps de plusieurs minutes voire plusieurs dizaines de minutes. Ces évaluations soulèvent certaines questions concernant l'importance de l'effet des incertitudes dans le calcul et nécessitent pourtant une bonne description des entrées incluant leur variabilité. Dans le cadre du réseau d'observatoires français SOERE « URBIS » ont été constituées des bases de données de mesure en continu de la turbidité cumulant plusieurs centaines d'événements pluvieux et autant de journées sèches pour deux sites de caractéristiques différentes : Clichy à Paris et Ecully à Lyon. Ces mesures, converties en concentration en matières en suspension (MES) par des relations MES-Turbidité et couplées avec un modèle de concentrations moyennes événementielles des eaux de ruissellement, ont permis d'évaluer la contribution des dépôts aux masses événementielles des MES observées à l'exutoire de deux bassins versants de caractéristiques très différentes. La contribution des trois sources aux flux de MES à l'échelle de l'événement a été évaluée par une approche de bilan de masse entre l'entrée (eaux usées et eaux de ruissellement) et la sortie (exutoire) du réseau de chaque bassin versant a été réalisée. La méthode proposée permet de prendre en compte toutes les sources d'incertitudes et de variabilité des entrées et de la sortie. Les bilans réalisés sur des bases de données représentatives (88 événements pluvieux à Clichy et 200 événements à Ecully) consolident les résultats similaires suggérés par d'autres études : la masse en MES transitée à l'exutoire pendant


Elena Tushkanova

Christophe Ringeissen

Alain Giorgetti

Olga Kouchnarenko

Automatic Decidability for Theories with Counting Operators (Presentation-only paper)

Introduction

Decision procedures for satisfiability modulo background theories of classical datatypes are at the core of many state-of-the-art verification tools. Designing and implementing these satisfiability procedures remains a very hard task. To help the researcher with this time-consuming task, an important approach based on rewriting has been investigated in the last decade [START_REF] Armando | A rewriting approach to satisfiability procedures[END_REF][START_REF] Armando | New results on rewrite-based satisfiability procedures[END_REF]. The rewriting-based approach allows building satisfiability procedures in a flexible way by using a general calculus for automated deduction, namely the paramodulation calculus [START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF] (also called superposition calculus). The paramodulation calculus is a refutationcomplete inference system at the core of all equational theorem provers. In general this calculus provides a semi-decision procedure that halts on unsatisfiable inputs by generating an empty clause, but may not terminate on satisfiable ones. However, it also terminates on satisfiable inputs for some theories axiomatising standard datatypes such as arrays, lists, etc, and thus provides a decision procedure for these theories. A classical termination proof consists in considering the finitely many cases of inputs made of the (finitely many) axioms and any set of ground flat literals. This proof can be done by hand, by analysing the finitely many forms of clauses generated by saturation, but the process is tedious and error-prone. To simplify this process, a schematic paramodulation calculus has been developed [START_REF] Lynch | Automatic decidability[END_REF] to build the schematic form of the saturations. It can be seen as an abstraction of the paramodulation calculus: If it halts on one given abstract input, then the paramodulation calculus halts for all the corresponding concrete inputs. More generally, schematic paramodulation is a fundamental tool to check important properties related to decidability and combinability [START_REF] Lynch | Automatic decidability and combinability[END_REF].

To ensure efficiency, it is very useful to have built-in axioms in the calculus, and so to design paramodulation calculi modulo theories. This is particularly important for arithmetic fragments due to the ubiquity of arithmetics in applications of formal methods. For instance, paramodulation calculi have been developed for Abelian Groups [START_REF] Godoy | Superposition with completely built-in abelian groups[END_REF][START_REF] Nicolini | Combinable extensions of Abelian groups[END_REF] and Integer Offsets [START_REF] Nicolini | Satisfiability procedures for combination of theories sharing integer offsets[END_REF]. In [START_REF] Nicolini | Satisfiability procedures for combination of theories sharing integer offsets[END_REF], the termination of paramodulation modulo Integer Offsets is proved manually. Therefore, there is an obvious need for a method to automatically prove that an input theory admits a decision procedure based on paramodulation modulo Integer Offsets.

In this paper, we introduce theoretical underpinnings that allow us to automatically prove the termination of paramodulation modulo Integer Offsets. To this aim, we design a new schematic paramodulation calculus to describe saturations modulo Integer Offsets. Our approach requires a new form of schematization to cope with arithmetic expressions. The interest of schematic paramodulation relies on a correspondence between a derivation using (concrete) paramodulation and a derivation using schematic paramodulation: Roughly speaking, the set of derivations obtained by schematic paramodulation over-approximates the set of derivations obtained by (concrete) paramodulation.

Our approach has been developed and validated thanks to a proof system [START_REF] Tushkanova | A rule-based framework for building superposition-based decision procedures[END_REF] implemented in the rewriting logic-based environment Maude.

Paramodulation Calculus

As in [START_REF] Tushkanova | A rule-based framework for building superposition-based decision procedures[END_REF] we consider only unitary clauses, i.e. clauses composed of at most one literal. The Unitary Paramodulation Calculus, denoted by UPC [START_REF] Tushkanova | A rule-based framework for building superposition-based decision procedures[END_REF] corresponds to the standard paramodulation calculus restricted to the case of unit clauses.

The paramodulation-based calculus UPC I defined in [START_REF] Nicolini | Satisfiability procedures for combination of theories sharing integer offsets[END_REF] adapts the paramodulation calculus UPC to the theory of Integer Offsets, so that it can serve as a basis for the design of decision procedures for Integer Offsets extensions. Technically, the axioms of the theory of Integer Offsets are directly integrated in the simplification rules of UPC I . The theory of Integer Offsets is axiomatized by the set of axioms {∀X. s(X) = 0, ∀X, Y. s(X) = s(Y ) ⇒ X = Y , ∀X. X = s n (X) for all n ≥ 1} over the signature Σ I := {0 : int, s : int → int}. Compared to [START_REF] Bonacina | On Variable-inactivity and Polynomial T-Satisfiability Procedures[END_REF], our theory of Integer Offsets does not consider the predecessor function. Following [8, Section 5], a possible Integer Offsets extension is the theory LLI of lists with length whose signature is Σ LLI = {car : lists → elem, cdr : lists → lists, cons : elem × lists → lists, len : lists → int, nil :→ lists, 0 :→ int, s : int → int} and whose set of axioms Ax(LLI) is {car(cons(X, Y )) = X, cdr(cons(X, Y )) = Y, len(cons(X, Y )) = s(len(Y )), cons(X, Y ) = nil, len(nil) = 0}.

Schematic Paramodulation

The Schematic Unitary Paramodulation Calculus SUPC is an abstraction of UPC. Indeed, any concrete saturation computed by UPC can be viewed as an instance of an abstract saturation computed by SUPC [6, Theorem 2]. Hence, if SUPC halts on one given abstract input, then UPC halts for all the corresponding concrete inputs. More generally, SUPC is an automated tool to check properties of UPC such as termination, stable infiniteness and deduction completeness [START_REF] Lynch | Automatic decidability and combinability[END_REF].

SUPC is almost identical to UPC, except that literals are constrained by conjunctions of atomic constraints of the form const(x) which restricts the instantiation of the variable x by only constants. An implementation of Paramodulation and Schematic Paramodulation calculi UPC and SUPC is presented in [START_REF] Tushkanova | A rule-based framework for building superposition-based decision procedures[END_REF].

In the following, we extend the schematic calculus SUPC for UPC to get a schematic calculus for UPC I , named SUPC I .

Schematic Paramodulation Calculus for Integer Offsets

This section introduces a new schematic calculus named SUPC I . It is a schematization of UPC I taking into account the axioms of the theory of Integer Offsets within a framework based on schematic paramodulation [START_REF] Lynch | Automatic decidability and combinability[END_REF][START_REF] Tushkanova | A rule-based framework for building superposition-based decision procedures[END_REF].

The theory of Integer Offsets allows us to build arithmetic expressions of the form s n (t) for n ≥ 1. The idea investigated here is to represent all terms of this form in a unique way. To this end, we consider a new operator s + : int → int such that s + (t) denotes the infinite set of terms {s n (t) | n ≥ 1}. Let us introduce the notions of schematic clause and instance of schematic clause handled by SUPC I . These notions extend the ones used in [START_REF] Lynch | Automatic decidability and combinability[END_REF] for the schematization of PC.

Definition 1 (Schematic Clause) A schematic clause is a constrained clause built over the signature extended with s + . An instance of a schematic clause is a constraint instance where each occurrence of s + is replaced by some s n with n ≥ 1.

The calculus SUPC I takes as input a set of schematic literals, G 0 , that represents all possible sets of ground literals given as inputs to UPC I :

G 0 = {⊥, x = y const(x, y), x = y const(x, y), u = s + (v) ϕ} ∪ f ∈Σ T {f (x 1 , . . . , x n ) = x 0 const(x 0 , x 1 , . . . , x n )}
where u, v are flat terms of sort int whose variables are all constrained (in ϕ), and x, y are constrained variables of the same sort.

The calculus SUPC I is depicted in Fig. 1. It re-uses most of the rules of SUPC -Figs. 1(a) and 1(b) -and complete them with one new contraction rule named Schematic Deletion and two reduction rules -presented in Fig. 1(c)which are simplification rules for Integer Offsets.

Whenever a literal is generated by superposition or simplification, the rewrite system Rs + = { s + (s(x)) → s + (x), s(s + (x)) → s + (x), s + (s + (x)) → s + (x) } is applied eagerly to simplify terms containing s + . The rewrite system Rs + is also applied in the Schematic Deletion rule to implement a form of subsumption check via a morphism π replacing all the occurences of s by s + (π(s(t)) = s + (π(t)) for any t, π(x) = x if x is a variable).

It is important to note that SUPC I may diverge without the new Schematic Deletion rule. To illustrate this point, let us take a look at the theory of lists with length. In fact, the calculus generates a schematic clause len(a) = s(len(b)) const(a, b) which will superpose with a renamed copy of itself, i.e. with

Superposition l[u ′ ] ⊲⊳ r ϕ u = t ψ σ(l[t] ⊲⊳ r ϕ ∧ ψ) if i) σ(u) ≤ σ(t), ii) σ(l[u ′ ]) ≤ σ(r), and iii) u ′ is not an unconstrained variable.

Above, u and u ′ are unifiable and σ is the most general unifier of u and u ′ .

(a) Schematic expansion inference rules

, where σ is a renaming or a mapping from constrained variables to constrained variables.

Above, all the variables in u, v, t are constrained. As in [START_REF] Lynch | Automatic decidability[END_REF][START_REF] Lynch | Automatic decidability and combinability[END_REF], we are interested in satisfying the following properties:

-Any clause in a saturation generated by the paramodulation calculus with any possible input is an instance of a schematic clause in a saturation generated by the schematic paramodulation calculus with the input G 0 . -The termination of the schematic paramodulation calculus with the input G 0 implies the termination of the paramodulation calculus with any possible input.

The new form of schematization introduced for arithmetic expressions requires adapting the proofs done for the standard case [START_REF] Tushkanova | Automatic Decidability for Theories with Counting Operators[END_REF]. Our schematic paramodulation calculus for Integer Offsets provides us with an automatic proof method for the theories considered in [START_REF] Nicolini | Satisfiability procedures for combination of theories sharing integer offsets[END_REF], where the termination proofs are done manually.


Serdar Erbatur

Deepak Kapur

Andrew M Marshall

Paliath Narendran

Christophe Ringeissen

Hierarchical Combination of Unification Algorithms (Extended Abstract)

Introduction

A critical question in unification theory is how to obtain a unification algorithm for the combination of non-disjoint equational theories when there exists unification algorithms for the constituent theories. The problem is known to be difficult and can easily be seen to be undecidable in the general case. Therefore, previous work has focused on identifying specific conditions and methods in which the problem is decidable. We continue the investigation in this paper, building on previous combination results, [START_REF] Baader | Unification in the union of disjoint equational theories: Combining decision procedures[END_REF][START_REF] Domenjoud | Combination techniques for non-disjoint equational theories[END_REF][START_REF] Ringeissen | Unification in a combination of equational theories with shared constants and its application to primal algebras[END_REF] and [START_REF] Erbatur | Unification over distributive exponentiation (sub)theories[END_REF]. We are able to develop a novel approach to the non-disjoint combination problem. The approach is based on a new set of restrictions and combination method such that if the restrictions are satisfied the method produces an algorithm for the unification problem in the union of non-disjoint equational theories.

A full version of this paper [START_REF] Erbatur | Hierarchical combination[END_REF] will appear in the proceedings of the 24th International Conference on Automated Deduction (CADE-24).

Preliminaries

We use the standard notation of equational unification [START_REF] Baader | Unification theory[END_REF] and term rewriting systems [START_REF] Baader | Term rewriting and all that[END_REF]. A Σ-rooted term is a term whose top symbol is in Σ

. Let Σ (1,2) = Σ 1 ∩ Σ 2 . An alien subterm of a Σ 1 Σ (1,2) -rooted term t (resp. Σ 2 -rooted term) is a Σ 2 -rooted subterm (resp. Σ 1 Σ (1,2) -rooted subterm) of t such that all its superterms are Σ 1 Σ (1,2) -rooted (resp. Σ 2 -rooted).
A theory E is subterm collapse-free if and only if for all terms t it is not the case that t = E u where u is a strict subterm of t. Given a signature Σ ′ ⊆ Σ, S| Σ ′ denotes the set of Σ ′ -equations occurring in S. A set of equations S is said to be in standard form over a signature Σ if and only if every equation in S is of the form x = ? t, where x is a variable and t is one of the following: (a) a variable different from x, (b) a constant, or (c) a term of depth 1 that contains no constants, i.e., function symbols applied to variables. It is not generally difficult to decompose equations of a given problem into simpler standard forms. A set of equations is said to be in dag-solved form (or d-solved form) if and only if they can be arranged as a list x 1 = ? t 1 , . . . , x n = ? t n where (a) each left-hand side x i is a distinct variable, and (b) ∀ 1 ≤ i ≤ j ≤ n: x i does not occur in t j . Each x i in this case is called a solved variable. A set of equations S is said to be in Σ-solved form if and only if it is in standard form and S| Σ is in dag-solved form. For a convergent rewrite system R we define a constructor of R to be a function symbol f which does not appear at the root on the left-hand side of any rewrite rule of R. We define an inner constructor to be a constructor f that satisfies the following additional restrictions: (i) f does not appear on the left-hand side on any rule in R, (ii) f does not appear as the root symbol on the right-hand side of any rule in R, and (iii) there are no function symbols below f on the right-hand side of any rule in R.

Combination Procedure

We want to investigate conditions to build an E 1 ∪ E 2 -unification algorithm by using two algorithms A 1 and A 2 solving two different kinds of E 1 ∪ E 2 -unification problems, described below in Restriction 1 and Restriction 2 respectively. Consider an E 1 ∪ E 2 -unification problem P in standard form. The steps of the combination procedure (see Figure 2) are as follows: (1) run A 1 on the Σ 1 Σ (1,2) -equations of P; (2) run A 2 on the Σ 2 -equations of the unification problem obtained at step (1); (3) collect the resulting problems that are in dag-solved form. As in disjoint combination [START_REF] Baader | Unification in the union of disjoint equational theories: Combining decision procedures[END_REF], we perform as step (0) a variable identification in order to guess a priori all possible identifications of variables occurring in P. For this approach to work we need to place some restrictions.

Restrictions

We present a less technical overview of the required restrictions (see [START_REF] Erbatur | Hierarchical combination[END_REF] for more details). Consider two subterm collapse-free equational theories such that Σ 1 ∩ Σ 2 = Σ (1,2) = ∅. Fresh variables created by A 1 that could cause the need for reapplication of the rules of A 1 during the application of A 2 are called "Ping-Pong Variables" as it implies a back-and-forth mechanism between the algorithms.

Restriction 1. (on Algorithm

A 1 ) Let P be a set of Σ 1 Σ (1,2) -equations. Algorithm A 1 computes a set of problems {Q k } k∈K such that k∈K CSU E1∪E2 (Q k ) is a CSU E1∪E2 (P) and for each k ∈ K: (i) Q k consists of (Σ 1 Σ (1,2) )-equations and Σ (1,2) -equations. (ii) Q k is in standard form and (Σ 1 Σ (1,2) )-solved form. (iii) No fresh variable occurring in a nonvariable Σ (1,2) -term in Q k appears as solved in Q k .
(CSU stands for "complete set of unifiers".) Note that A 1 is a special type of algorithm that returns a "partial" solution to an E 1 ∪ E 2unification problem. A 1 is needed to solve some portion of the problem, namely the Σ 1 Σ (1,2)pure, but a standard E 1 -unification algorithm is not sufficient, even for Σ

1 Σ (1,2) -pure E 1 ∪ E 2 problems.
Example 3.1. Let E 1 := {h(a, x, y) = g(x * y), h(b, x, y) = g(y * x)} and let E 2 be the commutative theory for * . Then, h(a, a, z)

= ? h(b, a, b) is not solvable in E 1 but is in E 1 ∪ E 2 .
Restriction 1 ensures that completeness is not lost by ensuring that a CSU for all the partial solutions is a CSU for the original problem.

To explain Restriction 1(iii), let us note that A 1 may generate fresh Σ (1,2) -equations, e.g. z = ? f (x, y) where f ∈ Σ (1,2) , together with some Σ 1 Σ (1,2) -equations, e.g. x = ? s, y = ? t. If A 2 later generates x = ? y, then this may lead to the reapplication of A 1 , to solve x = ? s, x = ? t. If x and y are from the initial set of variables, this problem can be discarded without loss of generality, since the variable identification performed initially generates another unification problem where x and y are already identified. The problem remains if x or y are fresh variables, "ping-pong variables". In order to avoid it, we introduce Restriction 1(iii), where only the occurrences of fresh variables are restricted.

Restriction 2. (on Algorithm

A 2 ) Algorithm A 2 computes a finite complete set of 2-pure unifiers of 2-pure E 1 ∪ E 2 -unification problems.
We restrict A 2 to compute only 2-pure substitutions. This is used to avoid possible reapplications of A 1 after A 2 .

Restriction 3. (Errors

) (i) A Σ 1 Σ (1,2) -rooted term cannot be E 1 ∪ E 2 -equal to a Σ 2 -rooted term. (ii) E 1 ∪ E 2 is subterm collapse-free.
Note that in the next section we give a modularity result for subterm collapse-freeness. That is, we give a non-empty family of theories for which subterm collapse-freeness is a modular property.

The failure rules associated with Restriction 3 are given in Figure 1. It can be shown based on these restrictions that Algorithm C is a complete unification algorithm for the combined theory. More precisely, if A 1 and A 2 are algorithms satisfying Restrictions 1 through 3, then Algorithm C is sound and complete, which also means that E 1 ∪ E 2 -unification is finitary.

Conflict: If s(ǫ) ∈ Σ 1 Σ (1,

A Class of Hierarchically Combinable Theories

In this section we define a non-empty class of theories for which Restrictions 1 through 3 can be satisfied. We assume that E 1 and E 2 are subterm collapse-free. The class is then defined by the following additional properties.

Properties of E 1 :

R 1 is a left-linear, convergent term rewrite system corresponding to E 1 .

Properties of E 2 :

E 2 is a linear, finite equational theory.

Some of the steps below are non-deterministic, hence lead to computation paths. Throughout each path, the failure rules of Figure 1 are applied eagerly after each step. Let V = V ar(P).

Step 0: Variable Identification Guess a partition on V and set variables in each subset equal to each other. This requires adding fresh equations of type u = ? w, where u, w ∈ V and u and w belong to the same subset in the partition. Let us denote the enumeration of the partitions of V as π1, π2, . . . , πm. Once a partition is selected, the unification problem P is modified by adding the fresh equations between variables to the unification problem. We denote the modified problems by

P π i , 1 ≤ i ≤ m.
Step 1: Run A1 We apply A1 to the Σ1 Σ (1,2) -equations of P π i . If A1 fails for all πi, report failure and stop.

Otherwise, we now have a modified, by A1, set of unification problems from P π i , P π i 1 , . . . P π i n for n ≥ 1, such that all the Σ1 Σ (1,2) -equations in each P π i j , are in (Σ1 Σ (1,2) )-solved form.

Step 2: Run A2 Run Algorithm A2 on the 2-pure equations of each P π i j . If A2 equates variables in V not equated by πi j discard that particular P π i j . If none of the remaining P π i 1 , . . . P π i n exit with success, return failure. Otherwise, return success.

Properties of the shared symbols:

If

f ∈ Σ (1,2) , then f is an inner constructor of R 1 .
If f and g are inner constructors of R 1 , then f -rooted terms cannot be equated to g-rooted terms in E 2 . Here,

E AC = E 1 ∪ E 2 where E 1 = {(1), (2)
} and E 2 = {(3), (4)}.

Satisfying Restriction 1

The first and critical step to satisfying Restriction 1 is the construction of an inference system G such that the standard forms of leaves in the search tree generated by G are the Σ 1 Σ (1,2)solved forms corresponding to a complete set of E 1 ∪ E 2 -unifiers of the input problem, thus satisfying the majority of Restriction 1. In [START_REF] Erbatur | Hierarchical combination[END_REF], we modify the general syntactic E-unification procedure G [3], but we still have to identify interesting cases for which G can be turned into a terminating algorithm. For the particular case of E AC , an algorithm A 1 satisfying Restriction 1 can be constructed from scratch as in [START_REF] Erbatur | Unification over distributive exponentiation (sub)theories[END_REF].

Satisfying Restriction 2

Let t φ denote the standard 2-abstraction of t, which corresponds to the 2-pure term obtained from t by replacing alien subterms of t with fresh variables (E

Satisfying Restriction 3

Using the fact that E 2 is subterm collapse-free and the fact that if s ←→ E1∪E2 t then s φ = E2 t φ , it can be shown that a Σ 1 Σ (1,2) -rooted term cannot be E 1 ∪ E 2 -equal to a Σ 2 -rooted term. Lastly, it can be shown that for any term t and any strict subterm u of t, if t → + R1 t ′ , then t ′ = E2 u. This fact leads directly to the result that E 1 ∪ E 2 is subterm collapse-free.

As a final remark, it is important to note that our algorithm C does not work in a symmetric way with respect to E 1 and E 2 , contrary to combination algorithms where we assume that any (Σ 1 ∩ Σ 2 )-equality is valid in E 1 if and only if it is valid in E 2 [START_REF] Baader | Unification in the union of disjoint equational theories: Combining decision procedures[END_REF][START_REF] Domenjoud | Combination techniques for non-disjoint equational theories[END_REF][START_REF] Ringeissen | Unification in a combination of equational theories with shared constants and its application to primal algebras[END_REF]. Indeed, the algorithm A 1 partially solves the problem modulo E 1 ∪ E 2 (and not only modulo E 1 ). Then, A 2 is in charge of solving modulo E 2 the remaining part that was kept unsolved by A 1 . Our restrictions allow us to get all the solved forms without any further pingponging between A 2 and A 1 .

2 )Figure 1 :

 21 Figure 1: Failure rules

Figure 2 :

 2 Figure 2: C: Unification Algorithm for the combined theory E 1 ∪ E 2 .

Example 4 . 1 .

 41 The equational theory E AC considered in[START_REF] Erbatur | Unification over distributive exponentiation (sub)theories[END_REF] satisfies all the above properties. The axioms of E AC are as follows:exp(exp(x, y), z) = exp(x, y ⊛ z) (1) (x ⊛ y) ⊛ z = x ⊛ (y ⊛ z) (3)exp(x * y, z) = exp(x, z) * exp(y, z) (2) x ⊛ y = y ⊛ x (4)

  E1∪E2tσ, that sσ φ = E2 tσ φ . This implies that E 2 -unification is sound and complete for solving 2pure E 1 ∪ E 2 -unification problems. Hence, an E 2 -unification algorithm provides an algorithm A 2 satisfying Restriction 2 since it computes a complete set of 2-pure unifiers.

1 ∪ E 2 -equal alien subterms are replaced by the same fresh variable). It can be shown if s ←→ E1∪E2 t, then s φ = E2 t φ . Reasoning inductively it can further be shown for any 2-pure equation s = ? t where sσ =

* Supported by the Department of Computer Science of the University at Albany and then INRIA Nancy-Grand Est during a portion of this work. † Partially supported by the NSF grant CNS-0905222 ‡ Supported by an ASEE postdoctoral fellowship under contract to the NRL. § Partially supported by the NSF grant CNS-0905286