Florent Jacquemard
email: florent.jacquemard@inria.fr

Michael Rusinowitch

Laurent Vigneron
email: vigneron@loria.fr

Tree automata with equality constraints modulo equational theories

This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that this class has a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.

Introduction

Combining tree automata and term rewriting system (TRS) has been successful in domains like automated theorem proving [START_REF] Comon | Tree Automata Techniques and Applications[END_REF] and verification of infinite state systems e.g. [START_REF] Genet | Rewriting for Cryptographic Protocol Verification[END_REF][START_REF] Nielson | Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi[END_REF][START_REF] Küsters | Automata-Based Analysis of Recursive Cryptographic Protocols[END_REF].

A problem with such approaches is to extend the decidability results on tree automata languages to equivalence classes of terms modulo an equational theory. Some authors (e.g. [START_REF] Verma | Two-Way Equational Tree Automata[END_REF][START_REF] Ohsaki | Decidability and Closure Properties of Equational Tree Languages[END_REF]) have investigated the problem of emptiness decision for tree automata modulo specific equational theories, e.g. AC, ACU. . . Moreover, results about regularity preservation under rewriting have been established for several general classes of TRS during the last decades (see e.g. [START_REF] Seki | Layered Transducing Term Rewriting System and Its Recognizability Preserving Property[END_REF], Section 2.3 for a summary of some important results).

Another important difficulty stems from the non linear variables (variables with multiple occurrences) in the rewrite rules, which impose in general some over-approximations of the rewrite relation. Tree automata with constraints have been proposed earlier in order to deal with non-linear rewrite systems (see [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]). They are an extension of classical tree recognizers where syntactic equality and disequality tests between subterms are performed during the automata computations. The emptiness of the recognized language is undecidable without restriction, and two remarkable subclasses with decidable emptiness problem are the tree automata with equality and disequality constraints restricted to brother positions of [START_REF] Bogaert | Equality and Disequality Constraints on Direct Subterms in Tree Automata[END_REF] and the reduction automata of [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF]. This second class captures in particular languages of terms (ir)reducible by non linear rewrite systems.

Following [START_REF] Frühwirth | Logic programs as types for logic programs[END_REF], it is classical to represent tree automata by Horn clause sets. In this setting, a recognized language is defined as a least Herbrand model and it is possible to use classical first-order theorem proving techniques in order to establish decision results [START_REF] Verma | Two-Way Equational Tree Automata[END_REF][START_REF] Goubault-Larrecq | Deciding H1 by Resolution[END_REF].

In this paper, we follow this approach in order to unify the two problems mentioned above: we show how techniques of basic ordered paramodulation with selection and a variant of splitting without backtracking solve some decision problems on languages of tree automata with equality constraints, transformed by rewriting. More precisely, we show that the so called Generalized Membership Problem, GMP (whether there exists a ground instance of a given term in a given language) is decidable by saturation with a standard calculus presented in Section 3. Note that GMP generalizes the emptiness problem. Alternatively our results can be viewed as new decidable classes of first-order formula. Both classes of standard tree automata (TA) and tree automata with equality constraints generalizing those of [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF], where the equality tests are presented by arbitrary equations (TAD), are studied in these settings, as well as their respective generalisation modulo an equational theory E presented as a convergent term rewriting system (monadic TRS in the case of TA and restricted collapsing TRS in the case of TAD). The decision results are presented as follows in the paper:

E = ∅ E TA
Section 4 Section 6 TAD Section 5 Section 7

The last result (lower right corner of the table) is to our knowledge one of the first decision results (after [START_REF] Jacquemard | Unification in Extensions of Shallow Equational Theories[END_REF]) concerning tree automata with equality constraints modulo equational theories. We show that emptiness is undecidable for TA extended with non-linear facts, even with only one state. Unlike stated in [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF][START_REF] Comon | Tree Automata Techniques and Applications[END_REF], it appears also that this problem is undecidable for non-deterministic reduction automata (see Section 5). Therefore, we have introduced for the definition of TAD a refinement on the restriction for the automata of [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF] in order to make GMP decidable. The idea is roughly to bound the number of equality tests that can be performed along a whole computation (and not only along each computation path). The representation of constrained automata as Horn clauses permits us to use state of the art first-order theorem proving techniques to provide an effective (implementable) decision procedure for GMP (hence emptiness), instead of the complicated pumping lemmas used so far which hardly lead to effective algorithms. A key-ingredient for the termination of our saturation-based decision procedure was the application of recently proposed splitting rules.

As illustrated by two examples of authentication protocols (one with recursion) the class of automata of Section 7 permits a sharper modeling of verification problems (avoiding approximation as it is often required with more standard tree automata).

Related work.

A comparison with the reduction automata of [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF] is detailed in Sections 5 and 7.

The closely related works [START_REF] Nielson | Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi[END_REF][START_REF] Goubault-Larrecq | Deciding H1 by Resolution[END_REF] propose a different extension H 1 of standard TA defined as Horn clause sets for which satisfiability is decidable. In the version [START_REF] Goubault-Larrecq | Deciding H1 by Resolution[END_REF] of H 1 Horn clauses have a head whose argument is at most of height one and linear (without duplicated variables), or are purely negative (goals). None of the classes TAD and H 1 contains the other. However, H 1 becomes undecidable when allowing variable duplication in the heads. Our TAD class allows this under the previously mentioned restrictions.

Preliminaries

Term algebra. Let F be a signature of function symbols with arity, denoted by lowercase letters f , g. . . and let X be an infinite set of variables. The term algebra is denoted T (F , X ), and T (F ) for ground terms. A term is called linear if every variable occurs at most once in it and sublinear if all its strict subterms are linear. We note vars(t) the set of variables occurring in a term t ∈ T (F , X ). A substitution σ is a mapping from X to T (F , X ) such that {x|σ(x) = x}, the support of σ, is a finite set. The application of a substitution σ to a term t is denoted by tσ and is equal to the term t where all variables x have been replaced by the term σ(x). A substitution σ is grounding for t if tσ ∈ T (F ). The positions Pos(t) in a term t are represented as sequence of positive integers (Λ, the empty sequence, denotes the root position). A subterm of t at position p is denoted t| p , and the replacement in t of the subterm at position p by u denoted t[u] p .

Rewriting. We assume standard definitions and notations for TRS [START_REF] Dershowitz | Rewrite systems, chapter Handbook of Theoretical Computer Science[END_REF].

Clauses. Let P be a finite set of predicate symbols which contains an equality predicate =. The other predicate symbols are denoted by uppercase letter P , Q,. . . and are assumed unary. We shall use later a partition P \ {=} = P 0 P 1 . Let Q be a finite set of nullary predicate symbols disjoint from P and that we call splitting predicates, denoted by lowercase letters q. . . Constrained Horn clauses are constrained disjunctions of literals denoted Γ ⇒ H θ where Γ is a set of negative literals called antecedents, H is a positive literal called head of the clause and the constraint θ is a set of equations between terms of T (F , X ). A clause with a splitting literal as head or with no head at all is called a goal. The constraint is omitted when θ is empty. For sake of notation, we shall sometimes make no distinction between the constraint and its most general solution (when it exists). When θ is satisfiable, we call expansion of the above clause the unconstrained clause Γ θ ⇒ Hθ.

Atoms of the form P (s), resp. q, where P ∈ P and s ∈ T (F , X ), resp. q ∈ Q, are represented for uniformity as equations P (s) = true, resp. q = true, where true is a distinguished function symbol (in F ). An atom of the latter form is called non-equational and can be denoted simply P (s), resp. q. We assume in the following that predicate symbols can only occur at the root of the terms that we consider.

Orderings. We assume given a precedence ordering on F ∪P ∪Q, and denote ∼ the relation ∩ and the relation \ ∼. We assume that is total on P 1 and moreover that for all predicates P 0 , P 0 ∈ P 0 , P 1 ∈ P 1 , q ∈ Q and every function symbol f ∈ F, P 0 ∼ P 0 and P 1 P 0 q f . We assume the symbol true to be the minimal one. Assume that P 1 = {P 1 , . . . , P n } with P 1 . . . P n . We call i the index of P i , denoted ind (P i ), and let ind (Q) = 0 for all Q ∈ P 0 . We shall also use the constant ∞ = max(ind (P )|P ∈ P) + 1, which is bigger than the index of every predicate in P 1 .

We assume a a reduction ordering lpo [START_REF] Dershowitz | Rewrite systems, chapter Handbook of Theoretical Computer Science[END_REF] on T (F ∪ P ∪ Q, X ) total on ground terms, defined as a lexicographic path ordering. This ordering is extended to literals as in [START_REF] Bachmair | Basic Paramodulation[END_REF], see Appendix A for complete definitions.

Tree Automata. Tree automata are finite state recognizers of ground terms. We consider here a definition à la Frühwirth et al [START_REF] Frühwirth | Logic programs as types for logic programs[END_REF] of tree automata as finite sets of Horn clauses on P and F with equality. Every non-equational predicate symbol occurring in a given tree automaton A is called a state of A. Given a tree automaton A and a state Q ∈ P of A, the language of A in Q, denoted by

L(A, Q), is the set of terms t ∈ T (F ) such that Q(t) is a logical consequence of A.
General Membership Problem (GMP). We focus on one decision problem, GMP, which generalizes many important problems concerning tree automata (in particular membership and emptiness decision). This problem has been shown decidable in [START_REF] Tison | Tree automata and term rewrite systems[END_REF] for standard tree automata. INSTANCE: a tree automaton A, a state Q of A and a term t ∈ T (F , X ), QUESTION: is there a substitution σ grounding for t such that tσ ∈ L(A, Q)? In particular, when t is a ground term, this problem is equivalent to a membership problem for A: t ∈ L(A, Q)? When t is a variable, it is equivalent to a non-emptiness problem for A: L(A, Q) = ∅? Lemma 1. GMP is satisfied by A, Q and t iff A ∪ {Q(t) ⇒ } is inconsistent.

Basic Ordered Paramodulation with Selection

We shall establish the decidability of GMP for several classes of tree automata (with equations), using techniques of saturation under paramodulation, based on Lemma 1 and the calculus described in this section.

Basic Ordered Paramodulation with Selection. The following set of inference rules, parametrized by a reduction ordering , which we assume total on ground terms, and a function of selection of negative literals 1 , forms a sound and refutationally complete (i.e. for every unsatisfiable set of clauses the inference system will generate, with a fair strategy, the empty clause) calculus for Horn clauses called basic ordered paramodulation with selection [START_REF] Bachmair | Basic Paramodulation[END_REF][START_REF] Nieuwenhuis | Paramodulation-Based Theorem Proving, chapter Handbook of Automated Reasoning[END_REF].

Γ ⇒ = r θ Γ ⇒ u[ ] p = v θ RP Γ, Γ ⇒ u[x] p = v θ, θ , = , x = r if x is fresh,

and (i)

/ ∈ X , (ii) no literal is selected in Γ and Γ , (iii) and (v) hold.

