Khalil Djelloul

Thi-Bich-Hanh Dao

Theory of Finite or Infinite Trees Revisited

Keywords: Logical first-order formula, Theory of finite or infinite trees, Complete theory, Rewriting rules

We present in this paper a first-order axiomatization of an extended theory T of finite or infinite trees, built on a signature containing an infinite set of function symbols and a relation finite(t) which enables to distinguish between finite or infinite trees. We show that T has at least one model and prove its completeness by giving not only a decision procedure, but a full first-order constraint solver which gives clear and explicit solutions for any first-order constraint satisfaction problem in T . The solver is given in the form of 16 rewriting rules which transform any first-order constraint ϕ into an equivalent disjunction φ of simple formulas such that φ is either the formula true or the formula false or a formula having at least one free variable, being equivalent neither to true nor to false and where the solutions of the free variables are expressed in a clear and explicit way. The correctness of our rules implies the completeness of T . We also describe an implementation of our algorithm in CHR (Constraint Handling Rules) and compare the performance with an implementation in C++ and that of a recent decision procedure for decomposable theories.

schemes [START_REF] Courcelle | Fundamental Properties of Infinite Trees[END_REF][START_REF] Courcelle | Equivalences and Transformations of Regular Systems applications to Program Schemes and Grammars[END_REF]) and A. Colmerauer has described the execution of Prolog II, III and IV programs in terms of solving equations and disequations in the algebra of finite or infinite trees [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF][START_REF] Colmerauer | An introduction to Prolog III[END_REF][START_REF] Benhamou | Le manuel de Prolog IV[END_REF].

Concerning quantified constraints, solving universally quantified disequations on finite trees has been studied by D.A. Smith [START_REF] Smith | Constraint operations for CLP[END_REF] and there exist some decision procedures which transform any first-order formula into a Boolean combination of quantified conjunctions of atomic formulas using elimination of quantifiers. In the case of finite trees we can refer to A. Malcev [START_REF] Malcev | Axiomatizable classes of locally free algebras of various types[END_REF], K. Kunen [START_REF] Kunen | Negation in logic programming[END_REF]) and H. Comon [START_REF] Comon | Unification et disunification : Theorie et applications[END_REF]Comon 1991b;[START_REF] Comon | Equational problems and disunification[END_REF]. For infinite trees, we can refer to the work of H. Comon [START_REF] Comon | Unification et disunification : Theorie et applications[END_REF]Comon 1991a) and M. Maher [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF].

M. Maher has axiomatized all the cases by complete first-order theories [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF]. In particular, he has introduced the theory T of finite or infinite trees built on an infinite set F of function symbols and showed its completeness using a decision procedure which transforms any first-order formula ϕ into a Boolean combination φ of quantified conjunctions of atomic formulas. If ϕ does not contain free variables then φ is either the formula true or false.

K. Djelloul has then presented in (Djelloul 2006a) the class of decomposable theories and proved that the theory of finite or infinite trees is decomposable. He has also given a decision procedure in the form of five rewriting rules which, for any decomposable theory, transforms any first-order formula ϕ into an equivalent conjunction φ of solved formulas easily transformable into a Boolean combination of existentially quantified conjunctions of atomic formulas. In particular, if ϕ has no free variables then φ is either the formula true or ¬true.

Unfortunately, all the preceding decision procedures are not able to solve complex first-order constraint satisfaction problems in T . In fact, these algorithms are only basic decision procedures and not full first-order constraint solvers: they do not warrant that the solutions of the free variables of a solved formula are expressed in a clear and explicit way and can even produce, starting from a formula ϕ which contains free variables, an equivalent solved formula φ having free variables but being always false or always true in T . The appropriate solved formula of ϕ in this case should be the formula false or the formula true instead of φ. If we use for example the decision procedure of (Djelloul 2006a) to solve the following formula ϕ ¬(∃y x = f (y) ∧ ¬(∃zw x = f (z) ∧ w = f (w))), then we get the following solved1 formula φ

¬(∃y x = f (y) ∧ ¬(∃z x = f (z))).
The problem is that this formula contains free variables but is always true in the theory of finite or infinite trees. In fact, it is equivalent to

¬(∃y x = f (y) ∧ ¬(∃z x = f (y) ∧ x = f (z))),
i.e. to ¬(∃y x = f (y) ∧ ¬(x = f (y) ∧ (∃z z = y))), thus to ¬(∃y x = f (y) ∧ ¬(x = f (y))), which is finally equivalent to true. As a consequence, the solved formula of ϕ should be true instead of φ. This is a good example which shows the limits of the decision procedures in solving first-order constraints having at least one free variable.

Much more elaborated algorithms are then needed, specially when we want to induce solved formulas expressing solutions of complex first-order constraint satisfaction problems in the theory of finite or infinite. Of course, our goal in these kinds of problems is not only to know if there exist solutions or not, but to express these solutions in the form of a solved first-order formula φ which is either the formula true (i.e. the problem is always satisfiable) or the formula false (i.e. the problem is always unsatisfiable) or a simple formula which is neither equivalent to true nor to false and where the solutions of the free variables are expressed in a clear and explicit way. Algorithms which are able to produce such a formula φ are called first-order constraint solvers.

We have then presented in (Djelloul and Dao 2006b), not only a decision procedure, but a full first-order constraint solver in the theory T of finite or infinite trees, in the form of 11 rewriting rules, which gives clear and explicit solutions for any first-order constraint satisfaction problem in T . The intuitions behind this algorithm come from the works of T. Dao in [START_REF] Dao | Resolution de contraintes du premier ordre dans la theorie des arbres finis ou infinis[END_REF] where many elegant properties of the theory of finite or infinite trees were given. As far as we know, this is the first algorithm which is able to do a such work in T .

This is an extended and detailed version with full proofs of our previous work on the theory T of finite or infinite trees (Djelloul and Dao 2006b). Moreover, in this paper we extend the signature of T by the relation finite(t) which forces the term t to be a finite tree. Then we extend Maher's axiomatization by two new axioms and show its completeness by giving an extended version of our previous first-order constraint solver (Djelloul and Dao 2006b). We also describe a CHR (Constraint Handling Rules) implementation of our rules and compare the performances with those obtained using a C++ implementation of our solver and the decision procedure for decomposable theories (Djelloul 2006a).

Overview of the paper

This paper is organized in five sections followed by a conclusion. This introduction is the first section. In section 2, we introduce the structure of finite or infinite trees and give formal definitions of trees, finites trees, infinite trees and rational trees. We end this section by presenting particular algebras which handle finite or infinite trees.

In section 3, after a brief recall on first-order logic, we present the five axioms of our extended theory2 T of finite or infinite trees built on a signature containing not only an infinite set of function symbols, but also a relation finite(t) which enables to distinguish between finite or infinite trees. We then extend the algebras given at the end of section 2 by the relation finite(t) and show that these extended algebras are models of T . In particular, we show that the models of sets of nodes, of finite or infinite trees and of rational trees are models of T .

In section 4, we present structured formulas that we call working formulas and give some of their properties. These working formulas are extensions of those given in (Djelloul 2006a). We also introduce the notion of reachable variables and show that there exist particular formulas which have only quantified reachable variables, do not accept elimination of quantifiers and cannot be simplified any further. Such formulas are called general solved formulas. We then present 16 rewriting rules which handle working formulas and transform an initial working formula into an equivalent conjunction of final working formulas from which we can extract easily an equivalent conjunction of general solved formulas. We end this section by a full first-order constraint solver in T . This algorithm uses, among other things, our 16 rules and transforms any first-order formula ϕ into a disjunction φ of simple formulas such that φ is either the formula true or the formula false or a formula having at least one free variable, being equivalent neither to true nor to false and where the solutions of the free variables are expressed in a clear and explicit way. The correctness of our algorithm implies the completeness of T .

Finally, in section 5, we give a series of benchmarks. Our algorithm was implemented in C++ and CHR [START_REF] Fruehwirth | Theory and Practice of Constraint Handling Rules[END_REF][START_REF] Fruehwirth | Essentials of Constraint Programming[END_REF][START_REF] Schrijvers | Automatic implication checking for CHR constraints[END_REF]. The C++ implementation is able to solve formulas of a two player game involving 80 nested alternated quantifiers. Even if the C++ implementation is fastest, we found interesting to see how we can translate our algorithm into CHR rules. Using this high-level approach, we will be able to quickly prototype optimizations and variations of our algorithm and hope to parallelize it. We also compare the performances with those of C++ implementation of the decision procedure for decomposable theories3 (Djelloul 2006a).

The axiomatization of T , the proof that T has at least one model, the 16 rewriting rules, the proof of the correctness of our rules, the first-order constraint solver in T , the completeness of T , the CHR implementation, the two player game and the benchmarks are new contributions in this paper.

2 The structure of finite or infinite trees

What is a tree?

Trees are well known objects in the computer science world. Here are some of them: their nodes are labeled by the symbols a,b,f,s of respective arities 0,0,2,1. While the first tree is a finite tree, i.e. it has a finite set of nodes, the two others are infinite trees, i.e. they have an infinite set of nodes.

Let us now number from 1 to n and from left to right the branches that connect each node l to his n sons. We get:

Each node c labeled by l can now be seen as a pair (p, l) where p is the position of the node, i.e. the smallest series of positive integers that we meet if we move from the root of the tree to the node c. Thus, the preceding trees can be represented by the following sets of nodes: Let us now formalize all the preceding statements. Let L be a (possibly infinite) set. Its elements are called labels. To each label l ∈ L is linked a non-negative integer called arity of l. An n-ary label is a label of arity n. A position is a word built on strictly positive integers (the empty word is denoted by ε). Let p be a position and l a label. The pair (p, l) is called node and its depth is the length 4 of p. An n-ary node is a node whose label is of arity n. A root is a node of depth 0. The row of an n-ary node, with n = 0, is the last integer of its position. We say that c is the father of c ′ or c ′ is the son of c if c and c ′ are nodes whose positions are respectively of the form i 1 ...i k and i 1 ...i k i k+1 , where the i j 's are strictly positive integers and k a (possibly null5 ) positive integer. Let us denote by N the set of the nodes labeled by elements of L.

{(ε, f ),
Definition 2.1.1 A node c of N is called arborescent in a sub-set N 1 of N if N 1 = ∅ and either c ∈ N 1 , or c ∈ N 1 and the two following conditions hold:

• N 1 -{c} does not contain any node whose position is the same than those of c, • c is either a root or the son of an n-ary node of N 1 which has exactly n sons in N 1 of respective rows 1, ..., n.

We can now define formally a tree: Definition 2.1.2 A tree tr is a sub-set of N such that each element of N is arborescent in tr. A finite tree is a tree whose set of nodes is finite. An infinite tree is a tree whose set of nodes is infinite.

Let us now define the notion of subtree:

Definition 2.1.3
Let tr be a tree. The subtree linked to a node (i 1 ...i k , l) of tr is the set of the nodes of the form (i k+1 ...i k+n , l ′ ) with (i 1 ...i k+n , l ′ ) ∈ tr and6 n ≥ 0. We call subtree of tr a subtree linked to one of the nodes of tr. A subtree of tr of depth k is a subtree linked to a node of tr of depth k.

From Definition 2.1.2, we deduce that each subtree of a tree tr is also a tree.

Definition 2.1.4

A rational tree is a tree whose set of subtrees is a finite set.

Note that an infinite tree can be rational. In fact, even if its set of nodes is infinite but n subtrees linked to n different nodes can be similar. Let us see this in the following example:

Example 2.1.5 Let us consider the three trees presented in the beginning of Section 2.1. Let us name them from left to righ by: tr 1 , tr 2 and tr 3 . The set of the subtrees of tr 1 is the following finite set:

           {(ε, a)}, {(ε, b)}, {(ε, s), (1, a)}, {(ε, f ), (1, a), (2, b)}, {(ε, f ), (1, f ), (2, s), (11, a), (12, b), (21, a)}            i.e.
The set of the subtrees of tr 2 is the following finite set: The set of the subtrees of tr 3 is the following infinite set:

       {(ε, a)}, {(ε, b)}, {(ε, f ), (1,
                         {(ε, a)}, {(ε, s), (
                         i.e.
Note that the tree tr 1 has a finite set of nodes and a finite set of subtrees. Thus, it is a finite rational tree. The tree tr 2 has an infinite set of nodes but a finite set of subtrees. Thus, it is an infinite rational tree. The tree tr 3 has an infinite set of nodes and an infinite set of subtrees. Thus, it is an infinite non-rational tree. Note also that a rational tree can always be represented by a finite directed graph. For that, it is enough to merge all the nodes whose linked subtrees are similar. A non-rational tree cannot be represented by a finite directed graph. In this case, only an infinite directed graph representation will be possible. For example, the trees tr 1 , tr 2 and tr 3 can be represented as follows:

Of course, two different directed graphs can represent the same tree. For example the trees tr 2 and tr 3 can also be represented as follows:

Construction operations

We would like to provide the set T r of finite or infinite trees with a set of construction operations ; one for each label l of L. These operations will be schematized as follows:

with n the arity of the label l. In order to formally define these construction operations, we need first to define them in the set D of sets of nodes7 of N . Let i be a strictly positive integer. If d = (j 1 ...j k , l) is a node then we denote by i.

1. a = b ↔ ∞ k=1 ν k (a) = ν k (b). 2. ν 0 (l D (a 1 , ..., a n )) = {(ε, l)}.
3. For all k ≥ 0, there exists a function ϕ k+1 which is independent from all the ν k+1 (a i ), with i ∈ {1, ..., n}, such that ν k+1 (l D (a 1 , ..., a n )) = ϕ k+1 (ν k (a 1 ), ..., ν k (a n )). 4. The elements of ν 0 (l D (a 1 , ..., a n )) are arborescent in l D (a 1 , ..., a n ). 5. For all k ≥ 0, the elements of ν k+1 (l D (a 1 , ..., a n )) are arborescent in l D (a 1 , ..., a n ) if and only if, for each i ∈ {1, ..., n}, the elements of

ν k (a i ) are arborescent in a i . 6. If for all k ≥ 0 the elements of ν k (l D (a 1 , ..., a n )) are arborescent in l D (a 1 , ..., a n ) then each element of N is arborescent in l D (a 1 , ..., a n ).
Let now F be an infinite set of function symbols. Let us denote by:

• N the set of the nodes labeled by F ,

• D the set of sets of nodes of N , • T r the set of the elements of D which are trees,

• Ra the set of the elements of T r which are rational,

• F i the set of the elements of T r which are finite.

If f is an n-ary function symbol taken from F then the operation of construction f D associated to f is an application of the form D n → D. Let tr 1 , ..., tr n be elements of T r. From the fourth and fifth point of Remark 2.2.2 we deduce that f D (tr 1 , ..., tr n ) is also a tree, i.e. an element of T r. Thus, we can introduce the following application:

f T r : (tr 1 , ..., tr n ) → f D (tr 1 , ..., tr n ) which is of type T r n → T r.
On the other hand, the set of the subtrees of the tree f D (tr 1 , ..., tr n ) is obtained by the union of the sets of the subtrees of all the tr i plus the tree f D (tr 1 , ..., tr n ). Thus, if all the tr i 's are rational trees then the tree f D (tr 1 , ..., tr n ) is rational. As a consequence, we can introduce the following application:

f Ra : (tr 1 , ..., tr n ) → f D (tr 1 , ..., tr n ) which is of type Ra n → Ra.
Finally, if all the tr i 's are finite trees, then the tree f D (tr 1 , ..., tr n ) is finite. Thus, we can introduce the following application:

f F i : (tr 1 , ..., tr n ) → f D (tr 1 , ..., tr n ) which is of type F i n → F i. The pairs < D, (f D ) f ∈F >, < T r, (f T r ) f ∈F >, < F i, (f F i ) f ∈F > and <
Ra, (f Ra ) f ∈F > are known as the algebras of sets of nodes, of finite or infinite trees, of finite trees and of rational trees.

3 The extended theory T of finite or infinite trees

Formal preliminaries

Formulas

We are given once and for all an infinite countable set V of variables and the set L of logical symbols:

=, true, false, ¬, ∧, ∨, →, ↔, ∀, ∃, (, ).

We are also given once and for all a signature S, i.e. a set of symbols partitioned into two subsets: the set of function symbols and the set of relation symbols. To each element s of S is linked a non-negative integer called arity of s. An n-ary symbol is a symbol of arity n. A 0-ary function symbol is called constant.

As usual, an expression is a word on L ∪ S ∪ V which is either a term, i.e. of one of the two forms:

x, f (t 1 , . . . , t n ), (1)
or a formula, i.e. of one of the eleven forms:

s = t, r(t 1 , . . . , t n ), true, false, ¬ϕ, (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ), (ϕ ↔ ψ), (∀x ϕ), (∃x ϕ). (2)
In (1), x is taken from V , f is an n-ary function symbol taken from S and the t i 's are shorter terms. In (2), s, t and the t i 's are terms, r is an n-ary relation symbol taken from S and ϕ and ψ are shorter formulas. The set of the expressions forms a first-order language with equality.

The formulas of the first line of (2) are known as atomic, and flat if they are of one of the following forms:

true, false, x 0 = x 1 , x 0 = f (x 1 , ..., x n ), r(x 1 , ..., x n ),
where all the x i 's are (possibly non-distinct) variables taken from V , f is an n-ary function symbol taken from S and r is an n-ary relation symbol taken from S. An equation is a formula of the form s = t with s and t terms.

An occurrence of a variable x in a formula is bound if it occurs in a sub-formula of the form (∀x ϕ) or (∃x ϕ). It is free in the contrary case. The free variables of a formula are those which have at least one free occurrence in this formula. A proposition or a sentence is a formula without free variables. If ϕ is a formula, then we denote by var(ϕ) the set of the free variables of ϕ.

The syntax of the formulas being constraining, we allowed ourselves to use infix notations for the binary symbols and to add and remove brackets when there are no ambiguities. Moreover, we do not distinguish two formulas which can be made equal using the following transformations of sub-formulas:

ϕ ∧ ϕ =⇒ ϕ, ϕ ∧ ψ =⇒ ψ ∧ ϕ, (ϕ ∧ ψ) ∧ φ =⇒ ϕ ∧ (ψ ∧ φ), ϕ ∧ true =⇒ ϕ, ϕ ∨ false =⇒ ϕ.
If I is the set {i 1 , ..., i n }, we call conjunction of formulas and write i∈I ϕ i , each formula of the form ϕ i1 ∧ϕ i2 ∧...∧ϕ in ∧true. In particular, for I = ∅, the conjunction i∈I ϕ i is reduced to true.

Model

A model is a tuple M = < M, (f M ) f ∈F , (R M ) r∈R >, where:

• M , the universe or domain of M, is a nonempty set disjoint from S, its elements are called individuals of M; • F and R are sets of n-ary functions and relations in the set M , subscripted by the elements of S and such that:

for every n-ary function symbol f taken from S, f M is an n-ary operation in M , i.e. an application from M n in M . In particular, when f is a constant, f M belongs to M ; -for every n-ary relation symbol r taken from S, r M is an n-ary relation in M , i.e. a subset of M n .

Let M = < M, F, R > be a model. An M-expression ϕ is an expression built on the signature S ∪ M instead of S, by considering the elements of M as 0-ary function symbols. If for each free variable x of ϕ we replace each free occurrence of x by a same element m in M , we get an M-expression ϕ ′ called instantiation 8 or valuation of ϕ by individuals of M.

If ϕ is an M-formula, we say that ϕ is true in M and we write

M |= ϕ, (3)
if for any instantiation ϕ ′ of ϕ by individuals of M the set M has the property expressed by ϕ′, when we interpret the function and relation symbols of ϕ′ by the corresponding functions and relations of M and when we give to the logical symbols their usual meaning.

Remark 3.1.3 For every M-formula ϕ without free variables, one and only one of the following properties holds: M |= ϕ, M |= ¬ϕ.

Let us finish this sub-section by a convenient notation. Let x = x 1 ...x n be a word on V and let ī = i 1 ...i n be a word on M or V of the same length as x. If ϕ(x) and φ are two M-formulas, then we denote by ϕ( ī), respectively φ x← ī , the M-formula obtained by replacing in ϕ(x), respectively in φ, each free occurrence of x j by i j .

Theory

A theory is a (possibly infinite) set of propositions called axioms. We say that the model M is a model of T , if for each element ϕ of T , M |= ϕ. If ϕ is a formula, we write T |= ϕ, 8 We also say that the variable x is instantiated by m in ϕ ′ .

if for each model M of T , M |= ϕ. We say that the formulas ϕ and ψ are equivalent in T if T |= ϕ ↔ ψ. Definition 3.1.5 A theory T is complete if for every proposition ϕ, one and only one of the following properties holds: T |= ϕ, T |= ¬ϕ.

Let φ be a formula and x = x 1 ...x n be a word on V such that var(φ) = x. From the preceding definition we deduce that a decision procedure is sufficient in the case where we want just to show the completeness of a theory T , as it was done in (Djelloul 2006a) for decomposable theories. In fact, the completeness of T depends only on the truth values of the propositions in T . On the other hand, finding for each model M of T the instantiations ī of x such that M |= φ x← ī can be obtained only using a first-order constraint solver in T . This kind of problem is generally known as first-order constraint satisfaction problem.

Vectorial quantifiers

Let M be a model and T a theory. Let x = x 1 . . . x n and ȳ = y 1 . . . y n be two words on V of the same length. Let φ, ϕ and ϕ(x) be M-formulas. We write

∃x ϕ for ∃x 1 ...∃x n ϕ, ∀x ϕ for ∀x 1 ...∀x n ϕ, ∃?x ϕ(x) for ∀x∀ȳ ϕ(x) ∧ ϕ(ȳ) → i∈{1,...,n} x i = y i , ∃!x ϕ
for (∃x ϕ) ∧ (∃?x ϕ).

The word x, which can be the empty word ε, is called vector of variables. Note that the formulas ∃?εϕ and ∃!εϕ are respectively equivalent to true and to ϕ in any model M.

Notation 3.1.7 Let Q be a quantifier taken from {∀, ∃, ∃!, ∃?}. Let x be vector of variables taken from V . We write:

Qx ϕ ∧ φ f or Qx (ϕ ∧ φ).
Example 3.1.8 Let I = {1, ..., n} be a finite set. Let ϕ and φ i with i ∈ I be formulas. Let x and ȳi with i ∈ I be vectors of variables. We write:

∃x ϕ ∧ ¬φ 1 for ∃x (ϕ ∧ ¬φ 1 ), ∀x ϕ ∧ φ 1 for ∀x (ϕ ∧ φ 1 ), ∃!x ϕ ∧ i∈I (∃ȳ i φ i ) for ∃!x (ϕ ∧ (∃ȳ 1 φ 1 ) ∧ ... ∧ (∃ȳ n φ n ) ∧ true), ∃?x ϕ ∧ i∈I ¬(∃ȳ i φ i ) for ∃?x (ϕ ∧ (¬(∃ȳ 1 φ 1 )) ∧ ... ∧ (¬(∃ȳ n φ n )) ∧ true).
Notation 3.1.9 If x is a vector of variables then we denote by X the set of the variables of x.

Let I be a (possible empty) finite set. The two following properties hold for any theory T :

Property 3.1.10 If T |= ∃?x ϕ then T |= (∃x ϕ ∧ i∈I ¬φ i ) ↔ ((∃xϕ) ∧ i∈I ¬(∃x ϕ ∧ φ i )). Property 3.1.11 If T |= ∃!x ϕ then T |= (∃x ϕ ∧ i∈I ¬φ i ) ↔ i∈I ¬(∃x ϕ ∧ φ i ).
Full proofs of these two properties can be found in detail in (Djelloul 2006a).

The axioms of T

Let F be a set of function symbols containing infinitely many non-constant function symbols and at least one constant. Let finite be an 1-ary relation symbol. The theory T of finite or infinite trees built on the signature S = F ∪ {finite} has as axioms the infinite set of propositions of one of the five following forms:

∀x∀ȳ ¬(f (x) = g(ȳ)) [1] ∀x∀ȳ f (x) = f (ȳ) → i x i = y i [2] ∀x∃!z i z i = t i [xz] [3] ∀x∀u ¬(u = t[u, x] ∧ finite(u)) [4] ∀x∀u (u = f (x) ∧ finite(u)) ↔ (u = f (x) ∧ i finite(x i )) [5]
where f and g are distinct function symbols taken from F , x is a vector of (possibly non-distinct) variables x i , ȳ is a vector of (possibly non-distinct) variables y i , z is a vector of distinct variables z i , t i [xz] is a term which begins with an element of F followed by variables taken from x or z, and t[u, x] is a term containing at least one occurrence of an element of F and the variable u and possibly other variables taken from x. For example, we have

T |= ∀x 1 x 2 ∀u ¬(u = f 1 (x 1 , f 2 (u, x 2 )) ∧ finite(u)) and T |= ∀u¬(u = f 1 (f 2 (u, f 0 ), f 0 ) ∧ finite(u))
where f 1 and f 2 are 2-ary function symbols and f 0 a constant of F .

The forms [1],..., [5] are also called schemas of axioms of the theory T . Proposition [1] called conflict of symbols shows that two distinct operations produce two distinct individuals. Proposition [2] called explosion shows that the same operation on two distinct individuals produces two distinct individuals. Proposition [3] called unique solution shows that a certain form a conjunction of equations has a unique set of solutions in T . In particular, the formula ∃z z = f (z) has a unique solution which is the infinite tree f (f (f (...))). Proposition [4] means that a finite tree cannot be a strict subtree of itself. We emphasize strongly that t[u, x] should contain at least one occurrence of an element of F and the variable u. In Axiom [5], if x is the empty vector and f is a constant then we get ∀u u = f ∧ finite(u) ↔ u = f , which means that the property finite(f ) is true for each constant f of F . This theory is an extension of the basic theory of finite or infinite trees given by M. Maher in [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF]) and built on a signature containing an infinite set of function symbols. Maher's theory is composed of the three first axioms of T and its completeness was shown using a decision procedure which transforms each proposition into a Boolean combination of existentially quantified conjunctions of atomic formulas. Note also that both Maher's theory and the theory T do not accept full elimination of quantifiers, i.e. there exist some quantified formulas whose quantifiers cannot be eliminated. For example, the formula ∃x y = f (x) is neither true nor false in T . It accepts in each model of T a set of solutions and another set of non-solutions. As a consequence, we cannot simplify it any further. This non-full elimination of quantifiers makes the completeness of T not evident.

The models of T

Let us extend the algebras given at the end of section 2.2 by the relation finite. More precisely, if u 1 , u 2 , u 3 and u 4 are respectively elements of D, T r, F i and Ra then the operations finite D (u 1 ), finite T r (u 2 ), finite F i (u 3 ) and finite Ra (u 4 ) are true respectively in D, T r, F i and Ra, if and only if u 1 , u 2 , u 3 and u 4 have a finite set of nodes.

Let us now denote by:

• D =< D, (f D ) f ∈F , finite D >, the model of sets of nodes, • T r =< T r, (f T r ) f ∈F , finite T r >, the model of finite or infinite trees, • Ra =< Ra, (f Ra ) f ∈F , finite Ra >, the model of rational trees, • Fi =< F i, (f F i ) f ∈F , finite F i >, the model of finite trees.
We have:

Theorem 3.3.1
The models D, T r and Ra are models of the theory T .

This theorem is one of the essential contributions given in this paper and shows that our theory T is in fact an axiomatization of the structures D, T r and Ra together with an infinite set of construction operations and the 1-ary relation finite. It also shows that T has at least one model and thus T |= ¬(true ↔ false). Proof, first part: Let us show first that the model D of sets of nodes is a model of T . In other words, we must show that the following properties hold:

[1 D ] (∀a1, ..., am ∈ D)(∀b1, ..., bn ∈ D) ¬(f D (a1, ..., am) = g D (b1, ..., bn)) [2 D ] (∀a1, ..., an ∈ D)(∀b1, ..., bn ∈ D) (f D (a1, ..., an) = f D (b1, ..., bn) → n i=1 ai = bi) [3 D ] (∀a1, ..., am ∈ D)(∃!b1, ..., bn ∈ D) ( n i=1 bi = t D i [b1, ..., bn, a1, ..., am]) [4 D ] (∀a1, ..., am ∈ D)(∀u ∈ D)¬(u = t D [u, a1, ..., an] ∧ finite D (u)) [5 D ] (∀a1, ..., an ∈ D)(∀u ∈ D)(u = f D (a1, ..., an) ∧ finite D (u)) ↔ (u = f D (a1, ..., an) ∧ n i=1 finite D (ai))
where f and g are distinct function symbols taken from F , t D i [b 1 , ..., b n , a 1 , ..., a m ] is a term which begins with an element of F followed by variables taken from {a 1 , ..., a m , b 1 , ..., b n }, and t D [u, a 1 , ..., a n ] is a term containing at least one occurrence of an element of F and the variable u and possibly other variables taken from {a 1 , ..., a n }. According to Definition 2. • For each i ∈ {1, ..., n} there exists one node

i = t D i [b 1 , ..., b n , a 1 , ..., a m ], (4)
is equivalent in D to ∞ k=0 n i=1 ν k (b i ) = ν k (t D i [b 1 , ...,
ϕ i 0 = (ε, f i ), such that ν 0 (t D i [b 1 , ..., b n , a 1 , ..., a m ]) = {ϕ i 0 }. • For each i ∈ {1, ..., n} and each k ≥ 0 there exists a function ϕ i k+1 , which is independent from all the ν k+1 (x), with x ∈ [b 1 , ..., b n , a 1 , ..., a m ] i , such that ν k+1 (t D i [b 1 , ..., b n , a 1 , ..., a m ]) = ϕ i k+1 ([ν k (b 1 ), ..., ν k (b n ), ν k (a 1 ), ..., ν k (a m )] i ), where [ν k (b 1 ), ..., ν k (b n ), ν k (a 1 ), ..., ν k (a m )] i is a tuple of elements of the form ν k (x) for all x ∈ [b 1 , ..., b n , a 1 , ..., a m ] i .
Thus, the D-formula (5) is equivalent in D to

( n i=1 ν 0 (b i ) = {ϕ i 0 })∧( ∞ k=0 n i=1 ν k+1 (b i ) = ϕ i k+1 ([ν k (b 1 ), ..., ν k (b n ), ν k (a 1 ), ..., ν k (a m )] i )),
from which we deduce that:

• (i) For all i ∈ {1, ..., n}, ν 0 (b i ) has a constant value, which is equal to (ε, f i ). • (ii) Each ν k+1 (b i ) depends in the worst case on ν k (b 1 ), ..., ν k (b n ), ν k (a 1 ), ..., ν k (a m ), i.e. on ν k (b 1 ), ..., ν k (b n ) and a 1 , ..., a m .
Thus, by recurrence9 on k, we deduce that (iii) each ν k+1 (b i ) with k ≥ 0 and i ∈ {1, ..., n}, depends only on a 1 , ..., a m . From (i) and (iii) we deduce that all the b i 's depend only on a 1 , ..., a m and thus property [3 D ] holds. In other words, for each instantiation of a 1 , ..., a m by elements of D we can deduce the values of ν k (b i ) for all i ∈ {1, ..., n} and k ≥ 0.

We have shown that the model D satisfies the five axioms of T and thus it is a model of T .

Proof, second part: Let us now show that the model T r of finite or infinite trees is a model of T . For that, it is enough to show the validity of the following properties [1 T r ] (∀a1, ..., am ∈ T r)(∀b1, ..., bn ∈ T r) ¬(f T r (a1, ..., am) = g T r (b1, ..., bn)) [2 T r ] (∀a1, ..., an ∈ T r)(∀b1, ..., bn ∈ T r) (f T r (a1, ..., an) = f T r (b1, ..., bn) b1, ..., bn, a1, ..., am])

→ n i=1 ai = bi) [3 T r ] (∀a1, ..., am ∈ T r)(∃!b1, ..., bn ∈ T r) ( n i=1 bi = t T r i [
[4 T r ] (∀a1, ..., am ∈ T r)(∀u ∈ T r)¬(u = t T r [u, a1, ..., an] ∧ finite T r (u)) [5 T r ] (∀a1, ..., an ∈ T r)(∀u ∈ T r)(u = f T r (a1, ..., an) ∧ finite T r (u)) ↔ (u = f T r (a1, ..., an) ∧ n i=1 finite T r (ai))
where f and g are distinct function symbols taken from F , t T r i [b 1 , ..., b n , a 1 , ..., a m ] is a term which begins with an element of F followed by variables taken from {a 1 , ..., a m , b 1 , ..., b n }, and t T r [u, a 1 , ..., a n ] is a term containing at least one occurrence of an element of F and the variable u and possibly other variables taken from {a 1 , ..., a n }. Since T r is a subset of D, then according to the definition of f T r , f D , finite T r and finite D , the properties and[5 T r ]. On the other hand, to show property [3 T r ], it is enough to show the following implication:

[1 D ], [2 D ], [4 D ] and [5 D ] imply [1 T r ], [2 T r ], [4 T r ]
(∀a1, ..., am, b1, ...bn ∈ D)((( n i=1 bi = t D i [b1, ..., bn, a1, ..., am])∧( m i=1 ai ∈ T r)) → ( n i=1 bi ∈ T r)) (6)
Let a, b, a 1 ,...,a m , b 1 ,...,b n be elements of D. Let us consider the following notation:

Arb(a, b) ↔ each element of a is arborescent in b.
According to Definition 2.1.2, the T r-formula

( n i=1 b i = t D i [b 1 , ..., b n , a 1 , ..., a m ]) ∧ ( m i=1 a i ∈ T r), is equivalent in T r to ( n i=1 b i = t D i [b 1 , ..., b n , a 1 , ..., a m ]) ∧ ( m i=1 Arb(N, a i )),
which is equivalent to

( n i=1 b i = t D i [b 1 , ..., b n , a 1 , ..., a m ]) ∧ ( ∞ k=0 m i=1 Arb(ν k (N ), a i )), (7)
which for each

j ≥ 0 is equivalent in T r to ( n i=1 b i = t D i [b 1 , ..., b n , a 1 , ..., a m ]) ∧ ( ∞ k=0 m i=1 Arb(ν k (N ), a i )) ∧ ( n i=1 Arb(ν j (b i ), b i )).
(8) The equivalence (7 ↔ 8) holds for j = 0 according to the fourth point of Remark 2.2.2, and if we assume that this equivalence holds for an integer j with j ≥ 0 then according to the fifth point of Remark 2.2.2, we deduce that it holds also for j + 1. Thus, since the equivalence (7 ↔ 8) holds for any j ≥ 0 then according to the sixth point of Remark 2.2.2 and Definition 2.1.2 we deduce that (8) implies

n i=1 Arb(N, b i ), which, according to Definition 2.1.2, implies n i=1 b i ∈ T r.
Thus, the implication (6) holds and T r is a model of T .

Proof, third part: Finally, let us show that the model Ra is a model of T . For that, it is enough to show the validity of the following properties:

[1 Ra ] (∀a1, ..., am ∈ Ra)(∀b1, ..., bn ∈ Ra) ¬(f Ra (a1, ..., am) = g Ra (b1, ..., bn)) [2 Ra ] (∀a1, ..., an ∈ Ra)(∀b1, ..., bn ∈ Ra) (f Ra (a1, ..., an) = f Ra (b1, ..., bn) → n i=1 ai = bi) [3 Ra ] (∀a1, ..., am ∈ Ra)(∃!b1, ..., bn ∈ Ra) ( n i=1 bi = t Ra i [b1, ..., bn, a1, ..., am]) [4 Ra ] (∀a1, ..., am ∈ Ra)(∀u ∈ Ra)¬(u = t Ra [u, a1, ..., an] ∧ finite Ra (u)) [5 Ra ] (∀a1, ..., an ∈ Ra)(∀u ∈ Ra)(u = f Ra (a1, ..., an) ∧ finite Ra (u)) ↔ (u = f Ra (a1, ..., an) ∧ n i=1 finite Ra (ai))
where f and g are distinct function symbols taken from F , t Ra i [b 1 , ..., b n , a 1 , ..., a m ] is a term which begins with an element of F followed by variables taken from {a 1 , ..., a m , b 1 , ..., b n }, and t Ra [u, a 1 , ..., a n ] is a term containing at least one occurrence of an element of F and the variable u and possibly other variables taken from {a 1 , ..., a n }. Since Ra is a subset of T r and according to the definitions of f T r , f Ra , finite T r and finite Ra then the properties [1 and[5 Ra ]. On the other hand, in property [3 T r ], (in the preceding proof), a subtree of depth k of any b i is either one of the trees b 1 ,..., b n or a subtree of one of the a j 's with i ∈ {1, ..., n} and j ∈ {1, ..., m}. This is true for k = 0 and if we assume that it is true for k then we deduce that it is true for k + 1. Thus, if the a j 's are rational then the b i 's in [3 T r ] are also rational and thus we get [3 Ra ].

T r ], [2 T r ], [4 T r ] and [5 T r ] imply [1 Ra ], [2 Ra ], [4 Ra ]
We have shown that the models D, T r and Ra are models of T . What about the model Fi of finite trees? Since F contains at least one function symbol f which is not a constant then according to Axiom [3] of T we have

T |= ∃!x x = f (x, ..., x).
It is obvious that this property cannot be true in Fi, i.e. there exists no x ∈ F i such that x = f F i (x, ..., x). Thus, the model Fi of finite trees is not a model of T .

Let us end this section by a property concerning the cardinality of any model of T :

Property 3.3.2 Let M =< M, (f M ) f ∈F , finite M > be a model of T . The model M has an infinity of individuals i such that M |= finite M (i).

Proof

Since the set F contains at least one function symbol f which is a constant then according to Axiom [5], with x = ε, we have

M |= finite M (f M ). ( 9
)
On the other hand, according to the definition of the signature of T , the set F contains an infinity of distinct function symbols which are not constants. Let f 1 one of these symbols. According to (9) and Axiom [5] we have

M |= finite M (f M 1 (f M , ..., f M )), thus the individual f M 1 (f M , ..., f M ) is finite in M.
Since the set F contains an infinity of distinct function symbols f 1 , f 2 , f 3 , ... which are not constants then we can create by following the same preceding steps an infinity of finite individuals 4 Solving first-order constraints in T

f M 1 (f M , ..., f M ), f M 2 (f M , ..., f M ), f M 3 (f M , ..., f M ), .

Discipline of the formulas in T

Let us assume that the infinite set V is ordered by a strict linear dense order relation without endpoints denoted by ≻. Starting from this section, we impose the following discipline to every formula ϕ in T : the quantified variables of ϕ are renamed so that:

• (i) The quantified variables of ϕ have distinct names and different from those of the free variables. • (ii) For all variables x, y and all sub-formulas10 ϕ i of ϕ, if y has a free occurrence in ϕ i and x has a bound occurrence in ϕ i then x ≻ y.

Example 4.1.1 Let x, y, z, v be variables of V such that x ≻ y ≻ z ≻ v. Let ϕ be the formula

∃x x = f y ∧ ¬(∃z z = x)∧ ¬(∃z z = v) . ( 10
)
The quantified variables of ϕ have no distinct names. Since the order ≻ is dense and without endpoints, there exists a variable w in V such that x ≻ y ≻ z ≻ v ≻ w, and thus ϕ is equivalent in T to

∃x x = f y ∧ ¬(∃z z = x)∧ ¬(∃w w = v) .
In the preceding formula, the variables z and w have bound occurrences while the variables y and v have free occurrences. Since x ≻ y ≻ z ≻ v ≻ w then z and w must be renamed. On the other hand, since the order ≻ is dense and without endpoints, there exist two variables u and

d in V such that x ≻ u ≻ d ≻ y ≻ z ≻ v ≻ w. Thus, the preceding formula is equivalent in T to ∃x x = f y ∧ ¬(∃u u = x)∧ ¬(∃d d = v) .
In the sub-formula (∃u u = x) the variable x has a free occurrence while the variable u has a bound occurrence. Since x ≻ u then u must be renamed. On the other hand, since the order ≻ is dense and without endpoints, there exists a variable

n in V such that n ≻ x ≻ u ≻ d ≻ y ≻ z ≻ v ≻ w. Thus, the preceding formula is equivalent in T to ∃x x = f y ∧ ¬(∃n n = x)∧ ¬(∃d d = v) . ( 11
)
This formula satisfies our conditions. Of course, the equivalence between ( 11) and ( 10) holds because in each step we renamed only the quantified variables. It is obvious that we can always transform any formula ϕ into an equivalent formula φ, which respects the discipline of the formulas in T , only by renaming the quantified variables of ϕ. It is enough for that to rename the quantified variables by distinct names and different from those of the free variables and then check each sub-formula and rename the quantified variables if the condition (ii) does not hold.

We emphasize strongly that all the formulas which will be used starting from now satisfy the discipline of the formulas in T .

Basic formula

In this sub-section we introduce particular conjunctions of atomic formulas that we call basic formulas and show some of their properties. All of them will be used to show the correctness of our rewriting rules given in section 4.6.

Definition 4.2.1 Let v 1 , ..., v n , u 1 , ..., u m be variables. A basic formula is a formula of the form ( n i=1 v i = t i ) ∧ ( m i=1 finite(u i )) (12)
in which all the equations v i = t i are flat. Note that if n = m = 0 then ( 12) is reduced to true. The basic formula ( 12) is called solved if all the variables v 1 , ..., v n , u 1 , ..., u m are distinct and for each equation of the form x = y we have x ≻ y. If α is a basic formula then we denote by

• Lhs(α) the set of the variables which occur in the left hand sides of the equations of α. • F IN I(α) the set of the variables which occur in a sub-formula of α of the form finite(x).

Note that if α is a solved basic formula then for all variables x of α we have

x ∈ Lhs(α) → x ∈ F IN I(α). Example 4.2.2 The basic formula x = x ∧ finite(y) is not solved because x ≻ x. The basic formula x = f (y) ∧ z = f (y) ∧ finite(x)
is also not solved because x is a left hand side of an equation and occurs also in finite(x). The basic formulas true (empty conjunction) and x = f (y) ∧ z = f (y) ∧ finite(y) are solved.

According to the axiom [3] of T we deduce the following property:

Property 4.2.3
Let α be a solved basic formula containing only equations. Let x be the vector of the variables of Lhs(α). We have:

T |= ∃!x α.

Proof

Let α and β be two solved basic formulas containing only equations such that Lhs(α) = Lhs(β) and T |= α → β. Let us show that we have also T |= β → α. Let x be the vector of the variables of Lhs(α) and let ȳ be the vector of the variables which occur in α → β and do not occur in x. Since α and β are two solved basic formulas such that Lhs(α) = Lhs(β) then (i) x is also the vector of the left hand sides of the equations of β. Moreover, the following equivalences are true in T :

α → β ↔ ∀x∀ȳ α → β ↔ ∀ȳ∀x ¬α ∨ β ↔ ∀ȳ(¬(∃x α ∧ ¬β)) ↔ ∀ȳ(¬(¬(∃x α ∧ β))) according to the properties 4.2.3 and 3.1.11 ↔ ∀ȳ(¬(¬(∃x β ∧ α))) ↔ ∀ȳ(¬(∃x β ∧ ¬α))
according to: (i) and Property 4.2.3 and using the other sense (right to left) of the equivalence of Property 3.1.11

↔ ∀ȳ∀x ¬β ∨ α ↔ ∀ȳ∀x β → α ↔ β → α Property 4.2.5
Let α be a basic formula containing only equations and β and δ two conjunctions of constraints of the form finite(x) such that α ∧ β and α ∧ δ are solved basic formulas. We have T |= (α ∧ β) ↔ (α ∧ δ) if and only if β and δ have exactly the same contraints.

Proof

If β and δ have the same constraints then it is evident that we have T |= (α ∧ β) ↔ (α ∧ δ). Let us now show that if we have T |= (α ∧ β) ↔ (α ∧ δ) then β and δ have the same constraints. Suppose that we have (*) T |= (α ∧ β) ↔ (α ∧ δ) and let us show that if finite(u) occurs in β then it occurs also in δ and vice versa.

If finite(u) occurs in β then T |= (α ∧ β) → finite(u), thus from (*) we have (i) T |= (α ∧ δ) → finite(u).
Since α ∧ β is solved then u is not the left hand side of an equation of α. Thus, (ii) the conjunction α ∧ δ does not contain sub-formulas of the form u = t[x] ∧ i finite(x i ). Since α ∧ δ is solved then δ does not contain formulas of the form finite(v) where v is the left hand side of an equation of α. Thus, (iii) the conjunction α ∧ δ does not contain also sub-formulas of the form v = t[x, u] ∧ finite(v). From (i), (ii) and (iii), finite(u) should occur in δ. By the same reasoning (we replace β by δ and vice versa), we show that if finite(u) occurs in δ then it occurs in β.

Let us now introduce the notion of reachable variable: Definition 4.2.6 Let α be a basic formula and x a vector of variables. The reachable variables and equations of α from the variable x 0 are those which occur in a sub-formula of α of the form:

x 0 = t 0 (x 1 ) ∧ x 1 = t 1 (x 2 ) ∧ ... ∧ x n-1 = t n-1 (x n ),
where x i+1 occurs in the term t i (x i+1 ). The reachable variables and equations of ∃x α are those which are reachable in α from the free variables of ∃x α. A subformula of α of the form finite(u) is called reachable in ∃x α if u ∈ x or u is a reachable variable of ∃x α.

Example 4.2.7

In the formula:

∃uvw z = f (u, v) ∧ v = g(v, u) ∧ w = f (u, v) ∧ finite(u) ∧ finite(x), the equations z = f (u, v) and v = g(v, u
), the variables z, u and v and the formulas finite(u) and finite(x) are reachable. On the other hand the equation w = f (u, v) and the variable w are not reachable.

Remark 4.2.8

Let α be a solved basic formula. Let x be a vector of variables. We have:

• If all the variables of x are reachable in ∃x α then all the equations and relations of α are reachable in ∃x α.

• If v = t[y] is a reachable equation in ∃x α, then α contains a sub-formula of the form k j=1 v j = t j [v j+1 ] ( 13
)
with k ≥ 1 and (i) v 1 ∈ X, (ii) for all j ∈ {1, ..., k} the variable v j+1 occurs in the term t

j [v j+1 ], (iii) v k is the variable v, (iv) v k+1 is the variable y and t k [v k+1 ] is the term t[y].
According to the first point of Remark 4.2.8 and Definition 4.2.6 we have the following property: Property 4.2.9 Let α be a solved basic formula. If the formula ∃x α has no free variables and if all the variables of x are reachable in ∃x α then x is the empty vector ε and α is the formula true.

According to the axioms [1] and [2] of T we have the following property: Property 4.2.10 Let α be a basic formula. If all the variables of x are reachable in ∃x α then

T |= ∃?x α.
Property 4.2.11 Let x be a vector of variables and α a solved basic formula. We have:

T |= (∃x α) ↔ (∃x ′ α ′ ),
where:

• x′ is the vector of the variable of x which are reachable in ∃x α, • α ′ is the conjunction of the equations and the formulas of the form finite(x) which are reachable in ∃x α.

Proof

Let us decompose x into three vectors x′ , x′′ and x′′′ such that:

• x′ is the vector of the variables of x which are reachable in ∃x α.

• x′′ is the vector of the variables of x which are non-reachable in ∃x α and do not occur in the left hand sides of the equations of α. • x′′′ is the vector of the variables of x which are non-reachable in ∃x α and occur in a left hand side of an equation of α.

Let us now decompose α into three formulas α ′ , α ′′ and α ′′′ such that:

• α ′ is the conjunction of the equations and the formulas of the form finite(x) which are reachable in ∃x α. • α ′′ is the conjunction of the formulas of the form finite(x) which are non-reachable in ∃x α. • α ′′′ is the conjunction of the equations which are non-reachable in ∃x α.

According to Definition 4.2.6, all the variables of x′′ and x′′′ do not occur in α ′ (otherwise they will be reachable) and since α is solved then x′′′ is the vector of the left hand sides of the equations of α ′′′ and its variables do not occur in α ′′ . Thus the formula ∃x α is equivalent in T to

(∃x ′ α ′ ∧ (∃x ′′ α ′′ ∧ (∃x ′′′ α ′′′ ))).
According to Property 4.2.3 we have T |= ∃!x ′′′ α ′′′ . According to Corollary 3.3.3 we have T |= ∃x ′′ α ′′ . Thus, the preceding formula is equivalent in T to (∃x ′ α ′ ).

Example 4.2.12

The formula ∃xyzw

v = f (x, x) ∧ w = g(y, z, x) ∧ finite(x) ∧ finite(y) is equivalent in T to ∃x v = f (x, x) ∧ finite(x) ∧ (∃yz finite(y) ∧ (∃w w = g(y, z, x))), which, since T |= ∃!w w = g(y, z, x) and T |= ∃yz finite(y), is equivalent in T to ∃x v = f (x, x) ∧ finite(x).
Property 4.2.11 confirms the fact that the theory T does not accept full elimination of quantifiers and shows that we can eliminate only non-reachable quantified variables. On the other hand, reachable variables cannot be removed since their values depend on the instantiations of the free variables. In fact, the formula ∃x v = f (x, x) ∧ finite(x) is neither true nor false in T since for each model M of T there exist instantiations of the free variable v which make it false in M and others which make it true in M, and thus the reachable quantified variable x cannot be eliminated and the formula ∃x v = f (x, x) ∧ finite(x) cannot be simplified anymore. On the other hand, the formula ∃w w = g(y, z, x) is true in any model of T and for any instantiation of z. The quantified non-reachable variable w can then be eliminated and the formula is replaced by true. As we will see in section 4.6, reachability, has a crucial role while solving first-order constraints in T . It shows which quantifications can be eliminated and enables to simplify complex quantified basic formulas.

According to the axioms [1] and [2] and since the set F is infinite we have the following property: Property 4.2.13 Let I = {1, ..., n} be a finite (possibly empty) set and x and x′ two disjoint vectors of variables. Let ȳ1 ,...,ȳ n be vectors of variables and α 1 ,...,α n solved basic formulas such that for all i ∈ I all the variables of ȳi are reachable in ∃ȳ i α i . If each conjunction α i contains at least (1) one sub-formula of the form finite(x) with x ∈ X, or (2) one equation which contains at least one occurrence of a variable x ∈ X ∪ X ′ , then:

T |= ∃xx ′ ( x∈X ′ finite(x)) ∧ ( i∈I ¬(∃ȳ i α i )). ( 14
) Proof Let M =< M, (f M ) f ∈F , finite M > be a model of T .
To show the validity of ( 14) it is enough to show that:

M |= ∃xx ′ ( x∈X ′ finite M (x)) ∧ ( i∈I ¬(∃ȳ i α i )). ( 15
)
Since the basic formulas α i are solved, they do not contain equations of the form x = x. Suppose now that one of the α i contains one equation of the form x = v with x ∈ X ∪ X ′ and v ∈ Y i . Since α i is solved then x ≻ v but according to the discipline of the formulas in T we have v ≻ x11 . Since the order ≻ is strict then x = v cannot be a sub-formula of α i . Thus, according to the conditions of Property 4.2.13, each conjunction α i contains at least (1) one sub-formula of the form finite(x) with x ∈ X, or (2) one equation of the one of the following forms:

• (*) x = f (v 1 , ...v n ) with x ∈ X ∪ X ′ , • (**) x = v with x and v two distinct variables such that x ∈ X ∪ X ′ and v ∈ Y , • (***) v = t[x] where x is a variable of X ∪ X ′ which
k j=1 v j = t j [v j+1 ]) with v 1 ∈ Y i ,
for all j ∈ {1, ..., k} the variable v j+1 occurs in the term t j [v j+1 ] and v k+1 is the variable x. But, since the case v 1 ∈ X ∪ X ′ is already treated in (*) and (**), then we can restrict ourself without loosing generality to the case where

v 1 ∈ Y i ∪ X ∪ X ′ , i.e. v 1 is free in (15). Let ∃xx ′ ( x∈X ′ finite M (x)) ∧ ( i∈I ¬(∃ȳ i α * i )) (16) be an any instantiation of ∃xx ′ ( x∈X ′ finite M (x)) ∧ ( i∈I ¬(∃ȳ i α i )) by individuals of M.
Let us show that there exists an instantiation for the variables of X and X ′ which satisfies the preceding formula. For that, let us chose an instantiation which respects the following conditions:

• (i) For each x ∈ X ′ , the instantiation x * of x satisfies M |= finite M (x * ).
• (ii) If a conjunction α * i contains a sub-formula of the form finite M (x) with x ∈ X then the instantiation x * of x satisfies M |= x * = f M (x * , ..., x * ) with f an n-ary function symbol of strictly positive arity which does not occur in any α i with i ∈ I.

• (iii) If a conjunction α * i contains a sub-formula of the form x = f M (v 1 , ...v n ) with x ∈ X ∪ X ′ , then the instantiation of x starts with a different function symbol than f . • (iv) If a conjunction α * i contains a sub-formula of the form x = v with x and v two distinct variables such that x ∈ X ∪ X ′ and v ∈ Y , then the instantiation of x is different from those of v. • (v) If a conjunction α * i contains a sub-formula of the form ( k j=1 v j = t j [v j+1 ]) with v 1 ∈ (X ∪ X ′ ∪ Y ), for all j ∈ {1, ..., k} the variable v j+1 occurs in the term t j [v j+1 ], and v k+1 ∈ X ∪ X ′ , then the instantiation of v k+1 is different from v * , where v * is the instantiation of v k+1 obtained from those of v 1 in 12 (16) so that M |= k j=1 v j = t j [v j+1 ].
A such instantiation of the variables of X and X ′ is always possible since : (1) there exists an infinity of function symbols in F which are not constants (2) the set of the individuals i of M such that M |= finite M (i) is infinite (see Property 3.3.2). As a consequence, according to axioms [1] and [4], this instantiation implies a conflict inside each sub-instantiated-formula ∃ȳ i α * i , with i ∈ {1, ..., n} and thus

M |= ∃xx ′ ( i∈I ¬(∃ȳ i α * i )).
Since this instantiation satisfies the first condition (i) of the preceding list of conditions then ( 16) holds and thus (15) holds.

We emphasize strongly that this property holds only if the formula ( 14) satisfies the discipline of the formulas in T . This property is vital for solving first-order constraint over finite or infinite trees. In fact, since the variables of each ȳi with i ∈ {1, ..., n} are reachable in ∃ȳ i α i then we cannot eliminate or remove the quantification ∃ȳ i form ∃ȳ i α i , and thus solving a constraint containing such formulas is not evident. Property 4.2.13 enables us to surmount this problem by reducing to true particular formulas containing sub-formulas which does not accept full elimination of quantifiers.

Example 4.2.14 Let x, y, z and v be variables such that y ≻ x ≻ z ≻ w. Let us consider the following formula ϕ:

∃x   ¬(∃y z = f (y) ∧ y = g(x))∧ ¬(∃ε x = w)∧ ¬(∃ε x = g(x))   . ( 17
)
This formula satisfies the discipline of the formulas in T . Let M =< M, (f M ) f ∈F , finite M > be a model of T . Note that we cannot eliminate the quantifier ∃y in the sub-formula ∃y z = f (y)∧y = g(x). In fact, this sub-formula is neither true nor false in T because there exist instantiations of the free variable z in M which satisfy this sub-formula in M and others which do not satisfy it. On the other hand, Property 4.2.13, states that formula (17) is true in T for all instantiations of z even if the sub-formula ∃y z = f (y) ∧ y = g(x) is neither true nor false in T . Let us check this strange result. For that, let us show that for each instantiation of the free variables z and w by two individuals z * and w * of M, there exists an instantiation x * of x which makes false the three M-formulas (∃y z * = f M (y) ∧ y = g(x * )), (∃ε x * = w * ) and (∃ε x * = g(x * )). We have:

• In the formula (∃y z = f (y) ∧ y = g(x)), the variable x is reachable. Thus, its value is determined by the value of z (because z = f (g(x))). Two cases arise:

-If z * is of the form f (g(i)) with i ∈ M then it is enough to instantiate x by an individual x * ∈ M which is different from 13 i, in order to make false (∃y z * = f M (y) ∧ y = g M (x * )) in M.

13 For example, we can take x * = f M (i).

if z * is not of the form f (g(i)) with i ∈ M then the M-formula (∃y z * = f M (y) ∧ y = g M (x)) is false in M for all the instantiations of x.

• In the M-formula (∃ε x = w * ), it is enough to instantiate x by an element x * of M which is different from w * in order to make false the M-formula (∃ε x * = w * ). • In the M-formula (∃ε x = g M (x)), it is enough to instantiate x by an individual which starts by a distinct function symbol than g in order to make false (∃ε x = g M (x)) in M.

Since the set of the functions symbols which are not constants is infinite then there exists an infinity of instantiations of x which satisfy the three preceding conditions. Each of these instantiations x * makes false the three M-formulas (∃y z * = f M (y) ∧ y = g M (x * )), (∃ε x * = w * ) and (∃ε x * = g M (x * )) and thus (17) holds.

Normalized formula

Definition 4.3.1 A normalized formula ϕ of depth d ≥ 1 is a formula of the form ¬(∃x α ∧ i∈I ϕ i ), (18)
with I a finite (possibly empty) set, α a basic formula and the ϕ ′ i s are normalized formulas of depth d i with d = 1 + max{0, d 1 , ..., d n }.

Example 4.3.2 Let f and g be two 1-ary function symbols which belong to F . The formula

¬ ∃ε finite(u) ∧ ¬(∃x y = f (x) ∧ x = g(y) ∧ ¬(∃ε y = g(x) ∧ finite(x)))∧ ¬(∃ε x = f (z) ∧ finite(z))
is a normalized formula of depth equals to three. The formula ¬(∃ε true) is a normalized formula of depth 1. The smallest value of a depth of a normalized formula is 1. Normalized formulas of depth 0 are not defined and do not exist.

We will use now the abbreviation wnfv for "without new free variables". A formula ϕ is equivalent to a wnfv formula ψ in T means that T |= ϕ ↔ ψ and ψ does not contain other free variables than those of ϕ.

Property 4.3.3 Every formula ϕ is equivalent in T to a wnfv normalized formula of depth d ≥ 1.

Proof

It is easy to transform any formula into a normalized formula, it is enough for example to follow the followings steps:

1. Introduce a supplement of equations and existentially quantified variables to transform the conjunctions of atomic formulas into conjunctions of flat formulas.

2. Replace each sub-formula of the form false by ¬true then express all the quantifiers and logical connectors using only the logical symbols ¬, ∧ and ∃. This can be done using the following transformations 14 of sub-formulas:

(ϕ ∨ φ) =⇒ ¬(¬ϕ ∧ ¬φ), (ϕ → φ) =⇒ ¬(ϕ ∧ ¬φ), (ϕ ↔ φ) =⇒ (¬(ϕ ∧ ¬φ) ∧ ¬(φ ∧ ¬ϕ)), (∀x ϕ) =⇒ ¬(∃x ¬ϕ).
3. If the formula ϕ obtained does not start with the logical symbol ¬, then replace it by ¬(∃ε true ∧ ¬ϕ). 4. Rename the quantified variables so that the obtained formula satisfies the imposed discipline in T (see Section 4.1). 5. Lift the quantifier before the conjunction, i.e. ϕ ∧ (∃x ψ) or (∃x ψ) ∧ ϕ, becomes ∃x ϕ ∧ ψ because the free variables of ϕ are distinct from those of x. 6. Group the quantified variables into a vectorial quantifier, i.e. ∃x(∃ȳ ϕ) or ∃x∃ȳ ϕ becomes ∃xy ϕ. 7. Insert empty vectors and formulas of the form true to get the normalized form using the following transformations of sub-formulas:

¬( i∈I ¬ϕ i ) =⇒ ¬(∃ε true ∧ i∈I ¬ϕ i ), (19)
¬(α ∧ i∈I ¬ϕ i ) =⇒ ¬(∃ε α ∧ i∈I ¬ϕ i ), (20)
¬(∃x

j∈J ¬ϕ j ) =⇒ ¬(∃x true ∧ j∈J ¬ϕ j ). ( 21
)
with α a conjunction of elementary equations, I a finite (possibly empty) set and J a finite non-empty set. 8. Rename the quantified variables so that the obtained normalized formula satisfies the discipline of the formulas in T .

If the starting formula does not contain the logical symbol ↔ then this transformation will be linear, i.e. there exists a constant k such that n 2 ≤ kn 1 , where n 1 is the size of the starting formula and n 2 the size of the normalized formula. We show easily by contradiction that the final formula obtained after application of these steps is normalized.

Example 4.3.4 Let x, v, w, u be variables such that x ≻ v ≻ w ≻ u. Let f be a 2-ary function symbol which belongs to F . Let us apply the preceding steps to transform the following formula into a normalized formula:

(f (u, v) = f (w, u) ∧ (∃x u = x)) ∨ (∃u ∀w u = f (v, w)).
Note that the formula does not start with ¬ and the variables u and w are free in

f (u, v) = f (w, u) ∧ (∃x u = x)
and bound in ∃u ∀w u = f (v, w). Note also that this formula does not respect the discipline of the formulas in T .

Step 1: Let us first transform the equations into flat equations. The preceding formula is equivalent in T to

(∃u 1 u 1 = f (u, v) ∧ u 1 = f (w, u) ∧ (∃x u = x)) ∨ (∃u ∀w u = f (v, w)), (22)
where

u 1 is a variable of V such that u 1 ≻ x ≻ v ≻ w ≻ u.
Step 2: Let us now express the quantifier ∀ using ¬, ∧ and ∃. Thus, the formula ( 22) is equivalent in T to

(∃u 1 u 1 = f (u, v) ∧ u 1 = f (w, u) ∧ (∃x u = x)) ∨ (∃u ¬(∃w ¬(u = f (v, w)))).
Let us also express the logical symbol ∨ using ¬, ∧ and ∃. Thus, the preceding formula is equivalent in T to

¬(¬(∃u 1 u 1 = f (u, v) ∧ u 1 = f (w, u) ∧ (∃x u = x)) ∧ ¬(∃u ¬(∃w ¬(u = f (v, w))))). ( 23
)
Step 3: As the formula starts with ¬, we move to Step 4.

Step 4: The occurrences of the quantified variables u and w in (∃u ¬(∃w ¬(u = f (v, w)))) must be renamed. Thus, the formula ( 23) is equivalent in T to

¬(¬(∃u 1 u 1 = f (u, v)∧u 1 = f (w, u)∧(∃x u = x))∧¬(∃u 2 ¬(∃w 1 ¬(u 2 = f (v, w 1 ))))),
where u 2 and w 1 are variables of V such that

w 1 ≻ u 2 ≻ u 1 ≻ x ≻ v ≻ w ≻ u.
Step 5: By lifting the existential quantifier ∃x, the preceding formula is equivalent in T to

¬(¬(∃u 1 ∃x u 1 = f (u, v) ∧ u 1 = f (w, u) ∧ u = x) ∧ ¬(∃u 2 ¬(∃w 1 ¬(u 2 = f (v, w 1 ))))).
Step 6: Let us group the two quantified variables x and u 1 into a vectorial quantifier. Thus, the preceding formula is equivalent in T to

¬(¬(∃u 1 x u 1 = f (u, v) ∧ u 1 = f (w, u) ∧ u = x) ∧ ¬(∃u 2 ¬(∃w 1 ¬(u 2 = f (v, w 1 ))))).
Step 7: Let us introduce empty vectors of variables and formulas of the form true to get the normalized formula. According to the rule (19), the preceding formula is equivalent in T to

¬ ∃ε true ∧ ¬(∃u 1 x u 1 = f (u, v) ∧ u 1 = f (w, u) ∧ u = x)∧ ¬(∃u 2 ¬(∃w 1 ¬(u 2 = f (v, w 1 )))) ,
which using the rule (20) with

I = ∅ is equivalent in T to ¬ ∃ε true ∧ ¬(∃u 1 x u 1 = f (u, v) ∧ u 1 = f (w, u) ∧ u = x)∧ ¬(∃u 2 ¬(∃w 1 ¬(∃ε u 2 = f (v, w 1 )))) ,
which using the rule ( 21) is equivalent in T to

¬ ∃ε true ∧ ¬(∃u 1 x u 1 = f (u, v) ∧ u 1 = f (w, u) ∧ u = x)∧ ¬(∃u 2 true ∧ ¬(∃w 1 true ∧ ¬(∃ε u 2 = f (v, w 1 )))) .
Step 8: This is a normalized formula of depth 4 which respects the discipline of the formulas in T since

w 1 ≻ u 2 ≻ u 1 ≻ x ≻ v ≻ w ≻ u.

General solved formula

Definition 4.4.1 A general solved formula is a normalized formula of the form

¬(∃x α ∧ n i=1 ¬(∃ȳ i β i )),
with n ≥ 0 and such that:

1. α and all the β i , with i ∈ {1, ..., n}, are solved basic formulas.

2. If α ′ is the conjunction of the equations of α then all the conjunctions α ′ ∧ β i , with i ∈ {1, ..., n}, are solved basic formulas. 3. All the variables of x are reachable in ∃x α. 4. For all i ∈ {1, ..., n}, all the variables of ȳi are reachable in ∃ȳ i β i . 5. If finite(u) is a sub-formula of α then for all i ∈ {1, ..., n}, the formula β i contains either finite(u), or finite(v) where v is a reachable variable from u in α ∧ β i and does not occur in a left hand side of an equation of α ∧ β i . 6. For all i ∈ {1, ..., n}, the formula β i contains at least one atomic formula which does not occur in α.

Example 4.4.2 Let w, v, u 1 , u 2 , u 3 be variables such that w ≻ v ≻ u 1 ≻ u 2 ≻ u 3 . The following formula is not a general solved formula

¬(∃ε finite(w) ∧ ¬(∃v w = v ∧ finite(v))). ( 24
)
This formula satisfies all the conditions of Definition 4.4.1 but it does not satisfy the discipline of the formulas in T . In fact, the variable v is bound in (∃v w = v ∧ finite(v)) and the variable w is free in (∃v w = v ∧finite(v)) and thus we should have v ≻ w and not w ≻ v. Let u 4 be a variable such that

u 4 ≻ w ≻ v ≻ u 1 ≻ u 2 ≻ u 3 . The formula (24) is equivalent in T to ¬(∃ε finite(w) ∧ ¬(∃u 4 w = u 4 ∧ finite(v))).
This formula respects the discipline of the formulas of T but is not a general solved formula since it does not satisfy the first condition of Definition 4.4.1. In fact, w = u 4 ∧ finite(v) is not a solved basic formula since we have u 4 ≻ w.

The following formula is a general solved formula

¬(∃v u 1 = f (v) ∧ v = u 2 ∧ finite(u 2 ) ∧ ¬(∃w u 2 = f (w) ∧ finite(w) ∧ finite(u 3 ))).
Property 4.4.3 Let ϕ be a general solved formula. If ϕ has no free variables then ϕ is the formula ¬(∃ε true) else neither T |= ¬ϕ nor T |= ϕ.

Proof

Let ϕ be a general solved formula of the form

¬(∃x α ∧ i∈I ¬(∃ȳ i β i )), (25)
two cases arise:

(1) If ϕ does not contain free variables, then according to the first and third condition of Definition 4.4.1 and using Property 4.2.9 we get x = ε and α = true. As a consequence, the formula ( 25) is equivalent in T to

¬(∃ε true ∧ i∈I ¬(∃ȳ i β i )), (26)
Since ( 26) has no free variables then each ∃ȳ i β i has no free variables. According to the first and fourth condition of Definition 4.4.1, and using Property 4.2.9 we get: for all i ∈ I: ȳi = ε and β i = true. But according to the last condition of Definition 4.4.1 all the formulas β i should be different from true (since we do not distinguish between α and α ∧ true). Thus, the set I must be empty. As a consequence, ϕ is the formula ¬(∃ε true).

(2) If ϕ contains free variables then it is enough to show that there exist two distinct instantiations ϕ ′ and ϕ ′′ of ϕ by individuals of T r15 such that T r |= ϕ ′ and T r |= ¬ϕ ′′ .

Note first that if I = ∅ then each (∃ȳ i β i ), with i ∈ I, should contain at least one free variable. In fact, if (∃ȳ i β i ), with i ∈ I, does not contain free variables then this formula is of the form (∃ε true) according to the first and fourth point of Definition 4.4.1 and Property 4.2.9, which contradicts the last condition of Definition 4.4.1 (since we do not distinguish between α and α ∧ true). Thus each (∃ȳ i β i ), with i ∈ I, contains at least one free variable that can be instantiated. On the other hand:

Case 1 : If ∃x α contains free variables then we can easily find an instantiation of the free variables of ∃x α which contradicts the constraints of α. In fact, let z be a free variable. Four cases arise:

• If z = w is a sub-formula of α then according to Definition 4.4.1 α is a solved basic formula and thus z ≻ w. As a consequence, w cannot be a quantified variable otherwise the formula ϕ does not respect the discipline of the formulas in T . Thus is enough to instantiate z and w by two distinct values. • If z = f ( w) is a sub-formula of α then it is enough to instantiate z by a tree which starts by a function symbol which is different from f . • If w = z or w = t[z] is a sub-formula of α then according to Definition 4.4.1 all the variables of x are reachable in ∃x α and thus according to the first point of Remark 4.2.8 the equations w = z and w = t[z] are reachable. According to the second point of Remark 4.2.8 the value of z is linked to another free variable v which occurs in a left hand side of an equation of α. This case is already treated in two preceding cases. • If finite(z) is a sub-formula of α then it is enough to instantiate z by an infinite tree.

As a consequence, the instantiated formula of ∃x α will be false in T r and thus T r |= ϕ ′ . On the other hand, by following the same preceding steps and since: (i) the set F contains an infinity of function symbols which are not constants, (ii) T r contains an infinity of individuals u of T r such that T r |= finite T r (u), (iii) ϕ is a general solved formula, then we show that there exists at least one instantiation which satisfies all the constraints of α and contradicts the constraints of each β i , with i ∈ I. In fact, (iv) in order to contradicts each constraint β i , it is enough to follow the preceding discussion (by replacing α by β i ) and use (i) and (ii). On the other hand, according to Definition 4.4.1 all the variables of x are reachable in ∃x α, thus according to the first point of remark 4.2.8 all the equations and relations of α are reachable in ∃x α. According to the second point of remark 4.2.8 the values of the free variables which occur in these formulas are mainly linked to those of free variables which occur in left hand side of equations of α. According to the two first conditions of Definition 4.4.1, the variables of Lhs(α) are distinct and do not occur in F IN I(α), Lhs(β i ) and F IN I(β i ) for all i ∈ {1, ..., n}. As a consequence, from (iv) and using (i), (ii) and (iii) there exists at least one instantiation which satisfies ∃x α and contradicts each ∃ȳ i β i in T r, with i ∈ I and thus T r |= ¬ϕ ′′ . Note that if I = ∅ then we have also T r |= ¬ϕ ′′ and T r |= ϕ ′ using the preceding instantiations.

Case 2 : If ∃x α does not contain free variables then according to the first and third condition of Definition 4.4.1 and Property 4.2.9 we have x = ε and α = true. Since ϕ contains at least one free variable then I = ∅. Let k ∈ I. Since:

(i) the set F contains an infinity of function symbols which are not constants, (ii) T r contains an infinity of individuals u of T r such that T r |= finite T r (u), (iii) ϕ is a general solved formula, then we can easily find an instantiation of the free variables of ∃ȳ k β k which satisfies the constraints of β k (similar to the second part of Case 1 by replacing α by β k ). Such an instantiation makes false the instantiated formula ¬(∃ȳ k β k ) in T r and thus T r |= ϕ ′ . On the other hand, according to (i), (ii) and (iii), we show that there exists at least one instantiation which contradicts the constraints of each β i , with i ∈ I (similar to the second part of Case 1 with α = true and x = ε). As a consequence, this instantiation satisfies all the ¬(∃ȳ i β i ) in T r, with i ∈ I and thus T r |= ¬ϕ ′′ .

From Case 1 and Case 2, we have T r |= ϕ ′ and T r |= ¬ϕ ′′ , and thus neither T |= ϕ nor T |= ¬ϕ.

Example 4.4.4

Let v 1 , v 2 , v, u and w be variables such that v 1 ≻ v 2 ≻ v ≻ u ≻ w. Let ϕ be the following general solved formula

¬(∃v u = g(v, w) ∧ ¬(∃v 1 v = g(v, v 1 ) ∧ v 1 = f (v)) ∧ ¬(∃v 2 w = g(w, v 2 ) ∧ v 2 = f (w))
(27) Let us consider for example the model T r of finite or infinite trees. If we instantiate the free variable u by the finite tree 1 where 1 is a constant in F which is distinct from g then according to axiom [1] of conflict of symbols, the instantiated formula of ( 27) is true in T r. On the other hand, if u is instantiated by a tree of the form g(v * , w * ) with v * = g(v * , f (v * )) (for example v * = 1) and w * = g(w * , f (w * )) (for example w * = 1) then the instantiated formula of ( 27) is false in T r. As a consequence ( 27) is neither true nor false in the theory T . The reader should not think that the fact that we have neither T |= ¬ϕ nor T |= ϕ means that ϕ is unsatisfiable in T . This is of course false. In fact, since neither T |= ¬ϕ nor T |= ϕ then ϕ has in each model M of T a set of solutions which make it true in M and another set of non-solutions which make it false in M. We also remind the reader that all the properties given after Section 4.1 hold only for formulas that respect the discipline of the formulas of T .

A similar property has been shown for the finite trees of J. Lassez [START_REF] Lassez | Explicit representation of terms defined by counter examples[END_REF] and the rational trees of M. Maher [START_REF] Maher | On inductive inference of cyclic structures[END_REF]. M. Maher in [START_REF] Maher | On inductive inference of cyclic structures[END_REF] has also shown that if the set F is finite and contains at least one n-ary function symbol with n ≥ 2, then the problem of deciding if a formula containing equations and the logical symbols ∧, ∨, ¬ is equivalent to a disjunction of conjunctions of equations is a co-NP-complete problem, and the problem of deciding if an expression represents a nonempty set of rational trees is NP-complete. Note also that in all our proofs we have not used the famous independence of inequations [START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF][START_REF] Lassez | Unification revisited[END_REF][START_REF] Comon | Unification et disunification : Theorie et applications[END_REF]Lassez and McAloon 1986) but only the condition that the signature of T is infinite and contains an infinity of function symbols which are not constants and at least one symbol which is a constant, which implies in this case the independence of the inequations.

Property 4.4.5 Every general solved formula of the form ¬(∃x α ∧ n i=1 ¬(∃ȳ i β i )) is equivalent in T to the following Boolean combination of existentially quantified basic formulas:

(¬(∃x α)) ∨ n i=1 (∃xȳ i α ∧ β i ). Proof Let ¬(∃x α ∧ n i=1 ¬(∃ȳ i β i )), (28)
be a general solved formula. According to the third point of Definition 4.4.1, all the variables of x are reachable in ∃x α. Thus, according to Property 4.2.10, we have T |= ∃?x α. According to Property 3.1.10, the formula ( 28) is equivalent in T to

¬((∃x α) ∧ n i=1 ¬(∃x α ∧ (∃ȳ i β i ))), i.e. to (¬(∃x α)) ∨ n i=1 (∃x α ∧ (∃ȳ i β i )),
which, since the quantified variables have distinct names and different from those of the free variables, is equivalent in T to

(¬(∃x α)) ∨ n i=1 (∃xȳ α ∧ β i ),
which is a Boolean combination of existentially quantified basic formulas.

Definition 4.4.6

Let ϕ be a formula of the form

∃x α ∧ n i=1 ¬(∃ȳ i β i ), (29)
with x and ȳ two vectors of variables, n ≥ 0 and α and the β i , with i ∈ {1, ..., n}, basic formulas. We say that ϕ is written in an explicit solved form if and only if the formula ¬ϕ, i.e.

¬(∃x α ∧ n i=1 ¬(∃ȳ i β i )), (30)
is a general solved formula.

This definition shows how to easily extract from a general solved formula, a simple formula ϕ which has only one level of negation and where the solutions of the free variables are given in clear and explicit way, i.e. for each model M of T , it is easy to find all the possible instantiations of the free variables of ϕ which make it true in M. In fact, according to Definition 4.4.1, we warrant among other things that the left hand sides of the equations of α are distinct and do not occur in those of each β i , the left hand sides of the equations of each β i are distinct and we cannot eliminate any quantification since all the variables are reachable.

Example 4.4.7 Let w, v, u 1 , u 2 , u 3 be variables such that w ≻ v ≻ u 1 ≻ u 2 ≻ u 3 . Let ϕ be the following general solved formula

¬(∃v u 1 = f (v) ∧ v = u 2 ∧ finite(u 2 ) ∧ ¬(∃w u 2 = f (w) ∧ finite(w) ∧ finite(u 3 ))).
According to Definition 4.4.6, the following formula φ is written in an explicit solved form:

∃v u 1 = f (v) ∧ v = u 2 ∧ finite(u 2 ) ∧ ¬(∃w u 2 = f (w) ∧ finite(w) ∧ finite(u 3 )). ( 31
)
Let us chose the model T r of finite or infinite trees and let us give all the possible instantiations u * 1 , u * 2 , u * 3 of the free variables u 1 , u 2 , u 3 so that the instantiated formula of φ is true in the model T r. From (31) it is clear that we have two possibilities:

• Solution 1:

-u * 3 is any infinite tree. -u * 2 is any finite tree. -u * 1 is the tree f (u * 2 ).
• Solution 2:

u * 3 is any finite tree. -u * 2 is any finite tree which starts by a function symbol which is different from f . -u * 1 is the tree f (u * 2 ).

Working formula

Definition 4.5.1 A working formula is a normalized formula in which all the occurrences of ¬ are replaced by ¬ k with k ∈ {0, ..., 5} and such that each occurrence of a sub-formula of the form

p = ¬ k (∃x α ∧ q), with k > 0, (32)
satisfies the k first conditions of the condition list bellow. In (32) α is a basic formula, q is a conjunction of working formulas of the form n i=1 ¬ ki (∃ȳ i β i ∧ q i ), with n ≥ 0, β i a basic formula, q i a conjunction of working formulas, and in the below condition list α ′ is the basic formula of the immediate top-working formula16 p ′ of p if it exists.

1. If p ′ exists then T |= α → α ′ and T |= α eq → α ′ eq where α eq and α ′ eq are the conjunctions of the equations of α respectively α ′ . Moreover, the set of the variables of Lhs(α ′ ) ∪ F IN I(α ′ ) is included in those of Lhs(α) ∪ F IN I(α). 2. The left hand sides of the equations of α are distinct and for all equations of the form u = v we have u ≻ v. 3. α is a basic solved formula. 4. If p ′ exists then the set of the equations of α ′ is included in those of α. 5. The variables of x, the equations of α and the constraints of the form finite(x) of α are reachable in ∃x α. Moreover, if n > 0 then for all i ∈ {1, ..., n} the conjunction β i contains at least one atomic formula which does not occur in α.

The intuitions behind these working formulas come from an aim to have a full control on the execution of our rewriting rules by adding semantic informations on a syntactic form of formulas. We emphasize strongly that ¬ k does not mean that the normalized formula satisfies only the k th condition but all the conditions i with 1 ≤ i ≤ k.

Example 4.5.2 Let w 1 , w 2 , w 3 , v 1 , u be variables such that w 1 ≻ w 2 ≻ w 3 ≻ v 1 ≻ u. This is a working formula of depth 2:

¬ 2   ∃v 1 u = f (v 1 ) ∧ finite(u) ∧   ¬ 2 (∃w 1 u = f (w 1 ) ∧ w 1 = v 1 ∧ finite(u))∧ ¬ 3 (∃w 2 u = f (v 1 ) ∧ w 2 = f (v 1 ) ∧ finite(v 1 ))∧ ¬ 4 (∃w 3 u = f (v 1 ) ∧ v 1 = f (w 3 ) ∧ finite(w 3 ))     Definition 4.5.3
An initial working formula is a working formula which begins with ¬ 4 and such that k = 0 for all the other occurrences of ¬ k . A final working formula is a working formula of depth less or equal to 2 with k = 5 for all the occurrences of ¬ k .

The relation between the final working formulas and the general solved formulas is expressed in the following property: Property 4.5.4 Let p be the following final working formula

¬ 5 (∃x α ∧ n i=1 ¬ 5 (∃ȳ i β i )).
The formula

¬(∃x α ∧ n i=1 ¬(∃ȳ i β * i )),
is a general solved formula equivalent to p in T where β * i is the basic formula β i from which we have removed all the equations which occur also in α.

Example 4.5.5 Let w 2 , v, u and u 1 be variables such that w 2 ≻ v ≻ u ≻ u 1 . Let ϕ be the following final working formula

¬ 5   ∃ε v = u ∧ finite(u)∧ ¬ 5 (∃ε v = u ∧ u = u 1 ∧ finite(u 1 ))∧ ¬ 5 (∃w 2 v = u ∧ u = s(w 2 ) ∧ finite(w 2 ))   . The formula ¬   ∃ε v = u ∧ finite(u)∧ ¬(∃ε u = u 1 ∧ finite(u 1 ))∧ ¬(∃w 2 u = s(w 2 ) ∧ finite(w 2 ))   .
is a general solved formula equivalent to ϕ in T .

Rewriting rules

We now present the rewriting rules which transform an initial working formula of any depth d into an equivalent conjunction of final working formulas. To apply the rule p 1 =⇒ p 2 to the working formula p means to replace in p a sub-formula p 1 by the formula p 2 , by considering that the connector ∧ is associative and commutative. In the following, the letters u, v and w represent variables, the letters x, ȳ and z represent vectors of variables, the letters a, b and c represent basic formulas, the letter q represents a conjunction of working formulas, the letter r represents a conjunction of flat equations, formulas of the form finite(x) and working formulas. All these letters can be subscripted or have primes.

(1)

¬ 1 (∃x u = u ∧ r) =⇒ ¬ 1 (∃x r) (2) ¬ 1 (∃x v = u ∧ r) =⇒ ¬ 1 (∃x u = v ∧ r) (3) ¬ 1 (∃x u = v ∧ u = t ∧ r) =⇒ ¬ 1 (∃x u = v ∧ v = t ∧ r) (4) ¬ 1 (∃x u = f v1...vn ∧ u = gw1...wm ∧ r) =⇒ true (5) ¬ 1 (∃x u = f v1...vn ∧ u = f w1...wn ∧ r) =⇒ ¬ 1 (∃x u = f v1...vn ∧ n i=1 vi = wi ∧ r) (6) ¬ 1 (∃x a ∧ q) =⇒ ¬ 2 (∃x a ∧ q) (7) ¬ 2 (∃x finite(u) ∧ finite(u) ∧ r) =⇒ ¬ 2 (∃x finite(u) ∧ r) (8) ¬ 2 (∃x u = v ∧ finite(u) ∧ r) =⇒ ¬ 2 (∃x u = v ∧ finite(v) ∧ r) (9) ¬ 2 (∃x finite(u) ∧ a ∧ q) =⇒ true (10) ¬ 2 (∃x u = f (v1, ..., vn) ∧ finite(u) ∧ r) =⇒ ¬ 2 (∃x u = f (v1, ..., vn) ∧ n i=1 finite(vi) ∧ r) (11) ¬ 2 (∃x a ∧ q) =⇒ ¬ 3 (∃x a ∧ q) (12) ¬ 4 (∃x a ∧ q ∧ ¬ 0 (∃ȳ r)) =⇒ ¬ 4 (∃x a ∧ q ∧ ¬ 1 (∃ȳ a ∧ r)) (13) ¬ 4 (∃x a ∧ a ′ ∧ q ∧ ¬ 3 (∃ȳ a ′′ ∧ r)) =⇒ ¬ 4 (∃x a ∧ a ′ ∧ q ∧ ¬ 4 (∃ȳ a ∧ r)) (14) ¬ 4 (∃x a ∧ q ∧ ¬ 5 (∃ȳ a)) =⇒ true (15) ¬ 4 (∃x a ∧ n i=1 ¬ 5 (∃ȳi bi)) =⇒ ¬ 5 (∃x ′ a ′ ∧ i∈K ¬ 5 (∃ȳ ′ i b ′ i ) * ) (16) ¬ 4     ∃x a ∧ q∧ ¬ 5 ∃ȳ b∧ n i=1 ¬ 5 (∃zi ci)     =⇒ ¬ 4 (∃x a ∧ q ∧ ¬ 5 (∃ȳ b))∧ n i=1 ¬ 4 (∃xȳzi ci ∧ q0) *
with u ≻ v, f and g two distinct function symbols taken from F . In rule (3), t is a flat term, i.e. either a variable or a term of the form f (x 1 , ..., x n ) with f an n-ary function symbol taken from F . In rule ( 6), the equations of a have distinct left hand sides and for each equation of the form u = v we have u ≻ v. In rule (9), the variable u is reachable from u in a. In rule (10), the variable u is non-reachable from u in a. Moreover, if f is a constant then n = 0. In rule (11), a is a solved basic formula. In rule (13), a and a ′′ are conjunctions of equations having the same left hand sides and a ′ is a conjunction of formulas of the form finite(u). In rule (15), n ≥ 0 and for all i ∈ {1, ..., n} the formula b i is different from the formula a. The pairs (x ′ , a ′ ) and (ȳ ′ i , b ′ i ) are obtained by a decomposition of x and a into x′ x′′ x′′′ and a ′ ∧ a ′′ ∧ a ′′′ as follows:

• a ′ is the conjunction of the equations and the formulas of the form finite(x) which are reachable in ∃x a. • x′ is the vector the variables of x which are reachable in ∃x a.

• a ′′ is the conjunction of the formulas of the form finite(x) which are nonreachable in ∃x a. • x′′ is the vector the variables of x which are non-reachable in ∃x a and do not occur in the left hand sides of the equations of a. • a ′′′ is the conjunction of the equations which are non-reachable in ∃x a.

• x′′′ is the vector the variables of x which are non-reachable in ∃x a and occur in the left hand sides of the equations of a.

′ i . • The formula i∈K ¬ 5 (∃ȳ ′ i b ′ i ) * is the formula i∈K ¬ 5 (∃ȳ ′ i b ′ i
) in which we have renamed the quantified variables so that they satisfy the discipline of the formulas in T .

In rule ( 16), n > 0 and q 0 is the formula q in which all the occurrences of ¬ k have been replaced by ¬ 0 . The formula n i=1 ¬ 4 (∃xȳz i c i ∧ q 0 ) * is the formula n i=1 ¬ 4 (∃xȳz i c i ∧ q 0 ) in which we have renamed the quantified variables so that they satisfy the discipline of the formulas of T .

The use of indices on the negations of the working formulas enables us to force the application of the rules to follow a clear strategy until reaching a conjunction of final working formulas. In fact, the algorithm follows two main steps while solving any first-order constraint in T :

• (i) A top-down propagation of basic formulas following the tree structure of the working formulas and using the rules (1),...,(13). In this step, basic formulas are solved and copied in all sub-working formulas. Finiteness is also check and inconsistent basic formulas are removed by the rules (4) and ( 9). • (ii) A bottom-up elimination of quantifiers and depth reducing of the working formulas using the rules ( 14),...,( 16). Inconsistent working formulas are also removed in this step.

More precisely, starting from an initial working formula ϕ of the form ¬ 4 (∃x a ∧ i∈I q i ), where all the q i are working formulas whose negations are of the form ¬ 0 , rule (12) propagates the atomic formulas of a into a sub-formula q i , with i ∈ I, and changes the first negation of q i into ¬ 1 . The rules (1),...,(5) can now be applied until the equations of a have distinct left hand sides and for each equation of the form u = v we have u ≻ v. Rule ( 6) is then applied and changes the first negation of q i into ¬ 2 . The algorithm starts now a new phase which consists in solving the basic formulas using the rules (7),..., (10). In particular finiteness is checked by rule (9). When a solved basic formula is obtained, rule ( 11) is applied and changes the negation into ¬ 3 . Note that if a working formula starts by ¬ 3 then its top working formula starts by ¬ 4 . Rule ( 13) is then applied. It restores some equations and changes the first negation into ¬ 4 . Rule ( 12) can now be applied again since all the nested negations are of the form ¬ 0 and so on. This is the first step of our algorithm. Once the sub-working formulas of depth 1 are of the form ¬ 4 (∃ȳ i b i ), the second step starts using rule ( 15) with n = 0 on all these sub-working-formulas of depth 1 and transforms their negations into ¬ 5 . Inconsistent working formulas of the form ¬ 4 (∃x α ∧ ¬ 5 (∃ȳ α) ∧ q) are then removed by rule ( 14). When all the inconsistent working formulas have been removed, rule ( 15) with n = 0 can be applied on the sub-working-formulas of depth 2 of the form ¬ 4 (∃x a ∧ i∈I ¬ 5 (∃ȳ i b i )) and produces working formulas of the form ¬ 5 (∃x a ∧ i∈I ¬ 5 (∃ȳ i b i )). Rule ( 16) can now be applied on the working formulas of depth d > 2 of the form ¬ 4 (∃x a ∧ q ∧ ¬ 5 (∃ȳ b∧ n i=1 ¬ 5 (∃z i c i ))). After each application of this rule, new working formulas containing negations of the form ¬ 0 are created which implies the execution of the rules of the first step of our algorithm, starting by rule ( 12) and so on. After several applications of our rules, we get a conjunction of working formulas whose depth is less or equal to 2. The rules are then applied again until all the negations of these working formulas are of the form ¬ 5 . It is a conjunction of final working formulas.

Example 4.6.1 Let f and g be two function symbols taken from F of respective arities 2, 1. Let

w 1 , w 2 , v 1 , u 1 , u 2 , u 3 be variables such that w 1 ≻ w 2 ≻ v 1 ≻ u 1 ≻ u 2 ≻ u 3 .
Let us run our rules on the following initial working formula

¬ 4   ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 0 (∃w 1 v 1 = g(w 1 ))∧ ¬ 0 (∃w 2 u 2 = g(w 2 ) ∧ w 2 = g(u 3 ) ∧ finite(w 2 ))   . ( 33
)
According to rule (12), the preceding formula is equivalent in T to

¬ 4   ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 1 (∃w 1 v 1 = g(w 1 ) ∧ v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 ))∧ ¬ 0 (∃w 2 u 2 = g(w 2 ) ∧ w 2 = g(u 3 ) ∧ finite(w 2 ))   .
The application of rule (4) on the sub formula ¬ 1 (∃w

1 v 1 = g(w 1 ) ∧ v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 ) ∧ finite(w 2 )
) simplifies this sub formula into the formula true. Thus, the preceding formula is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 0 (∃w 2 u 2 = g(w 2 ) ∧ w 2 = g(u 3 ) ∧ finite(w 2 )) ,
which according to rule ( 12) is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 0 (∃w 2 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 ) ∧ u 2 = g(w 2 ) ∧ w 2 = g(u 3 ) ∧ finite(w 2 )) .
Rule (5) can now be applied. Thus, the preceding formula is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 1 (∃w 2 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(w 2 ) ∧ w 2 = u 1 ∧ w 2 = g(u 3 ) ∧ finite(w 2 )) ,
which according to rule (3) is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 1 (∃w 2 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(w 2 ) ∧ w 2 = u 1 ∧ u 1 = g(u 3 ) ∧ finite(w 2 )) .
Since the conjunction of equations of the sub-formula which starts by ¬ 1 has distinct left hand sides and w 2 ≻ u 1 , then rule ( 6) can be applied. Thus, the preceding formula is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 2 (∃w 2 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(w 2 ) ∧ w 2 = u 1 ∧ u 1 = g(u 3 ) ∧ finite(w 2 )) ,
which according to rule ( 8) is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 2 (∃w 2 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(w 2 ) ∧ w 2 = u 1 ∧ u 1 = g(u 3 ) ∧ finite(u 1 )) ,
which according to rule ( 10) is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 2 (∃w 2 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(w 2 ) ∧ w 2 = u 1 ∧ u 1 = g(u 3 ) ∧ finite(u 3 )) .
Since the basic formulas are solved then rule (11) can be applied. Thus, the preceding formula is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 3 (∃w 2 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(w 2 ) ∧ w 2 = u 1 ∧ u 1 = g(u 3 ) ∧ finite(u 3 )) ,
which according to rule ( 13) is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 4 (∃w 2 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 ) ∧ w 2 = u 1 ∧ u 1 = g(u 3 ) ∧ finite(u 3 )) .
Rule (15) can now be applied with n = 0. Thus, the preceding formula is equivalent in T to

¬ 4 ∃v 1 v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 )∧ ¬ 5 (∃ε v 1 = f (u 1 , u 2 ) ∧ u 2 = g(u 1 ) ∧ u 1 = g(u 3 ) ∧ finite(u 3 )) .
Once again rule (15) can be applied, with n = 0 and we get the following final working formula