Γ ⇒ = r θ Γ , u[ ] p = v ⇒ A θ LP Γ, Γ , u[x] p = v ⇒ A θ, θ , = , x = r if x is fresh, (i) / ∈ X , (ii) no literal is selected in Γ , (iii) holds, (iv) u = v is selected or (v') holds. Γ, s = t ⇒ A θ Eq Γ ⇒ A θ, s = t if (vi) s = t is selected or (vii) sσ ≺ tσ and sσ = tσ is maximal in Γ σ, sσ = tσ, Aσ, where σ is the mgu of θ, s = t.
The conditions missing above are: (i) / ∈ X , (iii) σ rσ and σ = rσ is strictly maximal in Γ σ, σ = rσ, (v) uσ = vσ is maximal in Γ σ, uσ = vσ, where σ is the most general unifier (mgu) of θ, θ , = , x = r, (v') uσ = vσ is maximal in Γ σ, uσ = vσ, Aσ (σ is as in (v)).

Concerning RP and LP, we shall talk of paramodulation of the first clause (called first premise) into the second clause (second premise). The clause returned by the above inferences is called conclusion. If after every step the constraints are eagerly propagated in the clauses (i.e. each clause is expanded) the calculus is called ordered paramodulation with selection.

Resolution. The application of LP into non-equational atoms followed by Eq is called basic resolution.

Γ ⇒ P ( ) = true θ Γ , P ( ) = true ⇒ A θ R Γ, Γ ⇒ A θ, θ , =
When the non-basic version of LP and Eq are used, this inference is simply called ordered resolution. Note that when the unconstrained part of a clause only contains variables (no function symbols), only the resolution rule applies into this clause, and the clause obtained also contains only variables (i.e. every application of LP is performed at the root position of an atom). Therefore, for the sake of presentation, we shall eagerly apply the constraint when describing the application of R in this case. The application of RP to clauses whose heads are non-equational returns a tautology, and hence this case will be ignored in the following proofs.

Deletion of redundant clauses. We assume that the deletion of tautologies and subsumed clauses (these notions are considered after clause expansion) and the simplification under rewriting by orientable positive equational clauses are applied as in [START_REF] Bachmair | Basic Paramodulation[END_REF].

Splitting. We shall use ε-splitting [START_REF] Goubault-Larrecq | Deciding H1 by Resolution[END_REF], a variant of splitting without backtracking [START_REF] Riazanov | Splitting Without Backtracking[END_REF].

B, Γ ⇒ H θ εsplit B ⇒ q B θ q B , Γ ⇒ H θ where the literals of Γ ∪H are not equational, Bθ is an ε-block, i.e. a set of literals of the form Q 1 (x), . . . , Q n (x), with Q 1 , . . . , Q n ∈ P, x is a variable which does not occur in Γ and H, and where q B ∈ Q is uniquely associated with B, modulo variable renaming.

Note that the above splitting rule replaces a clause by two split clauses. Using this rule eagerly (as soon as possible) preserves correctness and completeness of the calculus. Indeed, since every splitting predicate q B is smaller than any predicate of P, the original clause is redundant (wrt the general redundancy criterion of [START_REF] Bachmair | Basic Paramodulation[END_REF]) because its reduced instances are implied by smaller reduced instances of the split clauses. Another important point is that the number of splitting literals that can be introduced is bounded. We will assume that the set Q is large enough to cover all ε-blocks.

Standard Tree Automata

The transitions of standard tree automata are classically encoded into Horn clauses of the following form:

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q f (x 1 , . . . , x n ) (s)
where n ≥ 0 (when n = 0, by convention, the set of antecedents of the clause is empty), x 1 ,. . . ,x n are distinct variables and Q 1 , . . . , Q n , Q ∈ P 0 .

Definition 1. A standard bottom-up tree automaton (TA) is a finite set of clauses of type (s).

The language of a TA is called a regular language.

Example 1. The language of the following TA in Q 1 is the set of binary trees with inner nodes labelled by f and leaves labelled by 0 or 1, such that at least a leaf is labeled by 1:

⇒ Q 0 (0), ⇒ Q 1 (1), Q 0 (x 1 ), Q 0 (x 2 ) ⇒ Q 0 (f(x 1 , x 2 )), Q 1 (x 1 ), Q 0 (x 2 ) ⇒ Q 1 (f(x 1 , x 2 )), Q 0 (x 1 ), Q 1 (x 2 ) ⇒ Q 1 (f(x 1 , x 2 )), Q 1 (x 1 ), Q 1 (x 2 ) ⇒ Q 1 (f(x 1 , x 2 ))
The emptiness and membership problems for TA can be solved in deterministic time, respectively linear and quadratic. GMP for a linear term can be decided by a procedure of the same quadratic time complexity. For a non-linear term, the problem is EXPTIME-complete [START_REF] Devienne | Set-based analysis for logic programming and tree automata[END_REF]. We sketch below a slight variation of a DEXPTIME procedure of [START_REF] Goubault-Larrecq | Deciding H1 by Resolution[END_REF] in our framework, in order to introduce the principles of the proofs in the next sections. It is based on the function sel 1 which selects in a Horn clause Γ ⇒ H θ : every splitting negative literal, if any, and otherwise every non-equational literal Q(t) of Γ such that tθ is not a variable.

Proposition 1 ([13]). Ordered resolution with selection and ε-splitting saturates on the union of a TA and a goal clause P (t) ⇒.

Proof. (sketch, the complete proof may be found in Appendix B). We show that the saturation of a TA A and the goal P (t) ⇒ under ordered resolution wrt lpo and the selection function sel 1 , with eager application of the εsplit rule of Section 3, produce only clauses of one of the following form (gs), for goalsubterm, or (gf), for goal-flat. q 1 , . . . , q k , P 1 (s 1 ), . . . , P m (s m ) ⇒ [ q ]

( gs)

where m, k ≥ 0, s 1 , . . . , s m ∈ st(t), P 1 , . . . , P m ∈ P 0 , and q 1 , . . . , q k , q are splitting literals (the q in the head is optional, as indicated by the square brackets).

P 1 (y i1 ), . . . , P k (y i k ), P 1 (f (y 1 , . . . , y n )), . . . , P m (f (y 1 , . . . , y n )) ⇒ [ q ] (gf)
where k, m ≥ 0, i 1 , . . . , i k ≤ n, y 1 , . . . , y n are distinct variables, P 1 , . . . , P k , P 1 , . . . .P m ∈ P 0 , and q is a splitting literal (optional in the clause).

Since the number of clauses of type (gs) and (gf) is exponential, the saturation terminates and GMP is solvable in deterministic exponential time.

2

Corollary 1. GMP is decidable for TA.

Undecidable extension. Let us call fact a Horn clause ⇒ H with no antecedents at all. We define a clause to be of type (s + ) if it is of type (s) or a fact. Note that we allow non-linear variables in facts. We can show that GMP for this slight extension of TA is undecidable2 (even with one predicate only):

Proposition 2. GMP for sets of clauses of type (s + ) is undecidable.

Proof. We reduce in Appendix C the halting problem of 2 counter machines to GMP for (s + ).

Tree Automata with Syntactic Equational Constraints

Reduction Automata. The original reduction automata (RA) of [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF] can be defined as finite sets of constrained Horn clauses of the following form:

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q(f (x 1 , . . . , x n )) c (red)
where n > 0, x 1 ,. . . , x n are distinct variables, c is a conjunction of constraints of the form It appears that the emptiness problem is undecidable for non-deterministic reduction automata, contradicting a claim in [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF][START_REF] Comon | Tree Automata Techniques and Applications[END_REF]. Proposition 3. The emptiness problem is undecidable for non-deterministic RA.

x i | p = x i | p (equality constraint) or x i | p = x i | p (
The proof, a variation of the proof of Proposition 2, is given in Appendix D.

TAD. We propose here the definition of a new class of tree automata where the constraints are generalized (compared to [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF]) to equations between arbitrary terms and where the transitions comply to stronger ordering conditions, based on the ordering on states, in order to obtain a decidable GMP. We call below test predicates3 the elements of P 1 . The constrained transitions of our automata have the following form:

Q 1 (x 1 ), . . . , Q n (x n ), u 1 = v 1 , . . . , u k = v k ⇒ Q * (x) ( d)
where n, k ≥ 0, x 1 ,. . . , x n , x are distinct variables,

u 1 , v 1 , . . . , u k , v k ∈ T F , {x 1 , . . . , x n , x} , Q 1 , . . . , Q n , Q ∈ P, Q * is a test predicate, and for all i ≤ n, if Q i is a test predicate then Q * Q i .
The unconstrained transitions are restricted to clauses of type (s) which contain no more test predicates symbols in their antecedents than in their heads.

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q f (x 1 , . . . , x n ) (t)
where n > 0, x 1 ,. . . ,x n are distinct variables, and either Q 1 , . . . , Q n , Q ∈ P 0 or Q is a test predicate and at most one of Q 1 , . . . , Q n is equal to Q, and the others belong to P 0 .

Definition 2. A tree automaton with equational constraints or TAD is a finite set of clauses of type (t) or (d).

Note that every TA is a particular case of TAD (without test predicates).

Example 2. The language of the following TAD in state Q 2 is the set of stuttering lists of natural numbers build with the symbols cons and empty:

⇒ Q 0 (0) Q 0 (x 1 ) ⇒ Q 0 (s(x 1 )) ⇒ Q 1 (empty) Q 0 (x 1 ), Q 1 (x 2 ) ⇒ Q 1 (cons(x 1 , x 2 )) Q 0 (x 1 ), Q 2 (x 2 ) ⇒ Q 2 (cons(x 1 , x 2 )) Q 0 (x 1 ), Q 1 (x 2 ), x 2 = cons(x 1 , y), x = cons(x 1 , x 2 ) ⇒ Q 2 (x)
Proposition 4. Ordered paramodulation with selection and ε-splitting saturates on the union of a TAD and a goal clause P (t) ⇒.

Proof. (sketch) Let sel 2 be a selection function which generalizes sel 1 , by selecting every equational negative literals, if any, and otherwise is defined just like sel 1 . We consider saturation under ordered paramodulation wrt lpo with selection by sel 2 and ε-splitting.

The principle of the proof of termination (detailed in Appendix E) is to show that, starting with a TAD A and P (t) ⇒, every step of paramodulation returns either a clause smaller than all its premises (wrt to a well founded ordering ) or a clause of type (gf). Two key points ensure this result. First, because of the selection strategy, equations in clauses of type (d) will be eliminated first, using Eq, before these clauses can be involved in resolution. The type of clauses obtained (when all equations have been eliminated) is called (d + ) and their predicates satisfy the same ordering condition as for (d). Second, thanks to the ordering conditions on predicates for (t) and (d + ), the application of such clauses in resolution makes clauses decrease (wrt ).

Corollary 2. GMP is decidable for TAD.

Tree Automata Modulo Monadic Theories

There have been many works to identify some classes of rewrite systems preserving the regularity of sets of terms, like for instance ground TRS, right-linear monadic TRS, linear semi-monadic TRS. . . (see [START_REF] Seki | Layered Transducing Term Rewriting System and Its Recognizability Preserving Property[END_REF], Section 2.3 for a summary of some recent results). These results often rely on a procedure of completion of TA wrt some TRS, which adds new TA transitions without adding new states. As observed in [START_REF] Jacquemard | Unification in Extensions of Shallow Equational Theories[END_REF], such a TA completion can be simulated by saturation under paramodulation. The next results show that this method is effective (i.e. terminates) in the case of monadic theories. Definition 3. A rewrite rule → r is called sublinear if is sublinear, collapsing if r is either a ground term or a variable, and monadic if r is either a variable occurring in or a term g(z 1 , . . . , z k ) for some g ∈ F, k ≥ 0 and some distinct variables z 1 , . . . , z k occurring in .

Example 3. The following axiom for integer equality: eq(s(x), s(y)) → eq(x, y) as well as this rule for the elimination of stutterings in lists: cons(x, cons(x, y)) → cons(x, y) are monadic rewrite rules. Sublinear and collapsing rewrite rules permit to describe cryptographic functions [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], like decryption in a symmetric cryptosystem dec enc(x, y), y → x (the symbols enc and dec stand for encryption and decryption and the variables x and y correspond respectively to the encrypted plaintext and the encryption key), or, in the case of public (asymmetric) key cryptography: adec aenc(x, pub(y)), inv(pub(y)) → x and adec aenc(x, inv(pub(y))), pub(y) → x where inv is an idempotent operator, following the rule inv(inv(y)) → y, which associates to a public encryption key its corresponding private key (for decryption), and conversely. We will also consider below projections on pairs: fst(pair(x, y)) → x and snd(pair(x, y)) → y.

We call equational theory a set of positive clauses of the form:

⇒ = r (eq)
An equational theory E is called -convergent if for each clause of E, the equation = r is orientable by lpo , i.e. lpo r, and the rewrite system R = { → r ⇒ = r ∈ E and lpo r} is confluent. Moreover, the theory E is called sublinear (resp. collapsing, monadic) if all the rules of R are sublinear (resp. collapsing, monadic). Definition 4. A tree automaton modulo an equational theory (TAE) is the union of an equational theory and of a finite set of clauses of type (s).

Example 4. The language of the following simple TAE in state Q e is the set of expressions equivalent to non-negative even integers:

⇒ p(s(x)) = x ⇒ s(p(x)) = x ⇒ Q e (0) Q e (x) ⇒ Q o (s(x)) Q o (x) ⇒ Q e (s(x))
If, instead of the above equational theory for successor and predecessor we consider the following monadic equational theory for a partial substraction on natural numbers: s(x)s(y) = xy, x -0 = x, 0x = 0, the language is the set of ground terms that evaluate into non-negative even integers.

Proposition 5. Basic ordered paramodulation with selection and ε-splitting. saturates on the union of a TAE modulo a -convergent monadic equational theory and a goal clause P (t) ⇒.

Proof. We show the termination of saturation of A ∪ {P (t) ⇒} under basic ordered paramodulation wrt the ordering lpo and the selection function sel 1 and with eager ε-splitting.

The new situation here is that the right paramodulation RP can be applied to a clause of type (s), using an equation of the equational theory (i.e. of clause of A of type (eq)).

⇒ f ( 1 , . . . , n ) = r Q 1 (x 1 ), . . . , Q 1 (x n ) ⇒ Q f (x 1 , . . . , x n ) RP Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q(y) x 1 = 1 , . . . , x n = n , y = r
Also, LP with an equational clause (eq) is possible into the initial goal clause P (t) ⇒. We introduce in Appendix F a new clause type (l) to characterize the (expansions of) clauses obtained this way, and show by a case analysis that all the clauses obtained during the saturation are of type (l) or of a type (f) which generalizes (gf) (proof of Proposition 1), allowing a head of the form Q(r) where r is either a variable or a linear flat term g(x 1 , . . . , x n ).

Since the number of clauses of type (l) and (f) is finite, this proves that the saturation of A ∪ {P (t) ⇒} under basic ordered paramodulation terminates.

Note that the expanded form of the above clause

Q 1 ( 1 ), . . . , Q n ( n ) ⇒ Q(y)
is related to the push clauses of two-automata [START_REF] Verma | Two-Way Equational Tree Automata[END_REF] or selecting theories [START_REF] Truderung | Selecting theories and recursive protocols[END_REF]. We will come back to this remark in Example 7 showing how the approach for protocol verification of this last paper can be carry on by TADE. Corollary 3. GMP is decidable for TAE modulo a -convergent monadic equational theory.

Tree Automata with Equational Constraints Modulo a Theory

It is shown in [START_REF] Jacquemard | Unification in Extensions of Shallow Equational Theories[END_REF] that the class of languages of terms recognized by tree automata of [START_REF] Bogaert | Equality and Disequality Constraints on Direct Subterms in Tree Automata[END_REF], with equality constraints between brother positions is not closed under rewriting with shallow theories (rewrite systems whose left and right members of rules have depth 1). The reason is that these tree automata test syntactic equalities whereas we want to consider languages of terms modulo an equational theory. The problem is the same with the tree automata of [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF]. Our definition based on Horn clauses and our saturation method solve this problem by considering a class of tree automata which combines both equality constraints like TAD and equational theories like TAE. The tree automata defined this way test equality constraints modulo an equational theory and recognize languages of terms modulo the same theory.

Definition 5. A tree automaton with equational constraints modulo an equational theory (TADE) is the union of an equational theory and of a TAD.

We show in Appendix G that every reduction automaton with equality constraints only is equivalent to a TADE of the same size, as long as its transitions fulfill the restrictions on predicates introduced in the definition of (t) and (d) in order to make emptiness decidable.

Example 5. We illustrate in this example how TADE can be used to characterize the behaviour of security protocols running in an insecure environment, following a model with explicit destructors [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] specified with the rewrite rules of Example 3. More precisely, our representation is such that a state of the protocol is reachable (from an initial state) iff it is in the TADE language. The protocol of Denning & Sacco [START_REF] Denning | Timestamps in Key Distribution Protocols[END_REF] permits two agents A and B to exchange a new symmetric key using an asymmetric cryptosystem. The respective behaviour of the agents can be represented by the two following clauses of type (d) 4 :

Q 0j (x) ⇒ Q 1j (pair(A, aenc(aenc(K, inv(pub(A))), pub(B)))) j = 0, 1 Q i0 (x) ⇒ Q i1 (enc(S, adec(adec(snd(x), inv(pub(B))), pub(fst(x))))) i = 0, 1
The predicate Q ij represent the content of the a channel Q when agents A and B are in respective states i, j, which are either 0 (initial state) or 1 (final state). In the first clause, A initiates the protocol, sending B a freshly chosen symmetric key K for further secure communications (A, B, K, S are constant function symbols). This key is K signed, for authentication purpose, with the secret key inv(pub(A)) of A and encrypted with the public key pub(B) of B. Moreover, A appends its name at the beginning of the message. In the second clause, B answers with a secret value S encrypted with K, which has been extracted from the received message (using the destructor symbols and the rules of Example 3). Note that in this setting, equations in clauses (d) permit to model conditionals for the agents of protocols.

We add some clauses of type (t) and (d) in order to model the control of an attacker over the public communication channel Q, namely the ability to read / analyze and recompose (by application of any public function f, possibly a destructor symbol) / resend messages:

Q 00 (x 1 ), Q 00 (x 2 ) ⇒ Q 00 (f(x 1 , x 2 )) Q 00 (x 1 ), Q 01 (x 2 ) ⇒ Q 01 (f(x 1 , x 2 )) Q 00 (x 1 ), Q 10 (x 2 ) ⇒ Q 10 (f(x 1 , x 2 )) Q 00 (x 1 ), Q 11 (x 2 ) ⇒ Q 11 (f(x 1 , x 2
)) symmetric of the above clauses:

Q 01 (x 1 ), Q 00 (x 2 ) ⇒ Q 01 (f(x 1 , x 2 )) . . . Q 01 (x 1 ), Q 10 (x 2 ) ⇒ Q 11 (f(x 1 , x 2 )) Q 10 (x 1 ), Q 01 (x 2 ) ⇒ Q 11 (f(x 1 , x 2 ))
Note that in the above clauses we allow several combinations of the agent's states in the antecedents, but not every combination. The principle is that if A (resp. B) is in state 1 in the first antecedent, it must be in state 0 in the second one (and conversely), because we assume that each agent can run only once. This way, we ensure an exact representation (as ground terms) of the executions of an instance of the protocol, whereas many other Horn clauses or tree automata models are approximating. Note that these conditions fit well with the ordering restrictions on clauses of type (t) and (d). We also add some clauses (t) ensuring that some ground terms are initially known to the attacker, e.g. ⇒ Q 00 (A).

Proposition 6. Basic ordered paramodulation with selection and ε-splitting saturates on the union of a TADE modulo a -convergent sublinear and collapsing equational theory and a goal clause P (t) ⇒.

Proof. (sketch) We consider saturation under basic ordered paramodulation wrt the ordering lpo and the selection function sel 2 (defined in the proof of Proposition 4) and with eager ε-splitting. Following the same proof schema as for Proposition 4 (TAD) we show (in Appendix H) that, starting with a TADE A and P (t) ⇒, every step of paramodulation returns either a clause smaller than all its premises (wrt to a well founded ordering ) or a clause of type (gf) or (df), where this latter clause type is similar to (gf) and also contains only a finite number of clauses. The proof is nevertheless much more complicated than in the case of TAD (see Table 5). Indeed, like for TAD (Proposition 4), we obtain clauses of type (d + ) generalizing (d), in this case using basic narrowing. However, these clauses (d + ) can be combined, by resolution, with clauses of a type similar to (l) in Proposition 5. Clause decreasing, wrt , is obtained for such resolution steps thanks to the restrictions on the equational theory considered.

Corollary 4. GMP is decidable for TADE modulo a -convergent sublinear and collapsing equational theory. Example 6. Several security properties of the Denning & Sacco's protocol may be expressed as GMP wrt the TADE of Example 5: Q 01 (x) ⇒ expresses for instance that B has answered to a message not originating from A (authentication flaw) and Q 01 (S) ⇒ that the secret is revealed (confidentiality flaw). Both instances of GMP can be solved with the method of Proposition 6, revealing a known attack involving only the agent B (and an attacker), and reveals the secret S. Assume that the attacker initially knows A, pub(A), pub(B). This situation can be modeled using clauses of type (t), as explained in Example 5. With the attacker clauses of Example 5, the attacker is able to construct and send the message m 0 = pair(A, aenc(A, pub(B))) on the public channel Q, because this term is made of terms of its initial knowledge and public function symbols pair and aenc. It means that m 0 ∈ L(A, Q 00 ). When the agent B reads m 0 , he replies (in channel Q) with enc(S, adec(adec(snd(m 0 ), inv(pub(B))), pub(fst(m 0 )))). Using the rewrite rules for projection (Example 3), this term is reduced to enc(S, adec(adec(aenc(A, pub(B)), inv(pub(B))), pub(A))) and with one of the rewrite rules for asymmetric decryption, applied to the underline redex, this term is further reduced to m 1 = enc(S, adec(A, pub(A))). It means that m 1 ∈ L(A, Q 01 ). The attacker is then able to construct the "key" adec(A, pub(A)), which belongs to L(A, Q 00 ), and can recover S by decryption. Indeed, thanks to the clause Q 01 (x 1 ), Q 00 (x 2 ) ⇒ Q 01 (dec(x 1 , x 2 )), we have S ∈ L(A, Q 01 ). It means that the secret S is revealed on the channel Q.

The protocol can be patched in order to avoid such an attack, by requiring A to send the names A and B along with the symmetric key K (j = 0, 1):

Q 0j (x) ⇒ Q 1j (pair(A, aenc(aenc(pair(pair(A, B), K), inv(pub(A))), pub(B))))
and by requiring the agent B to make some preliminary verifications on the message received before sending his answer, namely that the names match. This latter feature can be modeled in TAD by adding equations in the clause of type (d) representing B (with i = 0, 1 and t = adec(adec(snd(x), inv(pub(B))), pub(fst(x)))):

Q i0 (x), snd(fst(t)) = x B , fst(fst(t)) = fst(x), ⇒ Q i1 (enc(S, snd(t)))
Example 7. The recursive authentication protocol [START_REF] Bull | The authentication protocol[END_REF] ensures the distribution of certified session keys to a group of clients by a server which process recursively an unbounded list of requests. The automated verification of such group protocols has been studied in [START_REF] Küsters | Automata-Based Analysis of Recursive Cryptographic Protocols[END_REF][START_REF] Truderung | Selecting theories and recursive protocols[END_REF]. We shall follow below the presentation of [START_REF] Küsters | Automata-Based Analysis of Recursive Cryptographic Protocols[END_REF], showing that it fits in our formalism. The server receives a sequence of requests for keys represented by a term of the form nil or 5 : hash(m(a), a, b, n a , y), a, b, n a , y , denoted below by h ma (a, b, n a , y), where hash is a unary one-way function, a is the name of the principal requesting a certificate, b is the name of the principal with whom a is willing to share a key, n a is a random number generated by a (nonce), m(a) is a mac key shared by the server and a and y is a subsequence of the other requests, which (if not nil) has the form h mc (c, a, n c , y ) (c is the name of another principal). The behaviour of the server, when receiving a request sequence, is defined by the following clauses of type (d) ) (a, b, c, n a , n c are variables):

Q 0 (x), x = h ma (a, b, n a , nil) ⇒ Q 1 aenc(pub(a), k(a, b, n a ), b, n a ) Q 0 (x), x = h ma (a, b, n a , h mc (c, a, n c , y )) ⇒ Q 1 aenc(pub(a), k(a, b, n a ), b, n a ) Q 1 aenc(pub(a), k(c, a, n c ), c, n a )
It means that the server sends to a one or two certificates encrypted with his public key, where k is a secret function used for the generation of session keys. Note the two occurrences of a in the equation of the second clause, which implicitly express an equality between the name of the requester of a query and the receiver in the next one. It is assumed that for the first element of the sequence, the receiver is actually the server himself (hence it is not necessary to send him a certificate). Moreover, we have a clause of type (t) for the enumeration of the requests by the server:

Q 0 (x) ⇒ Q 0 (next(x))
, where next is an operator which pops the first element of a request's sequence, defined by the following collapsing equation (m is a variable): next(hash(m, x 1 , x 2 , x 3 , y), x 1 , x 2 , x 3 , y ) = y.

Conclusion and further works

We have introduced new classes of tree automata with constraints and shown that the General Membership Problem is decidable for them with a uniform theorem-proving technique. Potential extensions are numerous.

As future work we think to extend the tree automata classes defined in this paper to disequality tests as in [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF]. This would permit us to characterize languages of normal form wrt a TRS and is useful in particular in inductive theorem proving [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]. Such an extension is not trivial. In particular, it is not possible to simply add the disequations as positive (equational) literals to the clauses defined above. This would lead us out of the expected semantics. Some ad-hoc axiomatization of the disequality, according to the equational theory, is necessary. Other tests, for instance ordering tests, could also be investigated.

Equality tests between brother positions à la [START_REF] Bogaert | Equality and Disequality Constraints on Direct Subterms in Tree Automata[END_REF] can be easily incorporated into the Horn clauses representation of tree automata (see e.g. [START_REF] Jacquemard | Unification in Extensions of Shallow Equational Theories[END_REF]). Equations are not necessary for this purpose, since multiple occurrences of a variable suffice, as in:

Q 1 (x), Q 2 (x) ⇒ Q f (x, x)
. The combination of TA classes of [START_REF] Bogaert | Equality and Disequality Constraints on Direct Subterms in Tree Automata[END_REF] and [START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF] preserves emptiness decidability [START_REF] Caron | Pumping, Cleaning and Symbolic Constraints Solving[END_REF]. Hence the combination of the above class of TA with equality test modulo and unrestricted test between brother positions is interesting to study.

It would also be interesting to extend the above saturation results (in particular for classes modulo monadic or collapsing theories) to term algebra modulo AC, using AC-paramodulation techniques. This combination (AC + sublinearcollapsing) permits to axiomatize primitives like the exclusive-or. clause). Let us consider the particular subtype (sp) of (gf) of positive clauses with a splitting literal as head (i.e. (gf) with k = m = 0):

⇒ [q] ( sp)
where q ∈ Q (note that this type contains the empty clause).

The initial goal P (t) ⇒ belongs to the type (gs) and also belongs to (gf) if t is a variable.

The different cases of resolution steps between clauses of type (s), (gs) and (gf) are now listed below: R( , s): no resolution step is possible into a clause of type (s) because of the maximality condition (v) in LP. Indeed, no literal is selected by sel 1 in any clause of the form

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q f (x 1 , . . . , x n ) and, for all i ≤ n, we have Q f (x 1 , . . . , x n ) lpo Q i (x i ). Hence, for all substitution σ, Q i (x i σ) cannot be maximal among Q 1 (x 1 σ),. . . , Q n (x n σ), Q f (x 1 , . . . , x n )σ .
R(s, gs) returns a clause of type (gs) when one non-splitting negative literal P 1 (s 1 ) in the premise (gs) is selected by sel 1 , i.e. when s 1 = f (s 1 , . . . , s n ) (note that in this case the premise does not contain splitting literals by definition of sel 1 ):

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x 1 , . . . , x n ) P 1 (s 1 ), . . . , P m (s m ) ⇒ [ q ] R Q 1 (s 1 ), . . . , Q n (s n ), P 2 (s 2 ), . . . , P m (s m ) ⇒ [ q ]
R(s, gs) returns a clause of type (gf) when no negative literal is selected by sel 1 in the premise (gs). Note that in this case, this premise contains only one variable, otherwise it would be split. The tuple x 1 , . . . , x n is denoted x below:

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x 1 , . . . , x n ) P 1 (y), . . . , P k (y) ⇒ [ q ] R Q 1 (x 1 ), . . . , Q n (x n ), P 2 (f (x)), . . . , P k (f (x)) ⇒ [ q ]
R(s, gf) returns a clause of type (gf) when one non-splitting negative literal at least is selected by sel 1 in the premise (gf) -the tuple y 1 , . . . , y n is denoted y:

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x 1 , . . . , x n ) P 1 (y i1 ), . . . , P k (y i k ), P 1 (f (y)), . . . , P m (f (y)) ⇒ [ q ] R P 1 (y i1 ), . . . , P k (y i k ), Q 1 (y 1 ), . . . , Q n (y n ), P 2 (f (y)), . . . , P m (f (y)) ⇒ [ q ]
R(s, gf) returns a clause of type (gf) when no negative literal is selected by sel 1 in the premise (gf). This case in embedded R(s, gs) when the second premise has type (gs) and no selected literals, which has been treated above. R(sp, gs) returns a clause of type (gs).