¬ 5 ∃ε u 2 = g(u 1 )∧ ¬ 5 (∃ε u 2 = g(u 1 ) ∧ u 1 = g(u 3 ) ∧ finite(u 3 )) ,
which according to Property 4.5.4 is equivalent in T to the following general solved formula

¬ u 2 = g(u 1 )∧ ¬(u 1 = g(u 3 ) ∧ finite(u 3 )) .
We have seen in the preceding example how the rules (1),...,(15) can be applied.

Let us now see how rule ( 16) is applied.

Example 4.6.2 Let s and 0 be two function symbols taken from F of respective arities 1, 0. Let w 1 , w 2 , u, v be variables such that w 1 ≻ w 2 ≻ v ≻ u. Let us apply our rules on the following working formula of depth 3:

¬ 4   ∃ε true ∧   ¬ 5 (∃ε u = s(v))∧ ¬ 5 (∃w 1 u = s(w 1 ) ∧ w 1 = s(v))∧ ¬ 5 (∃ε v = u ∧ ¬ 5 (∃ε v = u ∧ u = 0) ∧ ¬ 5 (∃w 2 v = u ∧ u = s(w 2 )))     .
By considering that

• (∃x a) = (∃εtrue)

• q = ¬ 5 (∃ε u = s(v))∧ ¬ 5 (∃w 1 u = s(w 1 ) ∧ w 1 = s(v)) • (∃ȳ b) = (∃ε v = u) • n i=1 ¬ 5 (∃z i c i ) = ¬ 5 (∃ε v = u ∧ u = 0)∧ ¬ 5 (∃w 2 v = u ∧ u = s(w 2 ))
rule ( 16) can be applied and produces the following formula

  ¬ 4 (∃ε true ∧ ¬ 5 (∃ε u = s(v)) ∧ ¬ 5 (∃w 1 u = s(w 1 ) ∧ w 1 = s(v)) ∧ ¬ 5 (∃ε v = u))∧ ¬ 4 (∃ε v = u ∧ u = 0 ∧ ¬ 0 (u = s(v)) ∧ ¬ 0 (∃w 11 u = s(w 11 ) ∧ w 11 = s(v)))∧ ¬ 4 (∃w 2 v = u ∧ u = s(w 2 ) ∧ ¬ 0 (∃ε u = s(v)) ∧ ¬ 0 (∃w 12 u = s(w 12 ) ∧ w 12 = s(v)))   ,