⇒ q 1 q 1 , . . . , q k , P 1 (s 1 ), . . . , P n (m m ) ⇒ [ q ] R q 2 , . . . , q k , P 1 (s 1 ), . . . , P m (s m ) ⇒ [ q ] Note that this is the only case where a clause of type (gs) or (gf) can be involved as first premise in a resolution step.

Since the number of clauses of type (gs) and (gf) is exponential, the saturation terminates and GMP is solvable in deterministic exponential time.

2

Appendix C Proof of Proposition 2 (undecidability)

We reduce the halting problem of 2 counter machines to GMP for (s + ). Let us consider a deterministic 2-counter machine such that q 0 is the initial state and q f the final one (from where no transition is possible). A configuration of the machine can be represented by a term q(s n (0), s m (0)) where q is the state, and n (resp. m) the value of the first (resp. second) counter. We encode every transition q(s, t) → q (s , t ) of the machine by a fact. We will need a predicate symbol Q, binary functions g, h, k and a constant symbol c:

MACHINE INSTRUCTION CLAUSAL REPRESENTATION

q : ADD 1 TO COUNTER 1; GOTO q ⇒ Q(g(q(x, y), h(g(q (s(x), y), u), u))) q : IF COUNTER 1 = 0 DEC 1; GOTO q ⇒ Q(g(q(s(x), y), h(g(q (x, y), u), u))) q : IF COUNTER 1 = 0; GOTO q ⇒ Q(g(q(0, y), h(g(q (0, y), u), u)))