where w 11 and w 12 are variables such that w 11 ≻ w 12 ≻ w 1 ≻ w 2 ≻ v ≻ u. Now, only the rules (1),...,(15) will be applied until all the negations are of the form ¬ 5 . Rule (16) will not be applied anymore since there exists no working formulas of depth greater or equal to 3 and the rules (1),...,(15) never increase the depth of the working formulas.

Property 4.6.3 Every repeated application of the preceding rewriting rules on an initial working formula p is terminating and producing a wnfv conjunction of final working formulas equivalent to p in T .

Proof

Proof, first part: The application of the rewriting rules terminates. Let us introduce the function α : q → n, where q is a conjunction of working formulas, n an integer and such that

• α(true) = 0, • α(¬(∃x a ∧ ϕ)) = 2 α(ϕ) , • α( i∈I ϕ i ) = i∈I α(ϕ i ),
with a a basic formula, ϕ a conjunction of working formulas and the ϕ i 's working formulas. Note that if α(p 2 ) < α(p 1 ) then α(p[p 2 ]) < α(p) where p[p 2 ] is the formula obtained from p when we replace the occurrence of the formula p 1 in p by p 2 . This function has been introduced in [START_REF] Vorobyov | An Improved Lower Bound for the Elementary Theories of Trees[END_REF] and [START_REF] Colmerauer | Expressiveness of full first-order formulas in the algebra of finite or infinite trees[END_REF] to show the non-elementary complexity of all algorithms solving propositions in the theory of finite or infinite trees. It has also the property to decrease if the depth of the working formula decreases after application of distributions as it is done in our rule ( 16).