See also Figure 1 for a representation of these three examples. We add two facts to detect the halting state: ⇒ Q(g(q f (x, y), c)) and ⇒ Q(c). We introduce two auxiliary (s) clauses:

Q(x 1 ), Q(x 2 ) ⇒ Q(h(x 1 , x 2 )) (h) Q(x 1 ), Q(x 2 ) ⇒ Q(k(x 1 , x 2 )) (k)
and finally we introduce a goal clause: Q(k(y, g(q 0 (0, 0), y))) ⇒. We shall employ a resolution strategy with selection function sel 1 . A first resolution step of (k) into the initial goal clause generates: Q(y), Q(g(q 0 (0, 0), y)) ⇒. Then a resolution with a fact encoding a transition q 0 (0, 0) → st, for some term st, generates: Q(h(g(st, u), u)) ⇒, which is resolved by (h) to produce Q(u), Q(g(st, u)) ⇒. This process can be iterated. The halting state can be reached iff some goal clause is derived that can be resolved with ⇒ Q(g(q f (x, y), c)), producing Q(c) ⇒ which in turn generates the empty clause with ⇒ Q(c). Hence the set of clauses encoding the machine is unsatisfiable iff the machine halts.

Appendix D Proof of Proposition 3 (RA)

As in the proof of Proposition 2, we reduce the halting problem of a 2-counter machine M. We consider the same representation of the configurations of M as in Proposition 2, using in particular the same signature. The respective initial and final states of M are q 0 and q f . We construct below a non-deterministic reduction automaton A with states Q 0 (for 0) and Q 1 (for strictly positive integers), a universal state Q ∀ , some states Q c , Q d , Q gd , Q hd , and T for every transition T : c → d of M, a state Q for chaining the transitions of M and a final state Q f . This reduction automaton A is such that the language L(A, Q f ) is the set of the term representations of halting computations of M, starting with the configuration q 0 (0, 0) and ending with q f (i 1 , i 2 ) for some i 1 and i 2 .

We have in A two states Q 0 (for 0) and Q 1 (for strictly positive integers), with the transitions:

⇒ Q 0 (0), Q 0 (x) ⇒ Q 1 (s(x)), Q 1 (x) ⇒ Q 1 (s(x)). Below, Q N is an abbreviation for either Q 0 or Q 1 .
The transition T 1 = c 1 → d 1 of M, with c 1 = q(x, y), d 1 = q (s(x), y) (it corresponds to the machine instruction q: ADD 1 TO COUNTER 1; GOTO q ) is represented by the term g(q(x, y), h(g(q (s(x), y), u), u)) where u is the rest of the computation (the term is displayed in Figure 1 for sake of readability). We -

Q N (x 1 ), Q N (x 2 ) ⇒ Q c1 (q(x 1 , x 2 )) and Q 1 (x 1 ), Q N (x 2 ) ⇒ Q d1 (q (x 1 , x 2 ))
where the states Q c1 Q d1 are respectively associated to the left and right members of the transition,

-Q d1 (x 1 ), Q ∀ (x 2 ) ⇒ Q gd1 (g(x 1 , x 2 )), -Q ∀ is a "universal" state, ⇒ Q ∀ (0), Q ∀ (x) ⇒ Q ∀ (s(x)), Q ∀ (x 1 ), Q ∀ (x 2 ) ⇒ Q ∀ (f (x 1 , x 2
)) for every binary function symbol f among g, h, k or any state

q of M. -Q gd1 (x 1 ), Q ∀ (x 2 ) ⇒ Q hd1 (h(x 1 , x 2 )),
and this last clause which permits to accept the term T 1 in Figure 1 into a state also called T 1 (i.e. in L(A, T 1 )), and performs equality tests:

Q c1 (x 1 ), Q hd1 (x 2 ) ⇒ T 1 (g(x 1 , x 2 )) x 1 | 1 = x 2 | 1111 , x 1 | 2 = x 2 | 112 , x 2 | 2 = x 2 | 12
The transition T 2 = c 2 → d 2 of M, with c 2 = q(s(x), y), d 2 = q (x, y) (it corresponds to the machine instruction q: IF COUNTER 1 = 0 DEC 1; GOTO q ) is represented by the term g(q(s(x), y), h(g(q (x, y), u), u)) (see Figure 1). We use the following states and clauses for the recognition of this term T 2 :

-Q 1 (x 1 ), Q N (x 2 ) ⇒ Q c2 (q(x 1 , x 2 )) and Q N (x 1 ), Q N (x 2 ) ⇒ Q d2 (q (x 1 , x 2 )), -Q d2 (x 1 ), Q ∀ (x 2 ) ⇒ Q gd2 (g(x 1 , x 2 )), Q gd2 (x 1 ), Q ∀ (x 2 ) ⇒ Q hd2 (h(x 1 , x 2 )),
and the last clause (for the recognition of the term T 2 , Figure 1) which performs equality tests:

Q c2 (x 1 ), Q hd2 (x 2 ) ⇒ T 2 (g(x 1 , x 2 )) x 1 | 11 = x 2 | 111 , x 1 | 2 = x 2 | 112 , x 2 | 2 = x 2 | 12
The transition T 3 = c 3 → d 3 of M, with c 3 = q(0, y), d 3 = q (0, y) (it corresponds to the machine instruction q: IF COUNTER 1 = 0; GOTO q ) is represented by the term g(q(0, y), h(g(q (0, y), u), u)) (see Figure 1). We use the following states and clauses for the recognition of this term T 3 :

-Q 0 (x 1 ), Q N (x 2 ) ⇒ Q c3 (q(x 1 , x 2 )) and Q 0 (x 1 ), Q N (x 2 ) ⇒ Q d3 (q (x 1 , x 2 )), -Q d3 (x 1 ), Q ∀ (x 2 ) ⇒ Q gd3 (g(x 1 , x 2 )), Q gd3 (x 1 ), Q ∀ (x 2 ) ⇒ Q hd3 (h(x 1 , x 2 )),
and the last clause (for the recognition of the term T 3 , Figure 1) which performs equality tests:

Q c3 (x 1 ), Q hd3 (x 2 ) ⇒ T 3 (g(x 1 , x 2 )) x 1 | 2 = x 2 | 112 , x 2 | 2 = x 2 | 12
To model the chaining of transitions, we use a a new state Q and, for each transition T of M and associated state T we introduce the following unconstrained clauses (recall that T is the state symbol associated to the transition as above):

T (x 1 ), Q(x 2 ) ⇒ Q(h(x 1 , x 2 ))
We have a special constrained clause, associated to the unique transition T 0 of M starting from the initial configuration c 0 = q 0 (0, 0), (M is assumed deterministic). Note that in this clause we have a symbol k in the head, instead of a h:

T 0 (x 1 ), Q(x 2 ) ⇒ Q f (k(x 1 , x 2 )) x 1 | 2 = x 2
Finally, we consider three unconstrained clauses to initiate the bottom-up computation of the automaton with a final configuration q f (i 1 , i 2 ) of M. We assume wlog that the state q f can not be reentered by M. These clauses aim at accepting the term h(g(q f (i 1 , i 2 ), c), c) in the language L(A, Q):

⇒ Q c (c), Q N (x 1 ), Q N (x 2 ) ⇒ Q c f (q f (x 1 , x 2 )), Q c f (x 1 ), Q c (x 2 ) ⇒ Q gc f (g(x 1 , x 2 )), Q gc f (x 1 ), Q c (x 2 ) ⇒ Q(h(x 1 , x 2 ))
A example of computation of A is described in Figure 2. In this figure, the nodes of a recognized term are decorated with the states of A in which they are accepted. Note that equality test are performed by A only at nodes labelled with the symbol g.

We can show that M halts on q f (i 1 , i 2 ) starting from q 0 (0, 0

) iff L(A, Q f ) = ∅.
For the only if direction, we associate to a halting computation of M a tree of L(A, Q f ) as in Figure 2.

For the if direction, we use the following fact:

k Q f g T0 c0 Qc 0 y1 Q hc 1 y1 = h Q g T1 c1 Qc 1 y2 Q hc 2 y2 = h Q g T2 c2 Qc 2 y3 Q hc 3 y3 = h Q h Q g q f 0 0 c c Fig. 2. A computation of A Fact 1 If i. t ∈ L(A, Q) and t = h(t 1 , t 2 ) or t = k(t 1 , t 2 ), ii. t 1 ∈ L(A, T )
for some transition T , and iii. t 1 | 2 = t 2 , then either the state of the right-hand side of T is q f and t 2 = h(g(q f (0, 0), c), c), or, i'.

t 2 = h(t 1 , t 2 ) ∈ L(A, Q), ii'. t 1 ∈ L(A, T
) for a transition T , and iii'.

t 1 | 2 = t 2 .
Moreover, in this last case, the term t 1 | 1 is rewritten to t 1 | 1 by T (seen as a rewrite rule).

Now, observe that by construction of

A, if t ∈ L(A, Q f ) then t = k(t 1 , t 2
) and t 1 = g(q 0 (0, 0), t 2 ) and t 2 = L(A, Q). Hence, every term t ∈ L(A, Q f ) satisfies the hypotheses i., ii., iii. of Fact 1, and with this fact, this ensures that t represents a halting computation of M.

where k, n ≥ 0, q 1 , . . . ,

q k ∈ Q, Q 1 , . . . , Q n , Q * ∈ P, s 1 , . . . , s n , s ∈ T (F , X ), Q * is a test predicate, and for all i ≤ n, if Q i is a test predicate then Q * Q i .
It order to analyse the type of clauses obtained by resolution, we shall consider the clause types (gf) and (sp) defined in the proof of Proposition 1, and the type (g + ) of arbitrary goals:

q 1 , . . . , q k , P 1 (s 1 ), . . . , P m (s m ) ⇒ [ q ] ( g + )
where k, m ≥ 0, P 1 , . . . , P m ∈ P, q 1 , . . . , q k , q ∈ Q and s 1 , . . . , s m ∈ T (F , X ). The head is optional in the clause, as indicated by the brackets, and can only be a splitting literal (hence we abusively call such a clause a goal). Note also that the initial goal P (t) ⇒ has type (g + ). The measure of a clause C = Γ, Ξ ⇒ H θ , where Γ is a multiset of non-equational atoms and Ξ is a multiset of equations, is the tuple made of the following components: The strict ordering on measures, extended as expected to clauses, is defined as the lexicographic extension >, >, mul , mul lpo lex , where > denotes the ordering on natural numbers. The following Fact is proved by a case analysis summarized in Figure 3 and detailed below.

-m 1 (C) = ind (Q) (see page 4 for the definition of ind ) if H = Q(t) with Q ∈ P, or m 1 (C) = ∞ if C has type (sp), m 1 (C) = 0 if C is
Fact 2 Starting with A ∪ {P (t) ⇒}, every step of ordered paramodulation with selection by sel 2 and ε-splitting returns either a clause smaller than all its premises (wrt ) or a clause of type (gf).

Fact 2 permits us show that ordered paramodulation with selection and εsplitting saturates A and the goal, hence to conclude the proof of the proposition. Indeed, the number of clauses of type (gf) is finite up to variable renaming, hence an infinite deduction path would contain an infinite decreasing chain, wrt , whereas this order is well-founded.

We detail below the proof Fact 2 by a case analysis of all the instances of Eq, LP (R) and εsplit involving as premises some clauses of type (t), (d), (d + ), (gf), (sp) or (g + ). We show that for each case, the conclusion of each such an instance is either of type (gf) (or (sp)) or either is smaller than all its premises wrt .

Eq(d): equality resolution (Eq) is possible with the equations in clauses of type (d) (each of these equations is selected by sel 2 ) and every such application of (Eq) makes m 2 decrease. Recall that we defined (d + ) at page 22 as the type of clauses obtained from clauses (d) and which contain no more equations.

inf. 1 st 2 nd cl 1 st premise 2 nd premise pr. pr. m1 m2 m4 m6 m1 m2 m4 m6

Eq d d/d+ = > R t R d+ R t g + (1) g + > = = ≥ > R t g + (2) gf R t g + sp R t gf gf R d+ g + g + > = = > R d+ g + sp R
sp d+ (3)

d+ > = = = > R sp g + (3) g + > = = = > R sp g + (3) sp εsplit d+ gf εsplit d+ d+ = = ≥ > εsplit g + gf εsplit g + g + = = ≥ >
(1) no negative splitting literals and at least one literal selected (2) no literal selected

(3) at least one negative splitting literal (selected) Fig. 3. Case analysis in the proof of Proposition 4. > (resp. ≥, =) means that the measure's component for the premise is strictly greater than (resp. greater or equal to, equal to) the conclusion.

R( , t): no resolution step is possible into a clause of type (t) because of the maximality condition (v) in LP. Indeed, for any clause of the form

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q f (x 1 , . . . , x n ) no negative literal is selected by sel 2 and, for all i ≤ n, Q f (x 1 , . . . , x n ) lpo Q i (x i
) by definition of lpo and (t). R( , d + ): no resolution step is neither possible into a clause of type (d + ) for the same reason as above. R( , d): with the definition of the selection function sel 2 , a clause of type (d) and not of type (d + ) has selected equations (which are the only selected literals). Therefore, no inference other than equality resolution (Eq) (in particular no resolution) is possible into such a clause. R(d, ): because of the definition of sel 2 also, no resolution of a clause containing an equation into another clause is possible. R(t, g + ) returns a clause of type (sp) or a clause of type (g + ) smaller than both premises when the premise (g + ) has no negative splitting literal and one negative literal P 1 (s 1 ) selected by sel 2 , i.e. when s 1 = f (s 1 , . . . , s n ). If n > 0 or the premise (g + ) has strictly more than one antecedent we obtain a clause (g + ) (the tuple x 1 , . . . , x n is denoted x below):

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (s 1 ), . . . , P m (s m ) ⇒ [ q ] R Q 1 (s 1 ), . . . , Q n (s n ), P 2 (s 2 ), . . . , P m (s m ) ⇒ [ q ]
Note that in this case, by definition of (t), the measure m 4 for the conclusion is at most equal to m 4 for the premise (g + ).

If n = 0 (f is a constant function symbol) and m = 1, we obtain a clause (sp):

⇒ P 1 (f ) P 1 (s 1 ) ⇒ [ q ] R ⇒ [ q ]
R(t, g + ) returns a clause of type (gf) when no literal is selected by sel 2 in the premise (g + ) (note that it implies that (g + ) has no negative splitting literal).

In this case, because of the eager application of ε-splitting, the premise (g + ) contains only one variable x.

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (x), . . . , P m (x) ⇒ [ q ] R Q 1 (x 1 ), . . . , Q n (x n ), P 1 (f (x)), . . . , P m (f (x)) ⇒ [ q ]
R(t, gf) returns a clause of type (gf) when the premise of type (gf) has at least one literal selected (the tuples of variables x 0 , . . . , x n and y 1 , . . . , y n are respectively denoted x and y below):

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (y i1 ), . . . , P k (y i k ), P 1 f (y) , . . . , P m f (y) ⇒ [ q ] R P 1 (y i1 ), . . . , P k (y i k ), Q 1 (y 1 ), . . . , Q n (y n ), P 2 f (y) , . . . , P m f (y) ⇒ [ q ]
The cases where no literal is selected by sel 2 in the premise of type (gf) is included in the case R(t, g + ), with (g + ) unselected, treated above. R(d + , g + ) returns a clause of type (sp) or a clause of type (g + ) smaller than both premises:

Q 1 (s 1 ), . . . , Q n (s n ) ⇒ P 1 (s) P 1 (t 1 ), . . . , P m (t m ) ⇒ [ q ] R Q 1 (s 1 θ), . . . , Q n (s n θ), P 2 (t 2 θ), . . . , P m (t m θ) ⇒ [ q ]
where θ = mgu(s, t 1 ). When n = 0 and m = 1, we obtain a clause of type (sp) or the empty clause. R(d + , gf) returns a clause of type (sp) or (g + ) smaller than both premises: this case is included in the above case R(d + , g + ). R(sp, d + ) returns a clause of type (d + ) smaller than both premises.

⇒ q 1 q 1 , . . . , q k , Q 1 (s 1 ), . . . , Q n (s n ) ⇒ Q(s) R q 2 , . . . , q k , Q 1 (s 1 ), . . . , Q n (s n ) ⇒ Q(s)
R(sp, g + ) returns either a clause of type (sp) or a clause of type (g + ) smaller than both premises.