Let us introduce also the function λ : (u, a) → n, where u is a variable, a a basic formula, n an integer and such that

λ(u, a) =             0,
if the conjunction of the equations of a has not distinct left hand sides or contains a sub-formula of the form x = y with y ≻ x, else 1, if u does not occur in a left hand side of an equation of a, or u is reachable from u in a, else

1 + λ(v, a), if the equation u = v is in a, else 2 + n i=1 λ(v i , a), if the equation u = f (v 1 , ..., v n ) is in a.            
Since the variables which occur in our formulas are ordered by the order relation " ≻ ", we can number them by positive integers such that

x ≻ y ↔ no(x) > no(y),
where no(x) is the number associated to the variable x. Let us consider the 10tuple (n 1 , n 2 , n 3 , n 4 , n 5 , n 6 , n 7 , n 8 , n 9 , n 10 ) where the n i 's are the following positive integers:

• n 1 = α(p),

• n 2 is the number of ¬ 0 ,

• n 3 is the number of ¬ 1 ,

• n 4 is the number of occurrences of function symbols in sub-formulas of the form ¬ 1 (...). For example, if we have

¬ 1 (∃x x = f (y) ∧ y = f (x) ∧ x = g(x, w) ∧ y = f (y))
then n 4 = 4. • n 5 is the sum of all the no(x) for each occurrence of a variable x in a basic formula of a sub-formula of the form ¬ 1 (...). For example, if we have