⇒ q 1 q 1 , [ q 2 , . . . , q k , P 1 (s 1 ), . . . , P m (s m ) ] ⇒ [ q ] R [ q 2 , . . . , q k , P 1 (s 1 ), . . . , P m (s m ) ] ⇒ [ q ]
Note that the conclusion, when not of type (sp), is indeed smaller than the premise (sp) because m 1 (sp) = ∞. εsplit(t) is not possible by definition. εsplit(d + ): such a step pf ε-splitting replaces a clause of type (d + ) by a clause of type (gf) and a clause of type (d + ) smaller than the premise (B is an ε-block):

q 1 , . . . , q k , B, Q 1 (s 1 ), . . . , Q n (s n ) ⇒ Q(s) εsplit B ⇒ q B q 1 , . . . , q k , q B , Q 1 (s 1 ), . . . , Q n (s n ) ⇒ Q(s)
εsplit(g + ): this ε-splitting replaces a clause of type (g + ) by a clause of type (gf) and a clause of type (g + ) smaller than the premise (B is an ε-block): q 1 , . . . , q k , B, P 1 (s 1 ), . . . , P m (s m ) ⇒ [ q ] εsplit B ⇒ q B q 1 , . . . , q k , q B , P 1 (s 1 ), . . . , P m (s m )

⇒ [ q ] 2 Appendix F Proof of Proposition 5 (TAE)
We assume given a TAE A modulo a -convergent monadic equational theory (presented by a convergent TRS R) and a a goal clause P (t) ⇒. We may assume wlog that P ∈ P 0 (otherwise the problem is trivial). Let us show the termination of saturation of A ∪ {P (t) ⇒} under basic ordered paramodulation wrt the ordering lpo and the selection function sel 1 defined in the proof of Proposition 1 and with eager ε-splitting.

The main difference with the situation of Proposition 1 is that some rule of the equational theory (i.e. a clause of type (eq)) may be applied to a clause of type (s) by right paramodulation RP.

⇒ f ( 1 , . . . , n ) = r Q 1 (x 1 ), . . . , Q 1 (x n ) ⇒ Q f (x 1 , . . . , x n ) RP Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q(y) x 1 = 1 , . . . , x n = n , y = r
Also, LP with an equational clause (eq) is possible into the initial goal clause P (t) ⇒.

We introduce below a new clause type (l) to characterize the (expansions of) clauses obtained this way, and show by a case analysis that all the clauses obtained during the saturation are of type (l) or of a type (f) which generalizes (gf) (proof of Proposition 1).

Let S be the smallest set of goal clauses containing the initial goal P (t) ⇒ and closed by application of basic left-paramodulation with an equational clause (eq) of A, i.e.:

⇒ = r P(s[ ] p ) ⇒ θ ∈ S LP P (s[x] p ) ⇒ θ, = , x = r ∈ S
The set S is finite (of cardinal linear in the size of t and A) because every application of basic left-paramodulation strictly decreases the number of function symbols in the unconstrained part of the goal clause.

The clause type (l) is defined as follows:

q 1 , . . . , q k , Q 1 (s 1 ), . . . , Q n (s n ) ⇒ [ H ] ( l)
where k, n ≥ 0, for every i ≤ n, either s i is a subterm of a left hand side of a rule of R, or Q i (s i ) ∈ S, q 1 , . . . , q k ∈ Q, Q 1 , . . . , Q n ∈ P 0 , and H is Q(r) for some Q ∈ P 0 where r is either a variable x ∈ vars(s 1 , . . . , s n ) a flat term g(z 1 , . . . , z m ) (k ≥ 0) whose variables z 1 , . . . , z m belong to vars(s 1 , . . . , s n ) and are pairwise distinct, or H is a splitting literal or else there is no H. Note that (sp) is a subcase of (l).

The following type (f) generalizes the type (gf) defined in the proof of Proposition 1:

Q 1 (y i1 ), . . . , Q k (y i k ), Q 1 f (y 1 , . . . , y n ) , . . . , Q m f (y 1 , . . . , y n ) ⇒ [ H ] (f)
where k, m ≥ 0, i 1 , . . . , i k ≤ n, y 1 , . . . , y n are distinct variables, P 1 , . . . , P k , P 1 , . . . .P m ∈ P, and H is of the form Q(y i ) or Q f (y 1 , . . . , y n ) with Q ∈ P, or H is a splitting literal or else there is no H, i.e. the clause is a goal.

The initial goal P (t) ⇒ belongs to type (l) and also belongs to (f) if t is a variable.

The different cases of saturation of A ∪ {P (t) ⇒} under basic ordered paramodulation are summarized in Figure 4 and detailed below.

inf. 1 st pr 2 nd pr cl inf. 1 st pr 2 nd pr cl inf. 1 st pr 2 nd pr cl

RP eq s l R s R s l (1) l R s l (2) f R s f f R sp l (3) l
(1) no negative splitting literals and at least one literal selected (2) no literal selected (3) at least one negative splitting literal (selected) Fig. 4. Case analysis in the proof of Proposition 5 RP(eq, eq) returns a clause of type (eq) which is deleted after simplification by rewriting by R, because by hypothesis, the equational theory of A is -convergent. RP(eq, s) returns a clause which is expanded into a clause of type (l).

⇒ f ( 1 , . . . , n ) = r Q 1 (x 1 ), . . . , Q 1 (x n ) ⇒ Q f (x 1 , . . . , x n ) RP Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q(y) x 1 = 1 , . . . , x n = n , y = r
Note that no further basic paramodulation step other than resolution is possible into the clauses obtained, because there are no function symbols in its unconstrained part.

LP(eq, s) is not possible because the antecedents of clauses of type (s) contain only variables. R( , s): no resolution step is possible into a clause of type (s) because of the maximality condition (v) in LP (see the proof of Proposition 1). R(s, l) return a clause of type (l) when one non-splitting negative literal P 1 (s 1 ) is selected in the premise of type (l), i.e. when s 1 = f (s 1 , . . . , s n ) (the tuple x 1 , . . . , x n is denoted x below):

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (s 1 ), . . . , P m (s m ) ⇒ [ H ] R Q 1 (s 1 ), . . . , Q n (s n ), P 2 (s 2 ), . . . , P m (s m ) ⇒ [ H ]
R(s, l) return a clause of type (f) when no negative literal is selected in the premise of type (l). Indeed, a clause of type (l) without a selected literal can have one of the following forms: P 1 (y 1 ), . . . , P m (y m ) ⇒ P g(y 1 , . . . , y m ) which is a particular case of (s), hence the resolution is not possible as seen above, or P 1 (y), . . . , P m (y) ⇒ P (y) where P 1 , . . . , P m , P ∈ P 0 P 1 (y), . . . , P m (y) ⇒ [ q ] where q ∈ Q is a splitting literal or else there is no head. In these two latter cases, the variable in the antecedent is unique, otherwise the clause would be split by ε-splitting. The corresponding resolution steps are the following:

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (y), . . . , P m (y) ⇒ P (y) R Q 1 (x 1 ), . . . , Q n (x n ), P 2 f (x) , . . . , P m f (x) ⇒ P f (x) Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (y), . . . , P m (y) ⇒ [ q ] R Q 1 (x 1 ), . . . , Q n (x n ), P 2 f (x) , . . . , P m f (x) ⇒ [ q ]
R(s, f) returns a clause of type (f) when one non-splitting literal at least is selected in the premise of type (f) (the tuples x 1 , . . . , x n and y 1 , . . . , y m are denoted resp. x and y below):

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (y i1 ), . . . , P k (y i k ), P 1 (f (y)), . . . , P m (f (y)) ⇒ [ H ] R P 1 (y i1 ), . . . , P k (y i k ), Q 1 (y 1 ), . . . , Q n (y n ), P 2 (f (y)), . . . , P m (f (y)) ⇒ [ H ] R(s, f) returns a clause of type (f) when no literal is selected in the premise of type (f); it is a subcase of R(s, l) (with (l) unselected) above. R(l, ), R(f, ): no resolution step can involve as first premise a clause of type (l) or (f) which is neither of type (s) nor of type (sp). Indeed, as we have seen above, a clause of this kind and without a selected literal must have the form: P 1 (y), . . . , P m (y) ⇒ P (y) or P 1 (y), . . . , P m (y) ⇒ [ q ] In both cases, the head of the clause cannot be strictly maximal w.r.t. lpo , contradicting the condition (iii) of LP. R(sp, l) returns a clause of type (l). The strict ordering on measures is defined as the lexicographic extension:

⇒ q 1 q 1 , . . . , q k , Q 1 (s 1 ), . . . , Q n (s n ) ⇒ [ H ] R q 2 , . . . , q k , Q 1 (s 1 ), . . . , Q n (s n ) ⇒ [ H ] -m 3 (C)
>, >, >, mul , (> mul , >), mul lpo lex , where > denotes the ordering on N. Fact 3 below permits to conclude the proof of Proposition 6. It refers to the following clause type (df) similar to (gf):

Q 1 (y i1 ), . . . , Q k (y i k ), Q 1 (f (y 1 , . . . , y n )), . . . , Q m (f (y 1 , . . . , y n )) ⇒ Q(r) (df)
where m ≥ 0, n > 0, y 1 , . . . , y n are distinct variables, i 1 , . . . , i k ≤ n, r is either one of the y i , with i ≤ n, or f (y 1 , . . . , y n ), and if Q is a test predicate then every test predicate among Q

1 , . . . , Q k , Q 1 , . . . , Q m is strictly smaller than Q (wrt ), otherwise, Q 1 , . . . , Q k , Q 1 , . . . , Q m ∈ P 0 .
Fact 3 Starting from A and a goal Q(t) ⇒, every step of basic ordered paramodulation and ε-splitting returns either a clause smaller than all its premises (wrt ) or a clause of type (df) or (gf).

Fact 3 is proved by a case analysis summarized in Figure 5 and detailed below. In this analysis, we need a new type of clauses (l + ) appearing during the saturation. Right paramodulation RP with an equational clause ⇒ f ( 1 , . . . , n ) → r into a clause of type (t) returns a clause expanded into the following form6 :

q 1 , . . . , q k , Q 1 ( 1 ), . . . , Q n ( n ) ⇒ Q(r) ( l + )
where n ≥ 0, 1 , . . . , n are linear, r is either ground or a variable x, q 1 , . . . , q k ∈ Q, and either Q 1 , . . . , Q n , Q ∈ P 0 or Q is a test predicate and at most one of Q 1 , . . . , Q n is equal to Q, and the others belong to P 0 .

Let us now detail the case analysis described in Figure 5.

Eq(d): equality resolution (Eq) is possible in the equations in clauses of type (d) (each of these equations is selected) and every such application of (Eq) return a clause of the following type (d ) with smaller m 2 .

Q 1 (x 1 ), . . . , Q n (x n ), u 1 = v 1 , . . . , u k = v k ⇒ Q(x) θ (d )
where where n, k ≥ 0, x 1 ,. . . ,

x n , x are distinct variables, u 1 , v 1 , . . . , u k , v k ∈ T F ,
= = > LP eq d/d d > = = > LP eq g + g + > = = > R t R t l+ (1) l+ = = > = = = = = > R t
d+ (1) d+

> = = = ≥ = > R t d+ (2) df R t df df R t g + (1) g + > = = ≥ = = > R t g + (2) gf R t gf gf R l+ R d+/df l+ d+ = = = = > = = = > R d+/df d+/df d+ > = = = > R d+/df g + /gf g + > = = ≥ > R sp l+ (3) l+ > = = = > R sp d+ (3) d+ > = = = > R sp g + (3) g + > = = = > R sp g + (3) sp εsplit l+ gf εsplit l+ l+ = = = ≥ = > εsplit d+ gf εsplit d+ d+ = = = ≥ = > εsplit g + gf εsplit g + g + = = = ≥ = >
(1) no neg. splitting literals and at least one literal selected (2) no literal selected

(3) at least one negative splitting literal (selected) Fig. 5. Case analysis in the proof of Proposition 6.

Eq(d ) also returns a clause of type (d ) smaller than the premise.

RP(eq, eq) returns a clause of type (eq) which is deleted after simplification by rewriting by R, because by hypothesis, the equational theory of A is presented as a convergent TRS (hence all critical pairs can be joined).

RP(eq, t) returns a clause expanded into type (l + ), smaller than both premises.

⇒ f ( 1 , . . . , n ) → r Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q f (x 1 , . . . , x n ) R Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q(x) x 1 = 1 , . . . , x n = n , x = r
Note that no further applications of RP or LP other than resolution is possible into such a clause, because of the basic strategy. LP(eq, t) is not possible with the basic strategy.

LP(eq, d) and LP(eq, d ) (into the equations selected by sel 2 ) return constrained clauses of type (d ) smaller than both premises. Indeed, every such step suppresses some symbols in the equations hence makes the measure m 3 decrease. Therefore, the calculus saturates on clauses of type (d) with equations, and terminates either with clauses of type (d + ) (without equations) or with clauses of type (d ) with equations which cannot be involved in any paramodulation step. Note that the clauses of type (d + ) can only be involved in resolution steps. LP(eq, g + ) return a clause of type (g + ) smaller than both premises. R( , t): no resolution step is possible into a clause of type (t) because of the maximality condition (v) in LP (see the proof of Proposition 4). R(t, l + ) returns a clause of type (l + ) smaller than both premises, when one non-splitting literal of the second premise (l + ) is selected, i.e. when 1 = f ( 1 , . . . , n ).

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q 1 f (x 1 , . . . , x n ) Q 1 ( 1 ), . . . , Q m ( m ) ⇒ Q (r) R Q 1 ( 1 ), . . . , Q n ( n ), Q 2 ( 2 ), . . . , Q m ( m ) ⇒ Q (r)
Note that with the definition of (t), the multiset of test predicates in (l + ) is unchanged or reduced during this resolution step. R(t, l + ) returns a clause of type (df) when the premise (l + ) has no selected negative literals. Indeed, this latter clause must have the form P 1 (x), . . . , P m (x) ⇒ P (x) where x is a variable, otherwise, it would be split by ε-splitting. Moreover, P is distinct from P 1 , . . . , P m , otherwise the clause would be a tautology.

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (x), . . . , P m (x) ⇒ P (x) R Q 1 (x 1 ), . . . , Q n (x n ), P 2 f (x) , . . . , P m f (x) ⇒ P f (x)
R(t, d + ) returns a clause of type (d + ) smaller than both premises when a negative literal P 1 (s 1 ) is selected in the premise (d + ) i.e. when s 1 = f (s 1 , . . . , s n ) (the tuple x 1 , . . . , x n is denoted x below):

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (s 1 ), . . . , P m (s m ) ⇒ P * (s) R Q 1 (s 1 ), . . . , Q n (s n ), P 2 (s 2 ), . . . , P m (s m ) ⇒ P * (s)
Note that with the restriction in the definition of (t) concerning the test predicates, the multiset of test predicates in (d + ) is unchanged or reduced during this resolution step. R(t, d + ) is not possible when no negative literal is selected in the second premise (d + ), by definition of type (d + ) and because of the ordering strategy. R(t, df) returns a clause of type (df) when the premise (df) has at least one negative literal selected (the tuples of variables x 1 , . . . , x n and y 1 , . . . , y n are respectively denoted x and y below):

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q 1 f (x)
P 1 (y i1 ), . . . , P k (y i k ), Q 1 f (y) , . . . , Q m f (y) ⇒ Q(r) R P 1 (y i1 ), . . . , P k (y i k ), Q 1 (y 1 ), . . . , Q n (y n ), Q 2 f (y) , . . . , Q m f (y) ⇒ Q(r) where r is either y i or f (y). R(t, df) returns a clause of type (df) when no negative literal is selected in the second premise (df): this case is similar to R(t, d + ) when (d + ) is not selected, which has been treated above. R(t, g + ) returns a clause of type (g + ) smaller than both premises when a negative literal P 1 (s 1 ) in the premise (g + ) is selected (i.e. when s 1 = f (s 1 , . . . , s n )):

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (s 1 ), . . . , P m (s m ) ⇒ [q] R Q 1 (s 1 ), . . . , Q n (s n ), P 2 (s 2 ), . . . , P m (s m ) ⇒ [q] R(t, g + ) returns a clause of type (gf) when no negative literal is selected in the premise (g + ). In this case, by ε-splitting, the premise (g + ) contains only one variable x:

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 f (x) P 1 (x), . . . , P m (x) ⇒ [q] R Q 1 (x 1 ), . . . , Q n (x n ), P 2 (f (x)), . . . , P m (f (x)) ⇒ [q] R(t, gf) returns a clause of type (gf) when the premise (gf) has at least one literal selected:

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q 1 f (x)
P 1 (y i1 ), . . . , P k (y i k ), Q 1 f (y) , . . . , Q m f (y) ⇒ [q] R P 1 (y i1 ), . . . , P k (y i k ), Q 1 (y 1 ), . . . , Q n (y n ), Q 2 f (y) , . . . , Q m f (y) ⇒ [q] R(t, gf) returns a clause of type (gf) when the premise (gf) has no negative literal selected. This is a subcase of the above step R(t, g + ) with (g + ) unselected. R(l + , ) is not possible. Indeed, let us consider a clause (l + ) not in (d + ) and without selected negative literals. It must have the (expanded) form Q 1 (x 1 ), . . . , Q n (x n ) ⇒ Q(r) where x 1 , . . . , x n are variables and r is either a ground term or a variable. If r is ground, the clause would be split by ε-splitting. If r is a variable, we must have x 1 = . . . = x n = r (because of the ε-splitting) and the resolution is not possible because the head of the clause cannot be strictly maximal, contradicting the condition (iii) in LP. R(d + , l + ) returns a clause of type (d + ) smaller than both premises. P 1 (x 1 ), . . . , P m (x m ) ⇒ Q * 1 (s) Q * 1 ( 1 ), Q 2 ( 2 ), . . . , Q n ( n ) ⇒ Q * 1 (r) R P 1 (x 1 θ), . . . , P n (x n θ), Q 2 ( 2 θ), . . . , Q n ( m θ) ⇒ Q * 1 (rθ) where θ = mgu(s, 1 ). Note that all the terms in the antecedents of the premise (d + ) are variables. Otherwise, some literal in this clause would be selected. By definition of (l + ), Q 2 , . . . , Q n are not test predicates and for every P i (i ≤ m) which is a test predicate Q * 1 P i . Hence m 4 is strictly smaller for the conclusion than for the premise (l + ). Moreover, m 5 is strictly smaller for the conclusion than for the first premise (d + ). We have the following cases:

If s is a variable, then, by splitting, we have x 1 = . . . , = x n = s. This would make the application of LP impossible, because of the ordering condition (iii) of this rule, and definition of the ordering lpo . Hence, we assume that s is not a variable. Moreover, all the variables x 1 , . . . , x n occur in s, otherwise, the clause (d + ) would be split. If r is a ground term, or if r is a variable which does not occur in 1 , then rθ = r. If r is a variable which occurs in 1 , then r = 1 , otherwise the premise (l + ) is a tautology. We can apply Lemma 2 to s, 1 (which is linear by hypothesis) and r, and if follows that m 5 (s) > m 5 (rθ). R(d + , d + ) and R(d + , df) both return a clause of type (d + ) smaller than both premises.

Q 1 (x 1 ), . . . , Q n (x n ) ⇒ P 1 (s) P 1 (t 1 ), . . . , P m (t m ) ⇒ P (t) R Q 1 (x 1 θ), . . . , Q n (x n θ), P 2 (t 2 θ), . . . , P m (t m θ) ⇒ P (tθ) where θ = mgu(s, t 1 ). R(d + , g + ) returns a clause of type (g + ) smaller than both premises: Q 1 (s 1 ), . . . , Q n (s n ) ⇒ P 1 (s) P 1 (t 1 ), . . . , P m (t m ) ⇒ [q] R Q 1 (s 1 θ), . . . , Q n (s n θ), P 2 (t 2 θ), . . . , P m (t m θ) ⇒ [q] where θ = mgu(s, t 1 ) and P 1 > Q 1 , . . . , Q n . R(d + , gf) is included in R(d + , g + ). R(df, l + ), R(df, d + ), R(df, df), and R(df, g + ): there are two cases of clause (df) without selected negative literal. Either such a clause has type (t), and the resolution steps have been treated above, or it has the form Q 1 (x), . . . , Q n (x) ⇒ Q(x), after ε-splitting. In the latter case, Q must be a test predicate. Indeed, otherwise, Q 1 , . . . , Q n , Q all belong to P 0 and it contradicts the condition (iii) of LP. Hence, the above clause has type (d + ) and the resolution cases are are subcases of R(d + , l + ), R(d + , d + ), R(d + , df), and R(d + , g + ) respectively. R(sp, l + ) returns a clause of type (l + ) smaller than both premises (note that m 1 (sp) = ∞).

⇒ q 1 q 1 , . . . , q k , Q 1 ( 1 ), . . . , Q n ( n ) ⇒ Q(r) R q 2 , . . . , q k , Q 1 ( 1 ), . . . , Q n ( n ) ⇒ Q(r) R(sp, d + ) returns a clause of type (d + ) smaller than both premises.

⇒ q 1 q 1 , . . . , q k , Q 1 (s 1 ), . . . , Q n (s n ) ⇒ Q(s) R q 2 , . . . , q k , Q 1 (s 1 ), . . . , Q n (s n ) ⇒ Q(s) R(sp, g + ) returns a clause of type (sp) or a clause of type (g + ) smaller than both premises.

⇒ q 1 q 1 , [ q 2 , . . . , q k , P 1 (s 1 ), . . . , P m (s m ) ] ⇒ [ q ] R [ q 2 , . . . , q k , P 1 (s 1 ), . . . , P m (s m ) ] ⇒ [ q ] Note that the conclusion is indeed smaller than the premise (sp) because m 1 (sp) = ∞. εsplit(l + ): the ε-splitting of such clauses returns a clause of type (gf) and a clause of type (l + ) smaller than the premise (B is an ε-block): q 1 , . . . , q k , B, Q 1 ( 1 ), . . . , Q n ( n ) ⇒ Q(r) εsplit B ⇒ q B q 1 , . . . , q k , q B , Q 1 ( 1 ), . . . , Q n ( n ) ⇒ Q(r) εsplit(d + ): the ε-splitting of a clause of type (d + ) returns a clause of type (gf) and a clause of type (d + ) smaller than the premise (B is an ε-block): q 1 , . . . , q k , B, Q 1 (s 1 ), . . . , Q n (s n ) ⇒ Q(s) εsplit B ⇒ q B q 1 , . . . , q k , q B , Q 1 (s 1 ), . . . , Q n (s n ) ⇒ Q(s) εsplit(g + ): the ε-splitting of a clause of type (g + ) returns a clause of type (gf) and a clause of type (g + ) smaller than the premise (B is an ε-block): q 1 , . . . , q k , B, P 1 (s 1 ), . . . , P m (s m ) ⇒ [ q ] εsplit B ⇒ q B q 1 , . . . , q k , q B , P 1 (s 1 ), . . . , P m (s m ) ⇒ [ q ]