¬ 1 (∃w x = f (x, z)∧y = x ∧ finite(z) ∧ ...) then n 5 = no(x) + no(x) + no(z) + no(y) + no(x) + no(z) + .... • n 6 is the number of formulas of the form v = u with u ≻ v in sub-formulas of the form ¬ 1 (...), • n 7 is the number of ¬ 2 ,
• n 8 is the sum of all the λ(u, a) for each occurrence of a sub-formula finite(u) in a basic-formula a of a working formula of the form ¬ 2 (∃x a ∧ q). For example, if we have

¬ 2 (∃z x = f (x, z) ∧ z = f (y, y) ∧ finite(x) ∧ finite(x) ∧ finite(z)) then n 8 = λ(x, a) + λ(x, a) + λ(z, a) = 1 + 1 + (2 + 1 + 1) where a is the basic formula x = f (x, z) ∧ z = f (y, y) ∧ finite(x) ∧ finite(x) ∧ finite(z). • n 9 is the number of ¬ 3 • n 10 is the number of ¬ 4 .
For each rule, there exists a positive integer i such that the application of this rule decreases or does not change the values of the n j 's, with 1 ≤ j < i, and decreases the value of n i . These i are equal to: 1 for the rules (4), ( 9), ( 14) and ( 16), 2 for rule (12), 3 for rule (6), 4 for rule (5), 5 for the rules (1), ( 3), ( 7) and ( 8) , 6 for rule (2), 7 for rule (11), 8 for rule (10), 9 for rule (13), and 10 for rule (15). To each sequence of formulas obtained by a finite application of the preceding rewriting rules, we can associate a series of 10-tuples (n 1 , n 2 , n 3 , n 4 , n 5 , n 6 , n 7 , n 8 , n 9 , n 10 ) which is strictly decreasing in the lexicographic order. Since the n i 's are positive integers, they cannot be negative, thus, this series of 10-tuples is a finite series and the application of the rewriting rules terminates.

Proof, second part: Let us now show that for each rule of the form p =⇒ p ′ we have T |= p ↔ p ′ and the formula p ′ remains a conjunction of working formula.

Correctness of the rules (1),...,(14)

The rules (1),...( 5) are correct according to the axioms [1] and [2] of T . Rules ( 6) and ( 11) are evident. The rules ( 7) and ( 8) are true in the empty theory and thus true in T . In rule (9), the variable u is reachable from itself in a, i.e. the basic formula a contains a sub-formula of the form

u = t 1 ∧ u 2 = t 2 ∧ ... ∧ u n = t n (34)
where u i occurs in the term t i-1 for all i ∈ {2, ..., n} and u occurs in t n . According to Definition 4.5.1, since our working formula starts with ¬ 2 then all the equations of a have distinct lef hand sides and for all equations of the form x = y we have x ≻ y. Thus, there exists at least one equation in (34) which contains a function symbol which is not a constant, otherwise (34) is of the form u = u 2 ∧ u 2 = u 3 ∧ ... ∧ u n = u which implies u ≻ u 2 ≻ ... ≻ u, i.e. u ≻ u which is false since the order ≻ is strict. Thus, according to the fourth axiom of T we have T |= a → ¬finite(u).

As a consequence, rule (9) is correct in T . Rule (10) is correct according to the last axiom of T . Rule ( 13) is correct according to Property 4.2.4 and Definition 4.5.1. The rules ( 12) and ( 14) are true in the empty theory and thus true in T . Note that according to Property 4.2.5, two solved basic formulas having the same equations are equivalent if and only if they have the same relations finite(x). This is why in Definition 4.5.1 of the working formulas (more precisely in condition 4) we force only the equations to be included in the sub-forworking formulas and use the elementary rule ( 14) to remove inconsistent working formulas of depth 2.

Correctness of rule ( 15)

¬ 4 (∃x a ∧ n i=1 ¬ 5 (∃ȳ i b i )) =⇒ ¬ 5 (∃x ′ a ′ ∧ i∈K ¬ 5 (∃ȳ ′ i b ′ i ) * )
with n ≥ 0, and for all i ∈ {1, ..., n} the formula b i is different from the formula a. The pairs (x ′ , a ′ ) and (ȳ ′ i , b ′ i ) are obtained by a decomposition of x and a into x′ x′′ x′′′ and a ′ ∧ a ′′ ∧ a ′′′ as follows:

• a ′ is the conjunction of the equations and the formulas of the form finite(x) which are reachable in ∃x a.

• x′ is the vector the variables of x which are reachable in ∃x a.

• a ′′ is the conjunction of the formulas of the form finite(x) which are non-reachable in ∃x a. • x′′ is the vector the variables of x which are non-reachable in ∃x a and do not occur in the left hand sides of the equations of a. • a ′′′ is the conjunction of the equations which are non-reachable in ∃x a.

• x′′′ is the vector the variables of x which are non-reachable in ∃x a and occur in the left hand sides of the equations of a. • b * i is the formula obtained by removing from b i the formulas of the form finite(u) which occur also in a ′′ • ȳ′ i is the vector of the variables of ȳi x′′′ which are reachable in

∃ȳ i x′′′ b * i . • b ′
i is the conjunction of the equations and the formulas of the form finite(x) which are reachable in

∃ȳ i x′′′ b * i . • K ⊆ {1, ..., n} is the set of the indices i such that i ∈ K if and only if no variable of x′′ occurs in b ′ i . • The formula i∈K ¬ 5 (∃ȳ ′ i b ′ i ) * is the formula i∈K ¬ 5 (∃ȳ ′ i b ′ i
) in which we have renamed the quantified variables so that they satisfy the discipline of the formulas in T .

Let x′ , x′′ , x′′′ , ȳ′ and a ′ , a ′′ , a ′′′ , b * i , b ′ i be the vector of variables and the basic formulas defined above. According to Definition 4.2.6, (i) all the variables of x′′ and x′′′ do not occur in a ′ , otherwise they are reachable in ∃x a. On the other hand, since the first negation in the left hand side of rule ( 15) is of the form ¬ 4 then according to Definition 4.5.1 (ii) a is a solved basic formula and thus x′′′ is the vector of the left hand sides of the equations of a ′′′ and its variables do not occur in a ′′ . Thus, according to (i) and (ii) the left hand side of rule ( 15) is equivalent in

T to ¬(∃x ′ a ′ ∧ (∃x ′′ a ′′ ∧ (∃x ′′′ a ′′′ ∧ n i=1 ¬(∃ȳ i b i )))).
Since a is a solved basic formula then a ′′′ is a solved basic formula which contains only equations and thus according to Property 4.2.3 we have T |= ∃!x ′′′ a ′′′ . Thus, according to Property 3.1.11 the preceding formula is equivalent in T to

¬(∃x ′ a ′ ∧ (∃x ′′ a ′′ ∧ n i=1 ¬(∃x ′′′ a ′′′ ∧ (∃ȳ i b i )))),
which, according to the discipline of the formulas in T (the quantified variables have distinct names and different from those of the free variables ), is equivalent in

T to ¬(∃x ′ a ′ ∧ (∃x ′′ a ′′ ∧ n i=1 ¬(∃x ′′′ ȳi a ′′′ ∧ b i ))). ( 35
)
Since all the nested negations in the left hand side of rule (15) are of the form ¬ 5 then according to Definition 4.5.1, for all i ∈ {1, ..., n}, the set of the equations of a is included in those of b i . As a consequence, the formula ( 35) is equivalent in T to

¬(∃x ′ a ′ ∧ (∃x ′′ a ′′ ∧ n i=1 ¬(∃x ′′′ ȳi b i ))), i.e. to ¬(∃x ′ a ′ ∧ (∃x ′′ a ′′ ∧ n i=1 ¬(∃x ′′′ ȳi b * i ))).
Since all the nested negations in the left hand side of rule ( 15) are of the form ¬ 5 , then according to Definition 4.5.1, for all i ∈ {1, ..., n}, b * i is a solved basic formula. Thus, according to Property 4.2.11, the preceding formula is equivalent in T to

¬(∃x ′ a ′ ∧ (∃x ′′ a ′′ ∧ n i=1 ¬(∃ȳ ′ i b ′ i ))), which is equivalent in T to ¬(∃x ′ a ′ ∧ ( i∈K ¬(∃ȳ ′ i b ′ i )) ∧ (∃x ′′ a ′′ ∧ i∈{1,...,n}-K ¬(∃ȳ ′ i b ′ i ))),
where K ⊆ {1, ..., n} is the set of the indices i such that i ∈ K if and only if no variable of x′′ occurs in b ′ i . Since all the nested negations in the left hand side of rule (15) are of the form ¬ 5 then according to Definition 4.5.1, for all i ∈ {1, ..., n} -K, the variables of ȳ′ i are reachable in ∃ȳ ′ i b ′ i and the formula b ′ i is a solved basic formula. Moreover, since each b ′ i does not contain sub-formulas of the form finite(x) which occur also in a ′′ (see the construction of b * i ), then the formula ∃x ′′ a ′′ ∧ i∈{1,...,n}-K ¬(∃ȳ ′ b ′ i ) satisfies the conditions of Property 4.2.13. As a consequence, according to Property 4.2.13 the preceding formula is equivalent in T to

¬(∃x ′ a ′ ∧ i∈K ¬(∃ȳ ′ i b ′ i )), i.e. to ¬(∃x ′ a ′ ∧ i∈K ¬(∃ȳ ′ i b ′ i ) * ), where i∈K ¬ 5 (∃ȳ ′ i b ′ i ) * is the formula i∈K ¬ 5 (∃ȳ ′ i b ′ i
) in which we have renamed the quantified variables so that they satisfy the discipline of the formulas in T . According to the conditions of application of rule ( 15) and the form of the negations in the left hand side of this rule, we check easily that we can fix the negations of the preceding formula as follows

¬ 5 (∃x ′ a ′ ∧ i∈K ¬ 5 (∃ȳ ′ i b ′ i ) * ).
Thus, rule ( 15) is correct in T .

Correctness of rule ( 16)

¬ 4     ∃x a ∧ q∧ ¬ 5 ∃ȳ b∧ n i=1 ¬ 5 (∃z i c i )     =⇒ ¬ 4 (∃x a ∧ q ∧ ¬ 5 (∃ȳ b))∧ n i=1 ¬ 4 (∃xȳz i c i ∧ q 0 ) *
with n > 0, and q 0 is the formula q in which all the occurrences of ¬ k have been replaced by ¬ 0 . The formula n i=1 ¬ 4 (∃xȳz i c i ∧ q 0 ) * is the formula n i=1 ¬ 4 (∃xȳz i c i ∧ q 0 ) in which we have renamed the quantified variables so that they satisfy the discipline of the formulas of T .

The left hand side of rule ( 16) is equivalent in T to