Fig. 1 .

 1 Fig. 1. Transitions of the 2-counter machine

  is the number of function symbols in Γ , Ξ and H. Note that we consider here the number of function symbols without applying the constraint θ, It means in particular that this m 3 is unchanged by resolution, only leftand right-paramodulation on non variable terms may change m 3 , m 4 (C) is the multiset of test predicate symbols occurring in Γ , m 5 (C) = m 5 (s) if H = Q(s), and m 5 (C) = ({}, 0) is the other cases, m 6 (C) is the multiset of the negative non-equational literals of Γ θ.

  disequality constraint) for some positions p and p (sequences of integers), Q is maximal in {Q, Q 1 , . . . , Q n } (here, we do not assume that the ordering on predicates is total) and it is moreover strictly maximal if c contains at least one equality constraint. An equality constraint as above (resp. disequality constraint) is satisfied by every two ground terms t, t ∈ T (F ) such that p ∈ Pos(t), p ∈ Pos(t ) and t| p = t | p (resp. p ∈ Pos(t), p ∈ Pos(t ) and t| p = t | p ). Given a RA A and a state Q of A, the language L(A, Q) is defined as in page 4 (extending the definition from Horn clause to constrained Horn clauses). The definition of GMP and emptiness problems for RA follow.

  a goal not of type (sp), i.e. if Γ is not empty and H is a splitting literal or there is no H, m 2 (C) is the number of equations in Ξ, m 4 (C) is the multiset of test predicate symbols occurring in Γ , m 6 (C) is the multiset of the negative non-equational literals of Γ θ.

  {x 1 , . . . , x n , x} , and Q > Q 1 , . . . , Q n . The type (d ) with k = 0 (no equation) is just a subcase of (d + ). Recall that the clauses obtained from clauses of type (d) which contain no more equations have type (d + ).

	inf. 1 st	2 nd	cl	1 st premise	2 nd premise
	pr.	pr.		m1 m2 m3 m4 m5 m6 m1 m2 m3 m4 m5 m6
	Eq d/d		d /d+ = >
	RP eq	t	l+	>

We shall sometimes underline literals to indicate that they are selected.

GMP with linear facts can be shown decidable.

and we shall sometimes mark a predicate Q with an asterisk like in Q * to indicate that it is a test predicate.

For the sake of simplicity we denote Q1(x1), x = u ⇒ Q(x) by Q1(x1) ⇒ Q(u).

We abbreviate pair(t1, pair(t2, . . . , pair(tn-1, tn))) by t1, . . . , tn (n ≥ 2).

Note that no further applications of RP or LP other than resolution is possible into the clause obtained, because of the basic strategy.

Acknowledgments. We wish to thank Stéphanie Delaune for her contribution to early phases of this work, Anne-Cécile Caron and Sophie Tison for their feedback on our undecidability results, and Jean Goubault-Larrecq and Christopher Lynch for their help about splitting techniques.

LSV Research Report 2006-07, http://lsv.ens-cachan.fr/ This work has been partially supported by the research projects RNTL PROUV É (No 03 V 360) and ACI-SI SATIN and ROSSIGNOL.

Appendix A Definitions of orderings

A reduction ordering > is a well-founded ordering on T (F ∪ P ∪ Q, X ) stable under substitutions and such that for all g ∈ F ∪ P ∪ Q, for all s, t ∈ T (F , X ) we have s > t implies g(. . . , s, . . .) > g(. . . , t, . . .). The multiset extension > mul of an ordering > is defined as the smallest ordering relation on multisets such that M ∪ {t} > mul M ∪ {s 1 , . . . , s n } whenever t > s i for all i ≤ n. The lexicographic extension (> 1 , . . . , > n ) lex of n orderings to n-tuples is defined as (s 1 , s 2 , . . . , s n )(> 1 , . . . , > n ) lex (t 1 , t 2 , . . . , t n ) if s 1 = t 1 ,. . . , s k-1 = t k-1 , and s k > k t k for some k ∈ 1 . . . n.

We can define a reduction ordering on T (F ∪P ∪Q, X ) total on ground terms by extending the precedence to a lexicographic path ordering [START_REF] Dershowitz | Rewrite systems, chapter Handbook of Theoretical Computer Science[END_REF] denoted lpo with: s = f (s 1 , s 2 , . . . , s m ) lpo g(t 1 , t 2 , . . . , t n ) = t iff 1. f g and s lpo t i for all 1 ≤ i ≤ n; or 2. f ∼ g and, for some j, we have (s 1 , . . . , s j-1 ) = (t 1 , . . . , t j-1 ), s j lpo t j and s lpo t k , for all k with j < k ≤ n; or 3. s j lpo t, for some j with 1 ≤ j ≤ m.

Then as in [START_REF] Bachmair | Basic Paramodulation[END_REF] we identify a positive literal s = t with the multiset {{s}, {t}}, and a negative literal s = t with the multiset {{s, t}}. Then we extend the ordering lpo (resp. lpo ) to literals by taking the twofold multiset ordering (( lpo ) mul ) mul (resp. (( lpo ) mul ) mul ).

Appendix B Proof of Proposition 1 (TA)

Recall that the selection function sel 1 selects in a Horn clause Γ ⇒ H θ :

every splitting negative literal, if any, -otherwise every non-equational literal Q(t) of Γ such that tθ is not a variable. Fix a TA A and a goal clause P (t) ⇒ and consider ordered resolution wrt lpo and the selection function sel 1 with eager application of the εsplit rule of Section 3. We assume wlog that P ∈ P 0 , otherwise the problem is trivial by definition of (s). We show that all the clauses generated have the type (gs) (goal-subterm), or (gf), (goal-flat), whose definition are recalled below: q 1 , . . . , q k , P 1 (s 1 ), . . . , P m (s m ) ⇒ [ q ] ( gs)

where m, k ≥ 0, s 1 , . . . , s m ∈ st(t). P 1 , . . . , P m ∈ P 0 , and q 1 , . . . , q k , q are splitting literals (the q in the head is optional, as indicated by the square brackets).

where k, m ≥ 0, i 1 , . . . , i k ≤ n, y 1 , . . . , y n are distinct variables, P 1 , . . . , P k , P 1 , . . . .P m ∈ P 0 , and q is a splitting literal (it is optional in the

Appendix E Proof of Proposition 4 (TAD)

Let sel 2 be a selection function which selects in a Horn clause C θ :

every splitting negative literal, if any, -otherwise, the equational negative literals of C, if C contains any, -otherwise, every (non-equational and non-splitting) negative literal Q(t) of C such that tθ is not a variable (if any).

Let us fix a TAD A and a goal clause P (t) ⇒ . We are going to show the termination of the saturation of A ∪ {P (t) ⇒ } under ordered paramodulation wrt the ordering lpo and the selection function sel 2 , with eager ε-splitting. Note first that with our selection strategy, the clauses of A of type (d) containing equations can only be involved in an equality resolution (Eq). Every such application solves (and remove) an equation (selected by sel 2 ), hence saturation of the clauses of type (d) under (Eq) terminates. Let us call (d + ) the type of clauses obtained this way (and with ε-splitting) from clauses of (d) and which contain no more equations.

Appendix G Relating RA, TAD and TADE

Let us consider a reduction automaton A, as defined in Section 5, with equality constraints only, and assume moreover that the transitions of A fulfill the restrictions on predicates introduced in the definition of TAD. More precisely, it means that for every clause (red) of A of the form

c contains no disequality constraint, -if c contains equality constraints, then Q is a test predicate, and for all i ≤ n such that

. . , Q n is equal to Q, and the others belong to P 0 .

We show how to construct a TADE B of the same size as A and which recognizes the same language. Let us first consider a -convergent sublinear-collapsing theory suitable for that purpose. Let a be the maximal arity of a function symbol of F and let us add new function symbols π 1 , . . . , π a to F . Consider the rewrite system R containing all rules of the form π i (f (x 1 , . . . , x n )) → x i for f ∈ F, i ≤ n. This system is convergent sublinear and collapsing. We add to B every clause ⇒ = x such that → x ∈ R. Every clause (red) of A as above with an empty constraint c has actually the type t, and is added to B.

To a clause (red) of A as above with c =

associate the following clause of type (d):

where π p (x) denotes π p1 (. . . π p k (x)) given a position p = p 1 . . . p k . For every state

Note that a reduction automaton of the above kind can also be transformed into an equivalent TAD, but at the cost of an exponential explosion, in order to fill with function symbols the positions prefix of p and p associated to each constraint

Appendix H Proof of Proposition 6 (TADE)

Before we start the proof of Proposition 6, let us introduce the following measure on terms: m 5 (u) = (mvar (u), |u|) where mvar (u) is the multiset of the numbers of occurrences for each variable in u and |u| is the size of u, that is the number of symbols in u. The measure of terms are compared using a lexicographic extension of orderings for each component. We denote by |u| z the number of occurrence of symbol z in term u. The following lemma will be used in the proof of saturation. Lemma 2. We consider terms s, t and a variable x such that vars(s)∩vars(t) = ∅, s is not a variable, t is linear, x ∈ vars(t), x = t, and σ is an mgu of s and t. Then m 5 (xσ) is strictly less than m 5 (s).

Proof. If s is linear then xσ has at most the same number of variables than s and has size smaller than s. Assume now that s is not linear. By applying eagerly Decompose, Orient (and Trivial) rules of unification algorithm to the system {s = t} we get the following equivalent system: X ∪ Y where X = {x 1 = s 1 , . . . , x n = s n } and Y = {y 1 = t 1 , . . . , y m = t m } with {x 1 , . . . , x n } ⊆ vars(t) and {y 1 , . . . , y m } ⊆ vars(s). The variables x 1 , . . . , x n have a unique occurrence in the whole system. Let us note too that every variable in t i 's is in vars(t) and therefore occurs only once in the system. As a consequence if we consider the system of equations T = {t i = t j | y i = y j , 1 ≤ i, j ≤ m}. We can check that it has a most general solution σ with support D included in vars(t) \ {x 1 , . . . , x n } and for each variable z in this support, zσ is a subterm of t and the variables in zσ occurs only once in X ∪ Y ∪ T . Applying some replacements the initial system gets equivalent to

where by abuse of notation σ is identified with the subsystem {z = zσ | z ∈ D}.

Then from this step all possible Replacement rule applications are performed using some equations of type y i = t i σ.

If x does not occur in a left-hand side in X , then mvar (xσ) is a multiset of 1 and therefore strictly less than mvar (s).

Assume now wlog that x is the variable x 1 . If no Replacement is applied on s 1 , since s 1 is a strict subterm of s, m 5 (xσ) < m 5 (s). If a nonempty sequence of Replacements is applied to s 1 , then we get a sequence of right-hand sides: s 1 1 , . . . , s q 1 and we can show by induction that mvar (s j i ) < mvar (s): Applying the replacement y j+1 = t j+1 on s j 1 has effect to replace |s j 1 | yj+1 occurrences of variable y j+1 by |s j 1 | yj+1 occurrences of each of the (linear) variables from t j+1 . Since |s 1 | yj+1 = |s j 1 | yj+1 < |s| yj+1 , then mvar (t j+1 ) < mvar (s). 2

Let us now prove Proposition 6. We assume given a TADE A and a goal clause Q(t) ⇒ . We note R the TRS corresponding to the clauses of type (eq) of A. We will show the termination of the saturation of A ∪ {Q(t) ⇒} under basic ordered paramodulation wrt the ordering lpo and the selection function sel 2 (defined in the proof of Proposition 4) and with eager ε-splitting.

The measure of a clause C = Γ, Ξ ⇒ H θ , where Γ is a multiset of non-equational atoms and Ξ is a multiset of equations, is the tuple (m 1 (C), . . . , m 6 (C)) where:

m 1 (C) = ∞ if H is an equation, and is defined like in the proof of Proposition 4 otherwise, m 2 (C) is the number of equations in Ξ,