¬(∃x a ∧ q ∧ ¬(∃ȳ b ∧ ¬ n i=1 (∃z i c i ))).
Since the first negation of ¬(∃ȳ b... in the left hand side of rule ( 16) is of the form ¬ 5 then according to Definition 4.5.1, all the variables of ȳ are reachable in ∃ȳ b, and thus according to Property 4.2.10 we have T |= ∃?ȳ b. According to Property 3.1.10, the precedent formula is equivalent in T to

¬(∃x a ∧ q ∧ ¬((∃ȳ b) ∧ ¬(∃ȳ b ∧ n i=1 (∃z i c i )))).
By distributing the ∧ on the ∨ and the ∃ on the ∨ and since the quantified variables have distinct names and different from those of the free variables then the preceding formula is equivalent in T to

¬(∃x a ∧ q ∧ ¬((∃ȳ b) ∧ ¬ n i=1 (∃z i ȳ b ∧ c i ))), i.e. to ¬(∃x a ∧ q ∧ ((¬(∃ȳ b)) ∨ n i=1 (∃z i ȳ b ∧ c i ))), i.e. to ¬(∃x (a ∧ q ∧ ¬(∃ȳ b)) ∨ n i=1 (a ∧ q ∧ (∃z i ȳ b ∧ c i ))),
which, according to the discipline of the formulas in T (the quantified variables have distinct names and different from those of the free variables), is equivalent in

T to ¬(∃x (a ∧ q ∧ ¬(∃ȳ b)) ∨ n i=1 (∃z i ȳ a ∧ q ∧ b ∧ c i )), i.e. to ¬((∃x a ∧ q ∧ ¬(∃ȳ b)) ∨ n i=1 (∃xz i ȳ a ∧ q ∧ b ∧ c i )), i.e. to ¬(∃x a ∧ q ∧ ¬(∃ȳ b)) ∧ n i=1 ¬(∃xȳz i a ∧ q ∧ b ∧ c i ).
Since we have ¬ 5 (∃ȳ b... in the left hand side of rule ( 16) then according to Definition 4.5.1, we have (i) T |= b → a. But since we have also ¬ 5 (∃z i c i ) for all i ∈ {1, ..., n}, then according to Definition 4.5.1 we have (ii) T |= c i → b. From (i) and (ii) we have T |= c i → (a ∧ b). Thus the preceding formula is equivalent in T to

¬(∃x a ∧ q ∧ ¬(∃ȳ b)) ∧ n i=1 ¬(∃xȳz i c i ∧ q), i.e. to ¬(∃x a ∧ q ∧ ¬(∃ȳ b)) ∧ n i=1 ¬(∃xȳz i c i ∧ q) * ,
where n i=1 ¬ 4 (∃xȳz i c i ∧ q) * is the formula n i=1 ¬ 4 (∃xȳz i c i ∧ q) in which we have renamed the quantified variables so that they satisfy the discipline of the formulas of T . According to the conditions of application of rule ( 16) and the form of the negations in the left hand side of this rule, we check easily that we can fix the negations of the preceding formula as follows

¬ 4 (∃x a ∧ q ∧ ¬ 5 (∃ȳ b)) ∧ n i=1 ¬ 4 (∃xȳz i c i ∧ q 0 ) * ,
where q 0 is the formula q in which all the occurrences of ¬ k have been replaced by ¬ 0 . Thus rule ( 16) is correct in T .

Proof, third part: Every repeated application of the rewriting rules on an initial working formula produces a conjunction of final working formulas. According to what we have shown in the sub-section "proof: first part", every repeated application of our rules on an initial working formula terminates. Let us now show that the obtained formula is a conjunction of final working formulas.

Recall that we write i∈I ϕ i , and call conjunction each formula of the form ϕ i1 ∧ ϕ i2 ∧ ... ∧ ϕ in ∧ true. In particular, for I = ∅, the conjunction i∈I ϕ i is reduced to true. Moreover, we do not distinguish two formulas which can be made equal using the following transformations of sub-formulas:

ϕ ∧ ϕ =⇒ ϕ, ϕ ∧ ψ =⇒ ψ ∧ ϕ, (ϕ ∧ ψ) ∧ φ =⇒ ϕ ∧ (ψ ∧ φ), ϕ ∧ true =⇒ ϕ, ϕ ∨ false =⇒ ϕ.
Let us show first that every substitution of a sub-working formula of a conjunction of working formulas by a conjunction of working formulas produces a conjunction of working formulas. Let i∈I ϕ i be a conjunction of working formulas. Let ϕ k with k ∈ I be an element of this conjunction of depth d k . Two cases arise:

1. We replace ϕ k by a conjunction of working formulas. Thus, let j∈J k φ j be a conjunction of working formulas which is equivalent to ϕ k in T . The conjunction of working formulas i∈I ϕ i is equivalent in T to

( i∈I-{k} ϕ i ) ∧ ( j∈J k φ j )
which is clearly a conjunction of working formulas. 2. We replace a strict sub-working formula of ϕ k by a conjunction of working formulas.

Thus, let φ be a sub-working formula of ϕ k of depth d φ < d k (thus φ is different from ϕ k ). Thus, ϕ k has a sub-working formula17 of the form

¬(∃xα ∧ ( l∈L ψ l ) ∧ φ),
where L is a finite (possibly empty) set and all the ψ l are working formulas. Let j∈J φ j be a conjunction of working formulas which is equivalent to φ in T . Thus the preceding sub-working formula of ϕ k is equivalent in T to

¬(∃xα ∧ ( l∈L ψ l ) ∧ ( j∈J φ j )),
which is clearly a sub-working formula and thus ϕ k is equivalent to a working formula and thus i∈I ϕ i is equivalent to a conjunction of working formulas.

From 1 and 2 we deduce that (i) every substitution of a sub-working formula of a conjunction of working formulas by a conjunction of working formulas produces a conjunction of working formulas.

Since each rule transforms a working formula into a conjunction of working formulas, then according to the sub-section "proof: first part" and (i) we deduce that every repeated application of the rewriting rules on an initial working formula terminates and produces a conjunction of working formulas. Thus, since an initial working formula starts by ¬ 4 and all its other negations are of the form ¬ 0 then all long the application of our rules and by going down along the nested negations of any working formula ϕ obtained after any finite application of our rules, we can build many series of negations which represent the paths that we should follow from the top negation of ϕ to reach one of the sub-working formulas of ϕ of depth equal to one. Each of these series is of the one of the following forms:

• a series of ¬ 4 followed by a possibly series of ¬ 0 , • a series of ¬ 4 followed by one ¬ 1 , followed by a possibly series of ¬ 0 , • a series of ¬ 4 followed by one ¬ 2 , followed by a possibly series of ¬ 0 , • a series of ¬ 4 followed by one ¬ 3 , followed by a possibly series of ¬ 0 , • a series of ¬ 4 followed by one or two ¬ 5 , • one or two ¬ 5 . While all the negations of these series are not of the form ¬ 5 or their length is greater than 2 then one of the rules (1),...,(16) can still be applied. As a consequence, when no rule can be applied, we obtain a conjunctions of formulas of depth less or equal to 2 in which all the negations are of the form ¬ 5 . It is a conjunction of final working formulas. Since all the rules do not introduce new free variables then Property 4.6.3 holds.

The Solving Algorithm

Let p be a formula. Solving p in T proceeds as follows:

(1) Transform the formula ¬p (the negation of p) into a wnfv normalized formula p 1 equivalent to ¬p in T .

(2) Transform p 1 into the following initial working formula p 2

p 2 = ¬ 4 (∃ε true ∧ ¬ 0 (∃ε true ∧ p 1 )),
where all the occurrences of ¬ in p 1 are replaced by ¬ 0 .

(3) Apply the preceding rewriting rules on p 2 as many time as possible. According to Property 4.6.3 we obtain at the end a wnfv conjunction p 3 of final working formulas of the form

n i=1 ¬ 5 (∃x i α i ∧ ni j=1 ¬ 5 (∃ȳ ij β ij )).
According to Property 4.5.4, the formula p 3 is equivalent in T to the following wnfv conjunction p 4 of general solved formulas

n i=1 ¬(∃x i α i ∧ ni j=1 ¬(∃ȳ ij β * ij )),
where β * ij is the formula β ij from which we have removed all the equations which occur also in α i . Since p 4 is equivalent to ¬p in T , then p is equivalent in T to

¬ n i=1 ¬(∃x i α i ∧ ni j=1 ¬(∃ȳ ij β * ij )),
which is equivalent to the following disjunction p 5 n i=1

(∃x i α i ∧ ni j=1 ¬(∃ȳ ij β * ij )).
This is the final answer of our solver to the initial constraint p. Note that the negations which were at the beginning of each general solved formula of p 4 have been removed and the top conjunction of p 4 has been replaced by a disjunction. As a consequence, the set of the solutions of the free variables of p 5 is nothing other than the union of the solutions of each formula of the form

∃x i α i ∧ ni j=1 ¬(∃ȳ ij β * ij )
. According to Definition 4.4.6, each of these formulas is written in an explicit solved form which enables us to easily extract the solutions of its free variables. On the other hand, two cases arise:

• If p 4 does not contain free variables then according to Property 4.4.3 the formula p 4 is of the form n i=1 ¬(∃ε true) and thus p 5 is of the form n i=1 ∃ε true. Two cases arise: if n = 0 then p 5 is the empty disjunction (i.e. the formula false). Else, if n = 0 then since we do not distinguish between ϕ ∧ ϕ and ϕ, p 5 is the formula ∃ε true. Since T has at least one model and since p 5 is equivalent to p in T and does not contain news free variables then we have the following theorem:

Theorem 4.7.1 Every formula is equivalent in T either to true, or to false, or to a wnfv formula which has at least one free variable, which is equivalent neither to true nor to false, and where the solutions of the free variables are expressed in a clear and explicit way.

The fact that T accepts at least one model is vital in this theorem. In fact, if T does not have models then the formula true can be equivalent to false in T . In other words, a formula can be equivalent to true in T using a finite application of our rules and equivalent to false using another different finite application of our rules. Theorem 3.3.1 prevents these kinds of conflicts and shows that T has at least three models D, T r and Ra and thus T |= ¬(true ↔ false).

Corollary 4.7.2 T is a complete theory.

Note that using Theorem 4.7.1 and the properties 4.4.5 and 4.2.11, we get Maher's decision procedure [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF] for the basic theory of finite or infinite trees.

Implementation of our algorithm

We have implemented our algorithm in C++ and CHR (Constraint Handling Rules) [START_REF] Fruehwirth | Theory and Practice of Constraint Handling Rules[END_REF][START_REF] Fruehwirth | Essentials of Constraint Programming[END_REF][START_REF] Schrijvers | Automatic implication checking for CHR constraints[END_REF]. The C++ implementation is a straightforward extension of those given in (Djelloul and Dao 2006b). It uses records and pointers and releases unused pointers after each rule application. The CHR implementation was done using Christian Holzbaur's CHR library of Sicstus Prolog 3.11.0. It consists of 18 CHR constraints and 73 CHR rules -most of them are needed for the complicated rules ( 15) and ( 16) of our algorithm. Even if our C++ implementation has given better performances, we think that it is interesting to show how can we translate our rules into CHR rules. We will be able to quickly prototype optimizations and variations of our algorithm and to parallelize it. For CHR, the implementation of this complex solver helps to understand what programming patterns and language features can be useful. The CHR code without comments and examples, but pretty-printed, is about 250 lines, which is one seventh of the size of our C++ implementation. Indeed for code size and degree of abstraction it seems only possible and interesting to describe the CHR implementation, and we do so in the following. The reader can find our full CHR implementation at http://khalil.djelloul.free.fr/solver.txt and can experiment with it online using webchr at http://chr.informatik.uni-ulm.de/ ∼ webchr/. Almost all CHR implementations execute queries from left to right and apply rules top-down in the textual order of the program [START_REF] Duck | The Refined Operational Semantics of Constraint Handling Rules[END_REF]. A CHR constraint in a query can be understood as a procedure that goes efficiently through the rules of the program. When it matches a head constraint of a rule, it will look for the other constraints of the head in the constraint store and check the guard. On success, it will apply the rule. The rule application cannot be undone. If the initial constraint has not been removed after trying all rules, it will be put into the constraint store. Constraints from the store will be reconsidered if newly added constraints constrain its variables.

CHR Constraints

The implementation consists of 18 constraints: two main constraints that encode the tree data structure of the working formulas (nf/4) and the atomic formulas (of/2), 9 auxiliary constraints that perform reachability analysis, variable renaming and copying of formulas, and 7 constraints that encode execution control information, mainly for rules (15) and ( 16).

In more detail, nf(ParentId,Id,K,ExVars) describes a negated quantified basic formula with the identifier of its parent node, its own identifier Id, the level K from ¬ k and the list of existentially quantified variables. Var=FlatTerm of Id denotes an equation between a variable and a flat term (a variable or a function symbol applied to variables) that belongs to the negated sub-formula with the identifier Id. finite(U) of Id denotes the relation finite(U ).

It is easy to represent any working formula ϕ using conjunctions of nf/4 and of/2 constraints. It is enough to create one nf/4 constraint for each quantified basic formula of ϕ and to use a conjunction of of/2 constraints to enumerate the atomic formulas linked to each quantified basic formula.

Example 5.1.2 Let ϕ be the following working formula

¬ 4       ∃u u = 1∧     ¬ 0 (∃ε u = s(v))∧ ¬ 0 (∃w 1 u = s(w 1 ) ∧ w 1 = s(v))∧ ¬ 5 (∃ε v = s(u) ∧ u = 1 ∧ ¬ 5 (∃ε v = s(u) ∧ u = 1 ∧ finite(w 1 ))∧ ¬ 5 (∃w 3 v = s(u) ∧ u = 1 ∧ w 2 = s(w 3 ) ∧ finite(w 3 )) )           .
In rule (9+10) reach args(U,T,P) checks reachability of U from itself in P. If so, true(P) will be executed and thus P will be removed, implementing rule (9). Otherwise, the subsequent finite args(U,T,P) will propagate down the finite relation from U to its arguments, implementing rule (10).

In the rules ( 12) and ( 13) we handle equations one by one (due to the chosen granularity of the constraints), and thus we need auxiliary second CHR rules that perform the update of the level K afterwards.

For rule ( 14) the implementation is easy when nested negation-as-absence [START_REF] Van Weert | Constraint Handling Rules with Negations as Absence[END_REF]) is used to verify that there is no constraint in the subformula that is not in the main formula. Negation-as-absence can be directly encoded in CHR, but then it requires two additional rules per negation. Instead, we have chosen to use in the guard of the rule the CHR library builtin findconstraint(Var,Pattern,Match) that returns on backtracking all constraints Match that match Pattern and that are indexed on variable Var together with negation-as-failure provided by the Prolog built-in \+.

The translation of the complex rules ( 15) and ( 16) of the algorithm require 40 CHR rules, because several non-trivial new expressions have to be computed. Simpagation rules and auxiliary constraints collect the nested nf/4 constraints, compute the reachable variables and atomic formulas, rename the quantified variables and produce updated nf/4 and of/2 constraints. In order not to overburden the reader with technical details, we omit the description of those 40 rules.

Benchmarks: Two partner game

Let us consider the following two partner game: An ordered pair (i, j) is given, with i a non-negative (possibly null) integer and j ∈ {0, 1}. One after another, each player changes the values of i and j according to the following rules • If j = 0 then the actual player should replace i by i -1 in the pair (i, j).

• If j = 1 and i is odd then the actual player can either replace i by i + 1 or replace j by j -1, in the pair (i, j). • If j = 1 and i is even then the actual player can either replace i by i + 1 and j by j -1 in the pair (i, j) or replace only i by i + 1 in the pair let (i, j)

The first player who cannot keep i non negative has lost. This game can be represented by the following directed infinite graph:

It is clear that the player which is at the position (0, 0) and should play has lost. Suppose that it is the turn of player A to play. A position (n, m) is called k-winning if, no matter the way the other player B plays, it is always possible for A to win, after having made at most k moves. It is easy to show that

winning k (x) =           ∃y move(x, y) ∧ ¬( ∃x move(y, x) ∧ ¬( ... ∃y move(x, y) ∧ ¬( ∃x move(y, x) ∧ ¬( f alse )...) 2k          
where move(x, y) means: "starting from the position x we play one time and reach the position y". By moving down the negations, we get an embedding of 2k alternated quantifiers. Suppose that F contains the function symbols 0, 1, f , g, c of respective arities 0, 0, 1, 1, 2. We code the vertices (i, j) of the game graph by the trees c( ī, 0) and c( ī, 1) with ī = (f g) i/2 (0) if i is even, and ī = g(i -1) if i is odd. 18 The relation move(x, y) is then defined as follows:

move(x, y) def ↔ transition(x, y) ∨ (¬(∃uv x = c(u, v)) ∧ x = y) with transition(x, y) def ↔                ∃u 1 v 1 u 2 v 2 x = c(u 1 , v 1 ) ∧ y = c(u 2 , v 2 )∧            (v 1 = 0 ∧ v 2 = v 1 ∧ pred(u 1 , u 2 )) ∨ (v 1 = 1 ∧   (∃w u 1 = g(w) ∧ (u 2 = f (u 1 ) ∧ v 2 = v 1 )∨ (u 2 = u 1 ∧ v 2 = 0) )∨ (¬(∃w u 1 = g(w)) ∧ u 2 = g(u 1 ) ∧ (v 2 = v 1 ∨ v 2 = 0))   ) ∨ (¬(v 1 = 0) ∧ ¬(v 1 = 1) ∧ u 2 = u 1 ∧ v 2 = v 1 )                           pred(u 1 , u 2 ) def ↔       (∃j u 1 = f (j) ∧ (∃k j = g(k) ∧ u 2 = j)∨ (¬(∃k j = g(k)) ∧ u 2 = u 1 ) )∨ (∃j u 1 = g(j) ∧ (∃k j = g(k) ∧ u 2 = u 1 )∨ (¬(∃k j = g(k)) ∧ u 2 = j) )∨ (¬(∃j u 1 = f (j)) ∧ ¬(∃j u 1 = g(j)) ∧ ¬(u 1 = 0) ∧ u 2 = u 1 )      
If we take as input of our solver the formula winning k (x) then we will get as output a disjunction of simple formulas where the solutions of the free variable x represent all the k-winning positions.

For winning 1 (x) our algorithm gives the following formula:

∃u 1 u 2 x = c(u 1 , u 2 ) ∧ u 1 = g(u 2 ) ∧ u 2 = 0,
which corresponds to the solution x = c(g(0), 0). For winning 2 (x) our algorithm gives the following disjunction of simple formulas   (∃u 1 u 2 x = c(u 1 , u 2 ) ∧ u 1 = g(u 2 ) ∧ u 2 = 0) ∨ (∃u 3 u 4 u 5 u 6 x = c(u 3 , u 6 ) ∧ u 3 = g(u 4 ) ∧ u 4 = f (u 5 ) ∧ u 5 = g(u 6 ) ∧ u 6 = 0)   , which corresponds to the solution x = c(g(0), 0) ∨ x = c(g(f (g(0))), 0). Note that x is the only free variable in the two preceding disjunctions and its solutions represent the positions which are k-winning.

The times of execution (CPU time in milliseconds) of the formulas winning k (x) are given in the following table as well as a comparison with those obtained using a decision procedure for decomposable theories (Djelloul 2006a) (even though the later does not produce comprehensible results, i.e. explicit solved forms). The benchmarks are performed on a 2.5Ghz Pentium IV processor, with 1024Mb of RAM. This decision procedure takes from 10% to 40% more time, comparing with our C++ implementation to solve the winning k (x) formulas of our game and overflows the memory for k > 20, i.e. 40 nested alternated quantifiers. Our C++ implementation has better performance and is able to give all the winning k strategies in a clear and explicit way until k = 40, i.e. 80 nested alternated quantifiers.

The execution times of winning k (x) using our CHR implementation are 12-30 times slower than those obtained using our C++ implementation and the maximal depth of working formula that can be solved is 14 (k = 7). These results are in line with the experience that the overhead of using declarative CHR without optimisations induces an overhead of about an order of magnitude over implementations in procedural languages. As discussed in the conclusions, switching to a more recent optimizing CHR compiler may close the gap to a small constant factor.

The algorithm given in (Djelloul 2006a) is a decision procedure in the form of five rewriting rules which for every decomposable theory T transforms a first-order formula ϕ into a conjunction φ of final formulas easily transformable into a Boolean combination of existentially quantified conjunctions of atomic formulas. This decision procedure does not warrant that the solutions of the free variables are expressed in a clear and explicit way and can even produce formulas having free variables but being always true or false in T . In fact, for our two player game, we got conjunctions of final formulas where the solutions of the free variable x was incomprehensible, especially from k = 5.

We also tried to use Remark 4.4.2 of (Djelloul 2006a) which gives a way to get a disjunction of the form

i∈I (∃x ′ i α ′ i ∧ j∈Ji ¬(∃ȳ ′ ij β ′ ij )) ( 36
)
as output of the decision procedure. As the author of (Djelloul 2006a) wrote: "it is more easy to understand the solutions of the free variables of this disjunction of solved formulas than those of a conjunction of solved formulas". That is of course true, but this does not mean that the solutions of the free variables of this formula are expressed in a clear and explicit way. In fact, we got a disjunction of the form (36) where many variables which occurred in left hand sides of equations of α ′ i occurred also in left hand sides of equations of some β ′ ij . Moreover, many formulas of the preceding disjunction contained occurrences of the free variable x but after a hard and complex manual checking we found them equivalent to false. As a consequence, the solutions of x was completely not evident to understand and we could not extract clear and understandable winning k (x) strategies for all k ≥ 5. In order to simplify the formula (36) we finally used our solving algorithm on it and have got a disjunction of simple formulas equivalent to (36) in T in which:

(1) all the formulas having free occurrences of x but being always false in T have been removed, (2) the solutions of the free variable x were expressed in a clear and explicit way.

We now discuss why our solver is faster than the decision procedure of K. Djelloul. The latter uses many times a particular distribution (rule (5) in (Djelloul 2006a)) which decreases the depth of the working formulas but increases exponentially the number of conjunctions of the working formulas until overflowing the memory. Our solving algorithm uses a similar distribution (rule ( 16)) but only after a necessary propagation step which copies the basic formulas into the sub-working formulas and checks if there exists no working formulas which contradict their top-working formula. This step enables us to remove the inconsistent working formulas and to not lose time with solving a huge working formulas (i.e. of big depth) which contradicts their top-working formulas. It also prevents us from making exponential distributions between huge inconsistent working formulas which finally are all equivalent to false. Unfortunately, we cannot add this propagation step to the decision procedure of (Djelloul 2006a) since it uses many properties which hold only for the theory of finite or infinite trees and not for any decomposable theory T .

The game introduced in this paper was inspired from those given in (Djelloul 2006a) but is different. Solving a winning k (x) formula in this game generates many huge working formulas which contradict their top-working formulas. Our algorithm removes directly these huge working formulas after the first propagation step (rules (1),...,(13)). The decision procedure cannot detect this inconsistency and is obliged to apply a costly rule (rule (5) in (Djelloul 2006a)) to decrease the size of these inconsistent working formulas until finding basic inconsistent formulas of the form ¬(a ∧ ¬(∃ε true)) or ¬(∃ε false ∧ ϕ). At each application of this rule, the depth of the working formulas decreases but the number of conjunctions increase exponentially until overflowing the memory. This explains why for this game the decision procedure overflows the memory for k > 20 while our solver can compute the winning k (x) strategies until k = 40.

Benchmarks: Random normalized formulas

We have also tested our 16 rules on randomly generated normalized formulas such that in each sub-normalized formula of the form ¬(∃x α ∧ n i=1 ϕ i ), with the ϕ i 's normalized formulas and n ≥ 0, we have:

• n is a positive integer randomly chosen between 0 and 4.

• The number of the atomic formulas in the basic formula α is randomly chosen between 1 and 8. Moreover, the atomic formula true occurs at most once in α.

• The vector of variables and the atomic formulas of ∃x α are randomly generated starting from a set containing 10 variables, the relation finite and 6 function symbols: f 0 , f 1 , f 2 , g 0 , g 1 , g 2 . Each function symbol f j or g j is of arity j with 0 ≥ j ≥ 2.

The benchmarks were realized on a 2.5Ghz Pentium IV processor with 1024Mb of RAM as follows: For each integer 1 ≥ d ≥ 42 we generated 10 random normalized formulas19 of depth d, we solved them and computed the average execution time (CPU time in milliseconds). Once again, the performances (time and space) of our 16 rules are impressive comparing with those of the decision procedure for decomposable theories. Note that for d = 42, all the normalized formulas could not be solved and overflowed the memory.

Discussion and conclusion

We gave in this paper a first-order axiomatization of an extended theory T of finite or infinite trees, built on a signature containing not only an infinite set of function symbols but also a relation finite(t) which enables to distinguish between finite or infinite trees. We showed that T has at least one model and proved its completeness by giving not only a decision procedure but a full first-order constraint solver which transforms any first-order constraint ϕ into an equivalent disjunction φ of simple formulas such that φ is either the formula true, or the formula false, or a formula having at least one free variable, being equivalent neither to true nor to false and where the solutions of the free variables are expressed in a clear and explicit way. This algorithm detects easily formulas that have free variables but are always true or always false in T and is able to solve any first-order constraint satisfaction problem in T . Its correctness implies the completeness of T .

On the other hand S. Vorobyov [START_REF] Vorobyov | An Improved Lower Bound for the Elementary Theories of Trees[END_REF] has shown that the problem of deciding if a proposition is true or not in the theory of finite or infinite trees is non-elementary, i.e. the complexity of all algorithms solving propositions is not bounded by a tower of powers of 2 ′ s (top down evaluation) with a fixed height. A. Colmerauer and T. Dao [START_REF] Colmerauer | Expressiveness of full first-order formulas in the algebra of finite or infinite trees[END_REF] have also given a proof of non-elementary complexity of solving constraints in this theory. As a consequence, our algorithm does not escape this huge complexity and the function α(ϕ) used to show the termination of our rules illustrates this result.

We implemented our algorithm in C++ and CHR and compared both performances with those obtained using a recent decision procedure for decomposable theories (Djelloul 2006a). This decision procedure is not able to present the solutions of the free variables in a clear and explicit way and overflows the memory while solving normalized formulas with depth d > 40. Our C++ implementation is faster than this decision procedure and can solve normalized formulas of depth d = 80. This is mainly due to the fact that our algorithm uses two steps: (1) a top-down propagation of constraints and (2) a bottom-up elimination of quantifiers and depth reduction of the working formulas. In particular, the first step enables to minimize the number of application of costly distributions and avoids to lose time with solving huge formulas which contradict their top-formulas.

Future implementation work will focus on our CHR implementation, since from previous experience we are confident that we can get the performance overhead down to a small constant factor while gaining the possibility to prototype variations of our algorithm in a very high level language. Switching to a more recent optimizing CHR compiler from K.U. Leuven would most likely improve performance. We also think that we can minimize the use of the debated negation-as-absence [START_REF] Van Weert | Constraint Handling Rules with Negations as Absence[END_REF]) by introducing reference counters for the two main constraints. This should also give us the possibility to obtain a parallel implementation that is derived from the existing one with little modification, similar to what has been done for parallelizing the union-find algorithm in CHR [START_REF] Fruehwirth | Parallelizing Union-Find in Constraint Handling Rules Using Confluence[END_REF].

  (1, f ), (2, s), (11, a), (12, b), (21, a)} {(ε, f ), (1, a), (2, f ), (21, b), (22, f ), (221, a), (222, f ), (2221, b), ...} (ε, f ), (1, a), (2, f ), (21, s), (22, f ), (211, a), (221, s), (222, f ), (2211, s), (2221, s), (2222, f ), (22111, a), (22211, s), (222111, s), (2221111, a), ...

  a), (2, f ), (21, b), (22, f ), (221, a), ...}, {(ε, f ), (1, b), (2, f ), (21, a), (22, f ), (221, b), ...

  1, a)}, {(ε, s), (1, s), (11, a)}, {(ε, s), (1, s), (11, s), (111, a)}, ... {(ε, f ), (1, a), (2, f ), (21, s), (22, f ), ...}, {(ε, f ), (1, s), (2, f ), (11, a), (21, s), (22, f ), ...} ...

  d the node (ij 1 ...j k , l). If a is a set of nodes (i.e. a ∈ D), then we denote by i.a the set of nodes {i.d | d ∈ a}. Definition 2.2.1 In the set D, the construction operation linked to the n-ary label l is the application l D : (a 1 , ..., a n ) → {(ε, l)} ∪ 1.a 1 ∪ ... ∪ n.a n with a 1 ...a n elements of D. Remark 2.2.2 Let a be an element of D. Let us denote by ν k (a) the set of nodes of a of depth k. Many remarks must be stated concerning any elements a, a i and b of D:

  2.1 and the definition of the relation finite D , the properties [1 D ], [2 D ], [4 D ] and [5 D ] hold. On the other hand, property [3 D ] is much less obvious and deserves to be proved. Let a 1 , ..., a m and b 1 , ..., b n be elements of D. According to the first point of Remark 2.2.2, the D-formula n i=1 b

  .. which start by distinct function symbols. According to Axiom [1], all these individuals are distinct. According to (9) and Axiom [5] all these individuals are finite in M. Corollary 3.3.3 Each model of T has an infinite domain, i.e. an infinite set of individuals.

  Property 4.2.4 Let α and β be two solved basic formulas containing only equations. If Lhs(α) = Lhs(β) and T |= α → β then T |= α ↔ β.

  Let us denote by f i respectively [b 1 , ..., b n , a 1 , ..., a m ] i the function symbol respectively the set of the variables which occur in the term t D i [b 1 , ..., b n , a 1 , ..., a m ]. According to the second and third point of Remark 2.2.2 we have:

	b n , a 1 , ..., a m ]).	(5)
	Let i ∈ {1, ..., n}.

  occurs in the term t[x]. According to the first point of Remark 4.2.8 and since for all i ∈ {1, ..., n} the variables of ȳi are reachable in ∃ ȳi α i , then the equation v = t[x] is reachable in ∃ ȳi α i and thus according to the second point of Remark 4.2.8 the conjunction α i contains a sub-formula of the form (

  • b * i is the formula obtained by removing from b i the formulas of the form finite(u) which occur also in a ′′ • ȳ′ i is the vector of the variables of ȳi x′′′ which are reachable in ∃ȳ i x′′′ b * i . • b ′ i is the conjunction of the equations and the formulas of the form finite(x) which are reachable in ∃ȳ i x′′′ b * i . • K ⊆ {1, ..., n} is the set of the indices i such that i ∈ K if and only if no variable of x′′ occurs in b

  • If p 4 contains at least one free variable then according to Property 4.4.3 neither T |= p 4 nor T |= ¬p 4 and thus neither T |= ¬p 5 nor T |= p 5 .

  and B denote conjunctions of constraints. A simplification rule H ⇔ C B replaces instances of the CHR constraints H by B provided the guard test C holds. A propagation rule H ⇒ C B instead just adds B to H without removing anything. The hybrid simpagation rules will come handy in the implementation:H 1 \H 2 ⇔ C B removes matched constraints H 2 but keeps constraints H 1 .The constraints of the store comprise the state of an execution. Starting from an arbitrary initial store (called query), CHR rules are applied exhaustively until a fixpoint is reached. Trivial non-termination of a propagation rule application is avoided by applying it at most once to the same constraints.

	5.1 Constraint Handling Rules (CHR) Implementation
	CHR manipulates conjunctions of constraints that reside in a constraint store. Let
	H, C

φ is solved according to Definition 4.2.4 of(Djelloul

2006a)

We have chosen to denote by T the Maher's theory of finite or infinite trees and by T our extended theory of finite or infinite trees.

In(Djelloul 2006a), we have shown that the Maher's theory T of finite or infinite trees is decomposable. We can show easily using a similar proof that our extended theory T is also decomposable.

Of course, for k = 0, i 1 ...i k is reduced to ε.

Of course, for n = 0, (i k+1 ...i k+n , l ′ ) is reduced to (ε, l ′ ).

In other words, each element of D is a set of nodes, i.e. a subset of N .

If k = 0 then according to (ii) each ν 1 (b i ) depends in the worst case on ν 0 (b 1 ), ..., ν 0 (bn) and a 1 ,...,am. According to (i) all the ν 0 (b 1 ), ..., ν 0 (bn) have constant values and thus each ν 1 (b i ) depends only on a 1 , ..., am. Let us now assume that each ν k (b i ) depends only on a 1 , ..., am and let us show that this hypothesis is true for ν k+1 (b i ). According to (ii), each ν k+1 (b i ) depends in the worst case on ν k (b 1 ), ..., ν k (bn) and a 1 , ..., am, which according to our hypothesis depend only on a 1 , ..., am. Thus, the recurrence is true for all k ≥ 0.

By considering that each formula is also a sub-formula of itself.

In fact, the variable x has a free occurrence in ∃ȳ i α i and the variable v has a bound occurrence in ∃ȳ i α i (because v is a quantified reachable variable in ∃ȳ i α i ) and thus according to the discipline of our formulas we have v ≻ x.

Recall that v 1 ∈ (X ∪ X ′ ∪ Y ) and thus v 1 is a free variable in (15). As a consequence, it is already instantiated in (16).

Recall that T r is the model of finite or infinite trees.

In other words, p ′ is of the form ¬ k ′ (∃x ′ α ′ ∧ p * ∧ p) where p * is a conjunction of working formulas and p is the formula (32).

By considering that the set of the sub-formulas of any formula ϕ contains also the whole formula ϕ.

We of course renamed the quantified variables of each randomly generated normalized formula so that it respects the discipline of the formulas in T

Acknowledgments We thank Alain Colmerauer for our very long discussions about the theory of finite or infinite trees and its models. Many thanks also to the anonymous referees for their careful reading and suggestions which help us to improve this paper. Khalil Djelloul thanks the DFG research project GLOB-CON for funding and supporting his research. Thanks also to Marc Meister and Hariolf Betz for their kind review of this article.

ϕ can be expressed using the following conjunction of constraints:

CHR Rules

The rules (1) to ( 14) have a rather direct translation into CHR rules. It seems hard to come up with a more concise implementation.

% 1 Locally simplify equations (1) @ nf(Q,P,1,Xs) \ U=U of P <=> true.

(2) @ nf(Q,P,1,Xs) \ V=U of P <=> gt(U,V) | U=V of P.

(3) @ nf(Q,P,1,Xs), U=V of P \ U=G of P <=> gt(U,V) | V=G of P. (4) @ nf(Q,P,1,Xs), U=F of P, U=G of P <=> notsamefunctor(F,G) | true(P).

(5) @ nf(Q,P,1,Xs), U=F of P \ U=G of P <=> samefunctor(F,G) | same_args(F,G,P). ( 6) @ nf(Q,P,1,Xs) <=> nf(Q,P,2,Xs). % 2 finiteness check (7) @ nf(P0,P,2,Xs), finite(U) of P \ finite(U) of P <=> true. (8) @ nf(P0,P,2,Xs), U=V of P \ finite(U) of P <=> var(V) | finite(V) of P. (9+10)@nf(P0,P,2,Xs),U=T of P \ finite(U) of P <=> nonvar(T) | reach_args(U,T,P), finite_args(U,T,P). (11) @ nf(Q,P,2,Xs) <=> nf(Q,P,3,Xs). % 4/0-4/1 copy down before solving (12) @ nf(Q,P,4,Xs), A of P, nf(P,P1,0,Ys) ==> A of P1.

nf(Q,P,4,Xs) \ nf(P,P1,0,Ys) <=> nf(P,P1,1,Ys).

% 4/3-4/4 replace down after solving (13) @ nf(Q,P,4,Xs),U=V of P, nf(P,P1,3,Ys)\ U=G of P1 <=> V\==G | U=V of P1. nf(Q,P,4,Xs) \ nf(P,P1,3,Ys) <=> nf(P,P1,4,Ys).

% 4/5-true trivial satisfaction -each A of P1 also occurs as A of P (14) @ nf(Q,P,4,Xs), nf(P,P1,5,Ys) <=> \+(findconstraint(P1,(A of P1),_), \+findconstraint(P,(A of P),_)) | true(P).

Note that rules (1) to ( 5) are similar to the classical CHR equation solver for flat rational trees [START_REF] Fruehwirth | Essentials of Constraint Programming[END_REF][START_REF] Meister | Complexity of the CHR Rational Tree Equation Solver[END_REF]. By applying results of [START_REF] Meister | Complexity of the CHR Rational Tree Equation Solver[END_REF], we can show that the worstcase time complexity of these rules of the algorithm is quadratic in the size of the equations.

In the rules (2) and (3), the predicate gt(U,V) checks if U ≻ V. Note that the constraint true(P) used in rule (4) removes all constraints associated with P using an auxiliary rule not shown.