Thi-Bich-Hanh Dao

Khalil Djelloul

Solving First-Order Constraints in the Theory of the Evaluated Trees

We present in this paper a first-order extension of the solver of Prolog III, by giving not only a decision procedure, but a full firstorder constraint solver in the theory T of the evaluated trees, which is a combination of the theory of finite or infinite trees and the theory of the rational numbers with addition, subtraction and a linear dense order relation. The solver is given in the form of 28 rewriting rules which transform any first-order formula ϕ into an equivalent disjunction φ of simple formulas in which the solutions of the free variables are expressed in a clear and explicit way. The correctness of our algorithm implies the completeness of a first-order theory built on the model of Prolog III.

Introduction

The algebra of finite or infinite trees plays a fundamental role in computer science: it is a model for data structures, program schemes and program executions. As early as 1976, G. Huet proposed an algorithm for unifying infinite terms, that is solving equations in that algebra [START_REF] Huet | Resolution d'equations dans les langages d'ordre 1[END_REF]. B. Courcelle has studied the properties of infinite trees in the scope of recursive program schemes [START_REF] Courcelle | Fundamental Properties of Infinite Trees[END_REF]. A. Colmerauer has described the execution of Prolog II, III and IV programs in terms of solving equations and disequations in that algebra [START_REF] Colmerauer | Equations and disequations 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].

The unification of finite terms, i.e. solving conjunctions of equations in the theory of finite trees has first been studied by A. Robinson [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF]. Some algorithms with better complexities have been proposed after by M.S. Paterson and M.N.Wegman [START_REF] Paterson | Linear unification[END_REF] and A. Martelli and U. Montanari [START_REF] Martelli | An efficient unification algorithm[END_REF]. A good synthesis on this field can be found in the paper of J.P. Jouannaud and C. Kirchner [START_REF] Jouannaud | Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification[END_REF]. Solving conjunctions of equations on infinite trees has been studied by G. Huet [START_REF] Huet | Resolution d'equations dans les langages d'ordre 1[END_REF], by A. Colmerauer [START_REF] Colmerauer | Prolog and infinite trees[END_REF] and by J. Jaffar [START_REF] Jaffar | Efficient unification over infinite terms[END_REF]. Solving conjunctions of equations and disequations on finite or infinite trees has been studied by H.J. Burckert [START_REF] Bürckert | Solving disequations in equational theories[END_REF] and A. Colmerauer [START_REF] Colmerauer | Equations and disequations on finite and infinite trees[END_REF]. An incremental algorithm for solving conjunctions of equations and disequations on rational trees has then been proposed by V.Ramachandran and P. Van Hentenryck [START_REF] Ramachandran | Incremental algorithms for constraint solving and entailment over rational trees[END_REF].

On the other hand, M.J. Maher has axiomatized the theory of finite or infinite trees and showed its completeness using a decision procedure which transforms any first-order formula into a Boolean combination of quantified conjunctions of atomic formulas [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF]. A much more general decision procedure was recently given by K. Djelloul in the frame of decomposable theories [START_REF] Djelloul | Decomposable Theories[END_REF].

We have then extended Maher's theory of finite or infinite trees by giving a complete first-order axiomatization of the evaluated trees which are a combination of finite or infinite trees with construction operations and the rational numbers with addition, subtraction and a linear dense order relation [START_REF] Djelloul | About the combination of trees and rational numbers in a complete first-order theory[END_REF]. This theory, denoted by T , reflects essentially to Prolog III which has been modeled by A. Colmerauer [START_REF] Colmerauer | An introduction to Prolog III[END_REF] using a combination of trees and rational numbers. Nevertheless, the solver of Prolog III is not able to solve arbitrary quantified first-order constraints built on a combination of trees and rational numbers.

A first attempt of an extension of the solver of Prolog III was given in [START_REF] Djelloul | Extension into trees of first order theories. Proceeding of the 8th International conference on artificial intelligence and symbolic computation[END_REF]. It consists in a decision procedure which for every proposition (formula without free variables) gives either true of false in T . Unfortunately, this decision procedure is not able to solve first-order constraints having free variables. In fact, it does 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 φ.

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 T . 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 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 first-order 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 present in this paper, not only a decision procedure, but a full firstorder constraint solver which gives clear and explicit solutions for any first-order constraint satisfaction problem in T . Our solver is not simply a combination of an algorithm over trees with one over rational numbers, but a powerful mechanism to solve mixed constraints. It includes full systems of typing deduction and constraint simplification and propagation. One of the major difficulties in this work resides in the fact that (i) the theory of finite or infinite trees does not accept full elimination of quantifiers, (ii) every algorithm deciding propositions in the theory of finite or infinite trees has a non-elementary complexity [START_REF] Vorobyov | An Improved Lower Bound for the Elementary Theories of Trees[END_REF] and (iii) the function symbols + andof T have two different behaviors whether they are applied on trees or rational numbers. For example +(1, 1) is the rational number 2, while +(1, f 0 ) is the tree whose root is labeled + and whose sons are 1 and the tree's constant f 0 .

One of the practical applications of our solver is a powerful extension of the internal solver of Prolog III by allowing the user to handle general first-order constraints and solve them in T . The solver will then give the solutions of the free variables in all the models of T and present them in a clear and explicit way. As far as we know, this is the first algorithm which is able to do a such work. Solving quantified constraints over trees and rational numbers can also be used in PSPACE-complete decision problems from areas such as planning under uncertainty, adversary game playing, and model checking. For example, in game playing we may want to find a winning strategy for all possible moves of the opponent. In a manufacturing problem it may be required that a configuration must be possible for all possible sequences of user choices. Finally, when planning in a safety critical environment, such as a nuclear power station, we require that an action is possible for every eventuality.

The paper is organized in four sections followed by a conclusion. This introduction is the first section. In Section 2 we present the theory of the evaluated trees and introduce an example of a complex constraint in this theory. In Section 3, we define the notions of basic formulas, blocks and solved blocks in T which are particular conjunctions of atomic formulas. We end this section by showing that every quantified solved block can be decomposed in three embedded sequences of quantifications having particular properties which enable us to eliminate some quantifiers. In Section 4, we present the working formulas, the general solved formulas and the algorithm of constraint solving in T . The algorithm is presented in the form of 28 rewriting rules and transforms an initial working formula of depth d into a final working formula of depth less than or equal to three. The main idea behind this algorithm consists in (1) a top-down simplification and propagation of constraints. In each level, quantified blocks are locally solved, decomposed and then propagated to the embedded sub-formulas. Inconsistent sub-formulas are also removed (2) a bottom-up elimination of quantifiers and working formulas' depth decrease using distribution. The disjunction φ of general solved formulas extracted from the final working formula is either the formula false or true or a formula having at least one free variable, being equivalent neither to false nor to true in T , and where the solutions of the free variables are expressed in a clear and explicit way. We end this section by giving an example of a constraint having two free variables but being always false in T .

The algorithm represented by a set of rewriting rules and the general solved formulas are our main contribution in this paper. The expressiveness and clearness of the solutions of the free variables in the final solved formula are our main goal in this work.

2 Theory T of evaluated trees

Preliminaries

Let F be an infinite set of function symbols containing the symbols +, -, 0 and 1. To each element of F is associated a non-negative integer, its arity. The arities of +, -, 0 and 1 are respectively 2, 1, 0 and 0. Let R = {<, num , tree } be the set of relation symbols, of respective arities 2, 1 and 1. Let V be an infinite countable set of variables. A term is an expression of the form x or f t 1 . . . t n where n ≥ 0, f an n-ary symbol in F and the t i 's are shorter terms. A formula is an expression of the forms:

s = t, rt 1 ..t n , true, false, ¬(ϕ), (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ), (ϕ ↔ ψ), ∃x ϕ, ∀x ϕ,
where x ∈ V , s, t and the t i 's are terms, r is an n-ary relation symbol in R and ϕ and ψ are shorter formulas. The first four forms are called atomic. 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 otherwise. The free variables of a formula are those which have at least a free occurrence in the formula. For each formula ϕ, we denote by var(ϕ) the set of all the free variables of ϕ. Let x = x 1 . . . x n and ȳ = y 1 . . . y n be two vectors of variables of the same length. The empty vector is denoted by ε. Let ϕ and ϕ(x) be formulas. We write ∃x ϕ for ∃x1...∃xn ϕ, ∀x ϕ for ∀x1...∀xn ϕ, ∃?x ϕ(x) for ∀x∀ȳ ϕ(x) ∧ ϕ(ȳ) → i∈{1,...,n} xi = yi, ∃!x ϕ for (∃x ϕ) ∧ (∃?x ϕ).

Semantically, the new quantifiers ∃? and ∃! simply mean "at most one" and "one and only one".

Axiomatization of T

Let a be a positive integer and let t 1 , ..., t n be terms. Let us denote by: -t 1 < t 2 , the term < t 1 t 2 , -t 1 + t 2 , the term +t 1 t 2 , -t 1 + t 2 + t 3 , the term +t 1 (+t 2 t 3 ), -0t 1 , the term 0,

-at 1 , the term t 1 + • • • + t 1 a , --at 1 , the term (-t 1 ) + • • • + (-t 1 ) a .
The theory T of the evaluated trees is the set of first-order propositions of the following forms:

1 ∀x∀ȳ ((tree f x ) ∧ (tree f ȳ) ∧ f x = f ȳ) → i xi = yi , 2 ∀x∀ȳ f x = g ȳ → num f x ∧ num gȳ, 3 ∀x∀ȳ (( i∈I num xi ) ∧ ( j ∈J tree yj )) → (∃!z k ∈K (tree z k ∧ z k = t k (x , ȳ, z ))), 4 ∀x∀y x < y → (num x ∧ num y), 5 ∀x∀y num x + y ↔ num x ∧ num y, 6 ∀x num -x ↔ num x , 7 ∀x tree hx , 8 ∀x∀y (num x ∧ num y) → x + y = y + x , 9 ∀x∀y∀z (num x ∧ num y ∧ num z ) → x + (y + z ) = (x + y) + z , 10 ∀x num x → x + 0 = x , 11 ∀x num x → x + (-x ) = 0 , 12n ∀x num x → (nx = 0 → x = 0 ), 13n ∀x num x → ∃!y num y ∧ ny = x , 14 ∀x num x → ¬x < x , 15 ∀x∀y∀z num x ∧ num y ∧ num z → ((x < y ∧ y < z ) → x < z ), 16 ∀x∀y (num x ∧ num y) → (x < y ∨ x = y ∨ y < x ), 17 ∀x∀y (num x ∧ num y) → (x < y → (∃z num z ∧ x < z ∧ z < y)), 18 ∀x num x → (∃y num y ∧ x < y), 19 ∀x num x → (∃y num y ∧ y < x ), 20 ∀x ∀y ∀z (num x ∧ num y ∧ num z ) → (x < y → (x + z < y + z )), 21 ∀x (¬num x ) ↔ tree x 22 0 < 1,
where n is a non-null integer, f and g are two distinct function symbols taken from F , h ∈ F -{+, -, 0, 1}, x, y, z are variables, x is a vector of variables x i , ȳ is a vector of variables y i , z is a vector of distinct variables z i , I and J are finite possibly empty sets, and where t k (x, ȳ, z) is a term which begins by a function symbol f k element of F -{0, 1} followed by variables taken from x or ȳ or z. Moreover, if f k ∈ {+, -} then t k (x, ȳ, z) contains at least one variable taken from ȳ or z. The axiom 3 shows that all models of T contain infinite trees. In fact we have T |= ∃!z z = f z ∧ tree z for I = J = ∅. In this case, the tree z is an infinite tree of the form f (f (f (...))). Note that we have not T |= ∀xnum x → (∃!z z = x +x ∧tree z ), since we have T |= num x ↔ num (x +x ) according to axiom 5 which contradicts tree z and z = x + x. This is why we have a condition if f k belongs to {+, -}.

This theory has as model (possibly) infinite trees whose nodes are labelled by Q∪F such that each subtree labelled by Q∪{+, -} is evaluated in Q and reduced to a leaf labeled by an element of Q.

Let us now introduce an example of constraints in T . Let us consider the following two-player game: An ordered pair (n, m) of non-negative rational numbers is given and one after another each player subtracts 1 or 2 from n or m but keeping n and m non-negative. The first player who cannot play any more 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. The constraint expressing that a position x is k-winning is:

winning k (x) ↔    ∃ymove(x, y) ∧ ¬(∃xmove(y, x)∧ ¬(∃ymove(x, y) ∧ ¬(∃xmove(y, x) ∧ ¬(. . . ∧ ¬(∃ymove(x, y) ∧ ¬(∃xmove(y, x) ∧ ¬(false )) . . .) 2k   
Each position (n, m) is represented by c(i, j) with c a function symbol of arity 2 and i, j ∈ Q. The constraint move(x, y) is defined by

     (∃i∃j x = c(i, j) ∧ y = c(i -1, j) ∧ i > 1 ∧ j > 0)∨ (∃i∃j x = c(i, j) ∧ y = c(i -2, j) ∧ i > 2 ∧ j > 0)∨ (∃i∃j x = c(i, j) ∧ y = c(i, j -1) ∧ i > 0 ∧ j > 1)∨ (∃i∃j x = c(i, j) ∧ y = c(i, j -2) ∧ i > 0 ∧ j > 2)∨ (¬(∃i∃j x = c(i, j) ∧ num i ∧ num j ) ∧ x = y)     
By replacing the definition of move in the constraint winning k (x), we have a first-order constraint with one free variable x in the theory T of evaluated trees. Solving this constraint means finding all the positions x which are k-winning.

3 Block and quantified block in T

We will now present structured formulas called blocks and show some of their properties. Essentially a block is a conjunction of atomic formulas where all the variables are well typed and which gives enough informations to be locally solved. We will also define a mechanism to decompose each quantified block in three quantified blocks having interesting properties that will help us for solving first-order constraints on quantified blocks.

Basic formula and block in T

Suppose that the variables of V are ordered by a linear strict and dense order relation without endpoints, denoted by " ≻ ". For each formula ϕ, the bound variables are renamed such that for each sub-formula of ϕ we have x ≻ y for each bound variable x and each free variable y. We denote by Σ n i=1 t i the term t 1 + . . . + t n + 0 with t 1 + . . . + t n the term t 1 + . . . + t n where all the terms 0 have been removed.

Let f ∈ F -{0, 1}, a 0 ∈ Z and a i ∈ Z. We call leader of the equation x 0 = f x 1 ...x n or x 0 = x 1 the variable x 0 . We call leader of the formula Σ n i=1 a i x i = a 0 1 the greatest variable x k (in the order ≻) such that a k = 0.

Let f ∈ F , a 0 ∈ Z and a i ∈ Z. We call basic formula every conjunction α of formulas of the form:

-true, false, num x, tree x , -x = y, x = f y 1 ...y n , Σ n i=1 a i x i = a 0 1, Σ n i=1 a i x i < a 0 1.
The formulas num x and tree x are called typing constraints. The formulas x = y, x = f y 1 ...y n , Σ n i=1 a i x i = a 0 1 are called equations. The formula Σ n i=1 a i x i < a 0 1 is called inequation. Let α be a basic formula:

(1) We say that "num x is a consequence of α" iff α contains at least one of the following sub-formulas:

num x , x = y∧num y, y = x∧num y, x = -y∧num y, y = -x∧num y, z = y +x∧num z , z = x+y ∧num z , x = y +z ∧num z ∧num y, x = 0, x = 1, Σ i a i x i = a 0 1 or Σ i a i x i < a 0 1 and x is one of the x i 's.
(2) We say that "tree x is a consequence of α" iff α contains at least one of the following sub-formulas: tree x , x = y ∧ tree y, y = x ∧ tree y, x = -y ∧ tree y, y = -x ∧ tree y, x = y + z ∧ tree z , x = z + y ∧ tree z , y = x + z ∧ tree y ∧ num z , y = z + x ∧ tree y ∧ num z , x = hy 1 ...y n , with h ∈ F -{+, -, 0, 1}.

(3) We call tree-section of α the conjunction α t of the sub-formulas of α of the form:

true, tree x , -x = y or x = f y 1 ...y n , with f ∈ F -{0, 1} and where x is such that tree x is a sub-formula of α.

This tree-section α t is called formatted iff all the left-hand sides of the equations of α t are distinct and for each equation x = y of α t we have x ≻ y.

(4) We call numeric-section of α the conjunction α n of sub-fomulas of α of the form:

-true, false, Σ n i=1 a i x i = a 0 1, Σ n i=1 a i x i < a 0 1, num x , -x = y, x = -y, x = y + z, where x is such that num x is a sub-formula of α.
This numeric-section α n is called consistent iff T |= ∃x α n with x = var(α n ) and formatted iff α n does not contain sub-formulas of the form x = y, x = -y, x = y + z, 0 = a 0 1, 0 < a 0 1, with a 0 ∈ Z -α n is consistent and each leader of the equations of α n has one occurrence in only one the equations of α n and no occurrence in the inequations of α n .

(5) The variable u is called reachable in ∃xα if u is a free variable in ∃xα or α has a sub-formula of the form y = t(u) ∧ tree y with t(u) a term containing u and y a reachable variable. In the last case, the equation y = t(u) is also called reachable in ∃xα. Example: In the formula ∃xyz w = f xy ∧ z = v ∧ tree w , the variables w, v, x, y are reachable because w, v are free and x and y occur in the sub-formula w = f xy ∧ tree w . The variable z is not reachable and since z is bound and v is free, they must be such that z ≻ v. The equation w = f xy is reachable while the equation z = v is not.

We call block every basic formulas α such that for each variable x in α either num x or tree x is a sub-formula of α and α does not contain sub-formulas of the form:

-x = 0 ∧ tree x , x = 1 ∧ tree x , -x = y ∧ num x ∧ tree y, x = y ∧ tree x ∧ num y, -x = -y ∧ tree x ∧ num y, x = -y ∧ num x ∧ tree y -x = y + z ∧ num x ∧ tree y, x = y + z ∧ num x ∧ tree z , x = hȳ ∧ num x , -x = y + z ∧ tree x ∧ num y ∧ num z , -Σ n i=1 a i x i = a 0 1 ∧ tree x k , Σ n i=1 a i x i < a 0 1 ∧ tree x k with h ∈ F -{+, -, 0, 1}, k ∈ {1, ..., n}, a 0 ∈ Z and a i ∈ Z.
Since each variable x in a block is typed i.e. occurs in a sub-formula of the form num x or tree x , every block α can be divided into two disjoint sections: a tree-section and a numeric-section.

A block α without equations is called relation block. A block α without inequations and where each variable has an occurrence in at least one of the equations of α is called equation block. A block α is called solved iff its tree-section and numerical-section are formatted.

Decomposition of quantified solved blocks

Let ψ be a formula. Let x be a vector of variables and α a solved block such that for all unreachable quantified variable u in ∃xα and all reachable quantified variable v in ∃xα we have u ≻ v. We call decomposition of the formula ∃xα ∧ ψ the formula

∃x 1 α 1 ∧ (∃x 2 α 2 ∧ (∃x 3 α 3 ∧ ψ))), (1)
obtained as follows : Let X be the set of the variables in x. Let us decompose the set X into two disjoint subsets: X r (the set of the elements of X which are reachable in ∃xα) and X u . Let Lead be the set of the leaders of the equations of α. We have: -x1 is the vector of the variables of X r .

-x2 is the vector of the variables of X u -Lead.

-x3 is the vector of the variables of X u ∩ Lead.

α 1 is of the form α 1 1 ∧ α 1 2 where α 1 1 is the conjunction of all the equations in ∃xα whose leader is reachable, α 1 2 is the conjunction of all the typing constraints of α which concern variables of var(α 1 1 ). α 2 is of the form α 2 1 ∧ α 2 2 where α 2 1 is the conjunction of all the inequations of α and α 2 2 is the conjunction of all the typing constraints of α which do not concern variables of x3 .

α 3 is of the form α 3 1 ∧ α 3 2 where α 3 1 is the conjunction of the other equations and α 3 2 is the conjunction of all the typing constraints of α which concern the variables of var(α 3 1 ). The restriction on the order ≻ of the quantified unreachable and reachable variables is due to an aim to get as leader of the equations of the numeric section of α unreachable variables. If one quantified leader is reachable then we deduce that all the quantified variables of this equation are reachable. This condition will help us for the algorithm of resolution given at Section 4. The intuitions behind this decomposition come from an aim to decompose a quantified solved block into three embedded sections each one having particular properties that enable us either to remove quantifiers or make special distributions in ψ and reduce the size of the formula ∃xα ∧ ψ.

Let A be the set of the solved blocks. Let A 1 be the set of the formulas of the form ∃x 1 α 1 , where α 1 is a solved equation block and all the variables of x1 are reachable in ∃x 1 α 1 . Let A 2 be the set of the solved relation blocks.

Property 3.2.1 For all decomposed formula of the form (1) we have :

∃x 1 α 1 ∈ A 1 , α 2 ∈ A 2 , α 3 ∈ A and T |= ∀x 2 α 2 → ∃!x 3 α 3 .
Example 3.2.2 Let v, w, x, y, z be variables such that w ≻ y ≻ z ≻ x ≻ v. Let us decompose the formula

∃wxyz   v = f vx ∧ w + 2x + (-2)z = 1 ∧ y + 3z = 0∧ z < 1 ∧ 3z + 2x < 0∧ tree v ∧ num w ∧ num x ∧ num y ∧ num z   (2)
The reachable variables in the formula (2) are v and x. We have X r = {x, v}, X u = {w, y, z} and Lead = {v, w, y}. Since w ≻ y ≻ z ≻ x then the formula ( 2) is equivalent in T to the decomposed formula

  ∃x v = f vx ∧ tree v ∧ num x ∧ (∃z z < 1 ∧ 3z + 2x < 0 ∧ num z ∧ numx ∧ tree v ∧ (∃wy w+2x+(-2)z = 1 ∧ y+3z = 0 ∧ num w ∧ num x ∧ num y ∧ num z ))  
Note that the elements of A 1 does not accept elimination of quantifiers, this is due to the fact that all the variables of x1 are reachable in ∃x 1 α 1 . Indeed in the formula ∃x v = f vx the quantification ∃x can not be eliminated in T .

In all what follows we will use the notations x1 , x2 , x3 , α 1 , α 2 ,α 3 to refer to the decomposition of the formula ∃xα.

φ = ¬ k (∃x α c ∧ α p ∧ i∈I ϕ i ), (4)
has α p = true if k = 0 and satisfies the first k conditions of the following condition list if k > 0. Here α p is a solved block and is called propagated constraint section, α c is a basic formula and is called core constraint section, the ϕ i are working formulas, and in the conditions: β p ∧ β c is the conjunction of the equations and relations of the immediate top-working formula ψ of φ if it exists. i.e. ψ = ¬ k (∃ȳβ c ∧ β p ∧ φ ∧ j∈J φ j ) where φ is the formula (4) and φ j are any working formulas.

1. if ψ exists then T |= α p ∧ α c → β p ∧ β c , and the tree-sections of α p and β c ∧ β p have the same set of left-hand side of equations, 2. the tree-section of α p ∧ α c is formatted and the formula α p ∧ α c does not contain tree x ∧ num x for any variable x, 3. α p ∧ α c is a block, 4. the numeric-section of α p ∧ α c is consistent, and we have u ≻ v for u any unreachable variable in x and v any reachable variable in x, 5. α p ∧ α c is a solved block, 6. α p is the formula β c ∧ β p if ψ exists, and is the formula true otherwise. The formula α c is a solved block and for each relation num x (or tree x ) in α p , if x does not occur in an equation or inequation of α c then num x (resp. tree x ) does not occur in α c , 7.

(∃x α c ) is decomposable into (∃x 1 α c1 ∧ (∃x 2 α c2 ∧ (∃ε true))), 8. (∃x α c ) is decomposable into (∃x 1 α c1 ∧ (∃ε α c2 ∧ (∃ε true))), 9. (∃x α c ) is decomposable into (∃x 1 α c1 ∧ (∃ε true ∧ (∃ε true))).
We use k in order to be able to control the execution of our rewriting rules on working formulas. We strongly insist on the fact that ¬ k does not mean that the normalized formula satisfies only the k th condition but all the conditions i with 1 ≤ i ≤ k. We call initial working formula a working formula of the form

¬ 6 (∃ε true ∧ i∈I ϕ i )
with ϕ i working formulas where all negation symbols ¬ k have k = 0 and all propagated constraint sections are reduced to true. We call final working formula a formula of the form

¬ 7 (∃ε true ∧ i∈I ¬ 8 (∃x i α c i ∧ α p i ∧ j ∈Ji ¬ 9 (∃ȳ ij β c ij ∧ β p ij ))), (5)
where all the β c ij are different from true.

Definition 4.1.4 A general solved formula is a formula of the form

∃x 1 α 1 ∧ α 2 ∧ i∈I ¬(∃ȳ 1 i β 1 i ), ( 6
)
where

∃x 1 α 1 ∈ A 1 , α 2 ∈ A 2 , ∃ȳ 1 i β 1 i ∈ A 1 , all the α 1 ∧ α 2 ∧ β 1
i are solved blocks and all the β 1 i are different from true.

According to the properties of ¬ 8 and ¬ 9 , in the final working formula (5), α p i = true and β p ij = α p i ∧ α c i . Thus the formula ( 5) is equivalent in T to the disjunction of general solved formulas i∈I

(∃x i α c i ∧ j∈Ji ¬(∃ȳ ij β c ij )) (7)
Property 4.1.5 Let ϕ be a general solved formula of the form [START_REF] Comon | Résolution de contraintes dans des algèbres de termes[END_REF]. If ϕ has no free variables then ϕ is the formula true, otherwise neither T |= ϕ nor T |= ¬ϕ and the solutions of the free variables of ϕ are explicit.

This result is very important because it shows that for each solved formula ϕ containing at least one free variable there exists a set of solutions and a set of non-solutions, i.e. ϕ is neither true nor false in T . A similar result 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]. Note also that in all our proofs [START_REF] Dao | Solving first-order constraints in evaluated trees[END_REF] we have not used the famous independence of inequations [START_REF] Colmerauer | Equations and disequations on finite and infinite trees[END_REF][START_REF] Lassez | Unification revisited[END_REF][START_REF] Comon | Résolution de contraintes dans des algèbres de termes[END_REF][START_REF] Lassez | Independence of negative constraints[END_REF] but only the condition that the signature of T is infinite (F is infinite) which implies in this case the independence of the inequations.

Main idea

The general algorithm for solving first-order constraints in T uses a system of rewriting rules. The main idea is to transform an initial working formula of depth d into a final working formula of depth less than or equal to three. The transformation is done in two steps:

(1) The first step is a top-down simplification and propagation. In each subworking formula, α c ∧ α p is transformed to a solved block, then ∃xα c is decomposed into three parts as in subsection 3.2. The third part is eliminated and added to the core-constraint section of the immediate sub-working formulas using a special property of the quantifier ∃!. The constraints of the two other parts in α p are propagated to the propagated-constraint section of the immediate subworking formulas. In this step, the rules 1 to 24 are applied and transform the initial working formula into a working formula where each negation symbol is of the form ¬ 7 .

(2) The second step is a bottom-up simplification and elimination of quantifiers. This step is done by the rules 25 to 28. In each sub-working formula of depth one or two, the rule 25 eliminates quantified variables of the second part of the decomposition (the third one had been already removed in the first step). The rule 26 eliminates the constraints of the second part in the deepest level. Each sub-working formula of depth 3 is transformed step by step to a conjunction of working formulas of depth 2 by the rule 28 using a property of the quantifier ∃?. The transformations in this step can create new sub-working formulas where the first step needs to be done. At the end of the transformation, we obtain a final working formula of depth less than or equal to 3.

Rewriting rules

We present in Figure 1 the rewriting rules which transform an initial working formula into an equivalent final working formula. 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 all these rules, α is a basic formula, ϕ and ψ are conjunctions of working formulas.

In the rules 1 to 14, the equations and relations in α c and α p are mixed by considering the connector ∧ associative and commutative. In these rules, except the rule 6, all modifications in the right hand side are done in α c , since α p is a solved block.

In the rule 2, f and g are two distinct function symbols taken from F . The rules 4, 6, 7, are applied only if x ≻ y. This condition prevents infinite loops and makes the procedure terminating. In the rule 5, the equation x = f z 1 ...z n does not belong to α p . In the rule 6, if the equation x = f z 1 ...z n belongs to α p , then x = y ∧ tree y is moved to α p . In the rule 7, the equation x = z does not belong to α p .

In the rule 9, a 0 > 0. In the rules 13 and 14 the variable x k is the leader of the equation Σ i a i x i = a 0 1 and b k = 0. Moreover, the equation Σ j b j x j = b 0 1 does not belong to α p . In the rule 14, the relation Σ j b j x j < b 0 1 does not belong to α p and λ = 1 if a k > 0 and λ = -1 otherwise.

In the rule 15, the tree section of α c ∧ α p is formatted and there is no subformula in α c ∧ α p of the form num x ∧ tree x . In the rule 16 respectively 17, the typing constraint num z , respectively tree z is not in α c ∧α p and is a consequence of α c ∧ α p . In the rule 18, z does not have typing constraints in α c ∧ α p and neither num z nor tree z is a consequence of α c ∧ α p .

In the rule 19, α c ∧α p is a block. In the rule 20, the numeric section of α c ∧α p is inconsistent. In the rule 21, the unreachable variables in x are renamed if necessary such that u ≻ v for each unreachable variable u and each reachable variable v in x and the numeric section of α c ∧ α p is consistent. The consistency

¬ 1 (∃ū num x ∧ tree x ∧ α ∧ ϕ) =⇒ true 2 ¬ 1 (∃ū x = f ȳ ∧ x = gz ∧ tree x ∧ α ∧ ϕ) =⇒ true 3 ¬ 1 (∃ū x = x ∧ α ∧ ϕ) =⇒ ¬ 1 (∃ū α ∧ ϕ) 4 ¬ 1 (∃ū y = x ∧ tree x ∧ α ∧ ϕ) =⇒ ¬ 1 (∃ū x = y ∧ tree x ∧ α ∧ ϕ) 5 ¬ 1 ∃ū x = f y1...yn ∧ x = f z1...zn∧ tree x ∧ α ∧ ϕ =⇒ ¬ 1 ∃ū x = f y1...yn ∧ i yi = zi∧ tree x ∧ α ∧ ϕ 6 ¬ 1 ∃ū x = y ∧ x = f z1...zn∧ tree x ∧ tree y ∧ α ∧ ϕ =⇒ ¬ 1 ∃ū x = y ∧ y = f z1...zn∧ tree x ∧ tree y ∧ α ∧ ϕ 7 ¬ 1 (∃ū x = y ∧ x = z ∧ tree x ∧ α ∧ ϕ) =⇒ ¬ 1 (∃ū x = y ∧ y = z ∧ tree x ∧ α ∧ ϕ) 8 ¬ 4 (∃ū 0 = 0 ∧ α ∧ ϕ) =⇒ ¬ 4 (∃ū α ∧ ϕ) 9 ¬ 4 (∃ū 0 < a01 ∧ α ∧ ϕ) =⇒ ¬ 4 (∃ū α ∧ ϕ) 10 ¬ 4 ∃ū x = y∧ num x ∧ num y ∧ α ∧ ϕ =⇒ ¬ 4 ∃ū x + (-1y) = 0∧ num x ∧ num y ∧ α ∧ ϕ 11 ¬ 4 ∃ū x = -y∧ num x ∧ num y ∧ α ∧ ϕ =⇒ ¬ 4 ∃ū x + y = 0∧ num x ∧ num y ∧ α ∧ ϕ 12 ¬ 4 ∃ū x = y + z ∧ num x ∧ num y ∧ num z ∧ α ∧ ϕ =⇒ ¬ 4 ∃ū x + (-1y) + (-1z) = 0∧ num x ∧ num y ∧ num z ∧ α ∧ ϕ 13 ¬ 4 ∃ū Σ n i=1 aixi = a01∧ Σ n i=1 bixi = b01∧ α ∧ ϕ =⇒ ¬ 4 ∃ū Σ n i=1 aixi = a01∧ Σ n i=1 (b k ai -a k bi)xi = (b k a0 -a k b0)1∧ α ∧ ϕ 14 ¬ 4 ∃ū Σ n i=1 aixi = a01∧ Σ n i=1 bixi < b01∧ α ∧ ϕ =⇒ ¬ 4 ∃ū Σ n i=1 aixi = a01∧ Σ n i=1 λ(b k ai -a k bi)xi < (b k a0 -a k b0)1∧ α ∧ ϕ 15 ¬ 1 (∃x α c ∧ α p ∧ ϕ) =⇒ ¬ 2 (∃x α c ∧ α p ∧ ϕ) 16 ¬ 2 (∃x α c ∧ α p ∧ ϕ) =⇒ ¬ 1 (∃x num z ∧ α c ∧ α p ∧ ϕ) 17 ¬ 2 (∃x α c ∧ α p ∧ ϕ) =⇒ ¬ 1 (∃x tree z ∧ α c ∧ α p ∧ ϕ) 18 ¬ 2 (∃x α c ∧ α p ∧ ϕ) =⇒ ¬ 1 (∃x num z ∧ α c ∧ α p ∧ ϕ)∧ ¬ 1 (∃x tree z ∧ α c ∧ α p ∧ ϕ) 19 ¬ 2 (∃x α c ∧ α p ∧ ϕ) =⇒ ¬ 3 (∃x α c ∧ α p ∧ ϕ) 20 ¬ 3 (∃x α c ∧ α p ∧ ϕ) =⇒ true 21 ¬ 3 (∃x α c ∧ α p ∧ ϕ) =⇒ ¬ 4 (∃x α c ∧ α p ∧ ϕ) 22 ¬ 4 (∃x α c ∧ α p ∧ ϕ) =⇒ ¬ 5 (∃x α c ∧ α p ∧ ϕ) 23 ¬ 7 ∃x α c ∧ α p ∧ ϕ∧ ¬ 5 (∃ȳ β c ∧ β p ∧ ψ) =⇒ ¬ 7 ∃x α c ∧ α p ∧ ϕ∧ ¬ 6 (∃ȳ γ c ∧ γ p ∧ ψ) 24 ¬ 6 ∃x α c ∧ α p ∧ i ¬ 0 (∃ȳiβ c i ∧ β p i ∧ ϕi) =⇒ ¬ 7 ∃x 1 x2 α c1 ∧ α c2 ∧ α p ∧ i ¬ 1 (∃ȳi x3 γ c i ∧ γ p i ∧ ϕi) 25 ¬ 7 ∃x α c ∧ α p ∧ i∈I ¬ 9 (∃ȳiβ c i ∧ β p i ) =⇒ ¬ 8 ∃x 1 α c1 ∧ α c2 * ∧ α p ∧ i∈I ′ ¬ 9 (∃ȳiβ c i ∧ β p * i ) 26 ¬ 7 ∃x α c ∧ α p ∧ ϕ∧ ¬ 8 (∃ȳβ c ∧ β p ) =⇒ ¬ 7 (∃x α c ∧ α p ∧ ϕ ∧ ¬ 9 (∃ȳβ c1 ∧ β p ))∧ i∈I ¬ 1 (∃xȳβ p ∧ β c1 ∧ β c2 * i ∧ ϕ0) 27 ¬ 7 ∃x α c ∧ α p ∧ ϕ∧ ¬ 9 (∃εtrue ∧ β p ) =⇒ true 28 ¬ 7     ∃x α c ∧ α p ∧ ϕ∧ ¬ 8   ∃ȳ β c ∧ β p ∧ i∈I ¬ 9 (∃zi γ c i ∧ γ p i )       =⇒   ¬ 7 (∃x α c ∧ α p ∧ ϕ ∧ ¬ 8 (∃ȳ β c ∧ β p ))∧ i∈I ¬ 6 (∃xȳzi δ c i ∧ δ p i ∧ ϕ0)
  can be verified for example by using the first step of the Simplex. In the rule 22, α c ∧ α p is a solved block.

In the rule 23, γ c is obtained from β c as follows: for every variable x ∈ var(β c ), we add all the relations num x or tree x which are in β p but not in β c , and for all the variables y which do not occur in an equation or inequation of β c we remove all relations num y or tree y which are both in β c and β p . The formula γ p is the formula α p ∧ α c .

In the rule 24, ∃xα c is decomposed into

∃x 1 α c1 ∧ (∃x 2 α c2 ∧ (∃x 3 α c3 )), γ c i = β c i ∧ α c3 and γ p i = β p i ∧ α c1 ∧ α c2 ∧ α p .
The four rules 25, 26, 27 and 28 cannot be applied on the occurrence of ¬ 7 of the first level of the general working formula. In the rule 25, all the β c i are different from true, I ′ is the set of i ∈ I such that β c i does not contain occurrences of any variables in x2 . The formula α c2 * is such that T |= (∃x 2 α c2 ) ↔ α c2 * and is computed using the Fourier quantifier elimination. The propagated-constraint section β p * i = α c1 ∧ α c2 * ∧ α p . In the rule 26, ϕ is such that every negation symbol ¬ k has k ≥ 6, ϕ 0 is obtained from ϕ by replacing all occurrences of ¬ k by ¬ 0 and all propagatedconstraint sections by true. Let β 2 be the formula obtained from β c2 by removing the multiple occurrences of typing constraints and for all the variables y which do not occur in an inequation of β c2 we remove all relations num y or tree y which are both in β c1 and β c2 . If β 2 is the formula true then I = ∅, otherwise the β c2 * i with i ∈ I are obtained from β 2 as follows: Since

β 2 ∈ A 2 then it is of the form ( ℓ∈L num z ℓ ) ∧ ( k ∈K tree v k )∧ (( j∈J n i=1 a ij x i < a 0j ) ∧ n m=1 num x m ) , thus ¬β 2 is of the form   ( ℓ∈L tree z ℓ ) ∨ ( k ∈K num v k ) ∨ ( n m=1 tree x m )∨ j∈J (( n i=1 a ij x i = a 0j 1 ∧ n m=1 num x m )∨ ( n i=1 (-a ij )x i < (-a 0j )1 ∧ n m=1 num x m ))  
Each element of this disjunction is a block and represents a formula β c2 * i . Of course we have T |= (¬β 2 ) ↔ i β c2 * i . In the rule 28, I = ∅, ϕ is such that every negation symbol ¬ k has k ≥ 6, ϕ 0 is obtained from ϕ by replacing all occurrences of ¬ k by ¬ 0 and all propagatedconstraint sections by true. Moreover δ p i = α p and δ

c i = γ c i ∧ β c ∧ α c .
Property 4.3.1 Every repeated application of the precedent rewriting rules on an inital working formula terminates and produces an equivalent final working formula which does not contain new free variables.

Corollary 4.3.2 Every formula is equivalent in T either to true or to false or to a disjunction of general solved formulas, having at least one free variable, being equivalent neither to true nor to false in T and where the solutions of the free variables are expressed in a clear and explicit way.

In fact, solving a constraint ϕ in T proceeds as follows:

1. Transform ϕ into a normalized formula, then into an initial working formula φ, which is equivalent to ϕ in T . 2. Transform φ into a final working formula ψ using the rewriting rules defined in the subsection 4.3. 3. Extract from ψ the equivalent disjunction of general solved formulas. If this disjunction contains the general solved formula true, then it is reduced to true.

Example: Let ϕ be the following constraint having i, j as free variables:

∃x x = f ij ∧ i > 0 ∧ tree x ∧ num i ∧ num j ∧ ¬(∃k j = 2k ∧ num k ).
We can see that num j ∧ ¬(∃k j = 2k ∧ num k ) is always false in T since for every variable j, there exists a unique variable k such that j = 2k (axiom 13n). Let us transform ϕ into an initial working formula (the propagated-constraint sections are underlined):

¬ 6 ¬ 0 (∃x x = f ij ∧ i > 0 ∧ tree x ∧ num j ∧ true ∧ ¬ 0 (∃k j = 2k ∧ num k ∧ true))
After having applied the rules [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF][START_REF] Jouannaud | Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification[END_REF][START_REF] Lassez | Unification revisited[END_REF][START_REF] Jouannaud | Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification[END_REF][START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF][START_REF] Martelli | An efficient unification algorithm[END_REF][START_REF] Paterson | Linear unification[END_REF][START_REF] Ramachandran | Incremental algorithms for constraint solving and entailment over rational trees[END_REF] in this order, we obtain: ¬ 7 ¬ 6 (∃x x = f ij ∧ i > 0 ∧ tree x ∧ num i ∧ num j ∧ true ∧ ¬ 0 (∃k j = 2k ∧ num k ∧ true))

The rule 24 being applied changes the formula to:

¬ 7 ¬ 7   i > 0 ∧ num i ∧ num j ∧ true∧ ¬ 1 ∃xk x = f ij ∧ j = 2k ∧ num k ∧ tree x ∧ i > 0 ∧ num i ∧ num j  
After having applied on the sub-working formula ¬ 1 (...) the rule 15, 19, 21, 12, 22, 23

¬ 7 ¬ 7   i > 0 ∧ num i ∧ num j ∧ true∧ ¬ 6 ∃xk x = f ij ∧ j -2k = 0 ∧ num k ∧ tree x ∧ i > 0 ∧ num i ∧ num j  
The rule 24 is applied then we obtain:

¬ 7 ¬ 7 (i > 0 ∧ num i ∧ num j ∧ true ∧ ¬ 7 (true ∧ i > 0 ∧ num i ∧ num j ))
The rules 25, 26 are applied in this order, giving:

¬ 7 ¬ 7 (i > 0 ∧ num i ∧ num j ∧ true ∧ ¬ 9 (true ∧ i > 0 ∧ num i ∧ num j ))
Finally, by application of the rule 27, we obtain the final working formula ¬ 7 true, which is equivalent to the empty disjunction of general solved formulas, i.e. false. Thus, the initial constraint ϕ is false in T and does not depend on the values of its free variables i and j. A such phenomena is impossible to detect using a decision procedure instead of a first-order constraint solver.

Conclusion

Quantified formulas over trees and rational numbers provide an expressive constraint language that is essential in applications such as program analysis and model checking. We have presented in this paper a first-order constraint solver in the theory of the evaluated trees. The algorithm is given in the form of 28 rewriting rules and its correctness implies the completeness of a theory built on the model of Prolog III. Our aim in this work was not only to decide proposition i.e. to decide if a formula without free variables is true or false in T but to express the solutions of any first-order constraint having free variables in a clear and explicit way. 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 trees is non-elementary, i.e. the complexity of all algorithms which solve it cannot be bound by a tower of powers of 2 ′ s (with a top down evaluation) with a fixed height. Thus, our algorithm must not escape this kind of complexity in the worst case. This is why we have used two strategies in the algorithm: a top down propagation of constraints and a bottom-up elimination of quantifiers and distribution. This technique can quickly detect (using propagation and local solving) sub-formulas which are equivalent to false and prevents us from solving a big working formula (i.e. a working formula of huge depth) which contradicts its top-working formula. We have recently programmed a similar algorithm only on the theory of finite or infinite trees and in spite of the high complexity we can solve formulas on two partners games involving 160 nested quantifiers [START_REF] Djelloul | Solving First-Order formulas in the Theory of Finite or Infinite Trees[END_REF].

Currently, we are trying to find other classes of theories T i such that we can apply a similar technique to solve first-order constraints in the hybrid theories T i + T rees. We are also working on a possibly CHR (Constraint Handling Rules) implementation of our solver.

4. 1 Property 4 . 1 . 2

 1412 Working and general solved formulas Definition 4.1.1 A normalized formula ϕ of depth d ≥ 1 is a formula of the form ¬(∃x α ∧ i∈I ϕ i ), (3) with I a finite (possibly empty) set, α a basic formula and the ϕ i normalized formulas of depth d i and d = 1 + max{0, d 1 , ..., d n }. Every formula is equivalent in T to a normalized formula. Definition 4.1.3 A working formula is a normalized formula in which all the occurrences of ¬ are of the form ¬ k with k ∈ {0, ..., 9} and such that each occurrence of a sub-formula of the form

Fig. 1 .

 1 Fig. 1. The rewriting rules 1¬ 1 (∃ū num x ∧ tree x ∧ α ∧ ϕ) =⇒ true 2 ¬ 1 (∃ū x = f ȳ ∧ x = gz ∧ tree x ∧ α ∧ ϕ) =⇒ true 3 ¬ 1 (∃ū x = x ∧ α ∧ ϕ) =⇒ ¬ 1 (∃ū α ∧ ϕ) 4 ¬ 1 (∃ū y = x ∧ tree x ∧ α ∧ ϕ) =⇒ ¬ 1 (∃ū x = y ∧ tree x ∧ α ∧ ϕ)

Acknowledgements We thank Alain Colmerauer for our many discussions and his help in this work. We dedicate to him this paper.


Khalil Djelloul
email: khalil.djelloul@uni-ulm.de

Thi-Bich-Hanh Dao
email: dao@lifo.univ-orleans.fr

Thom Fruehwirth
email: thom.fruehwirth@uni-ulm.de

Toward a First-Order Extension of Prolog's Unification using CHR A CHR First-Order Constraint Solver Over Finite or Infinite Trees

Keywords: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic-Logic and Constraints Programming; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving-Deduction, Logic Programming Algorithms, Theory Prolog, Unification, CHR (Constraint Handling Rules), Theory of finite or infinite trees, First-order constraints solving

Prolog, which stands for PROgramming in LOGic, is the most widely used language in the logic programming paradigm. One of its main concepts is unification. It represents the mechanism of binding the contents of variables and can be seen as solving conjunctions of equations over finite or infinite trees. We present in this paper an idea of a first-order extension of Prolog's unification by giving a general algorithm for solving any first-order constraint in the theory T of finite or infinite trees, extended by a relation which allows to distinguish between finite and infinite trees. The algorithm is given in the form of 16 rewriting rules which transform any first-order formula ϕ into an equivalent disjunction φ of simple formulas in which the solutions of the free variables are expressed in a clear and explicit way. We end this paper describing a CHR implementation of our algorithm. CHR (Constraint Handling Rules) has originally been developed for writing constraint solvers, but the constraints here go much beyond implicitly quantified conjunctions of atomic constraints and are considered as arbitrary first-order formulas built on the signature of T . We discuss how we implement nested local constraint stores and what programming patterns and language features we found useful in the CHR implementation of our algorithm.

INTRODUCTION

Prolog, which stands for PROgramming in LOGic [START_REF] Roussel | Prolog : Manuel de Reference et d'Utilisation[END_REF][START_REF] Colmerauer | Prolog, Theoretical Basis and Current Developments[END_REF], is the most widely used language in the logic programming paradigm. Prolog is based on first-order predicate calculus over Horn clauses and the execution of a Prolog program is an application of theorem proving by first-order resolution. The fundamental concepts behind Prolog are unification, tail recursion and backtracking.

The core of Prolog, namely Alan Robinson's unification algorithm [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF] is a mechanism of binding the contents of variables and can be viewed as a one-time assignment. This operation is represented in Prolog by the symbol "=". For example, the unification f (g(a)) = f (x) is possible by binding the variable x to the term g(a). A. Colmerauer has then incorporated into the first extension of Prolog, known as Prolog II, the unification of infinite terms [START_REF] Colmerauer | Prolog and infinite trees[END_REF][START_REF] Colmerauer | Equations and inequations on finite and infinite trees[END_REF] and has shown that unifications of the form x = f (x) are possible by binding the variable x to the infinite term f (f (f (...))).

One of the most significant innovations in Prolog was done in Prolog III and IV [START_REF] Colmerauer | An introduction to Prolog III[END_REF][START_REF] Benhamou | Le manuel de Prolog IV[END_REF] where the concept of unification was replaced by the concept of constraint solving over finite or infinite trees. However, the internal solvers of Prolog III and IV are not able to solve arbitrary quantified first-order constraints over finite or infinite trees.

In this paper, we present two contributions:

(1) A theoretical contribution: First of all, we extend the signature of Maher's theory of finite or infinite trees [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF] 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, not only a decision procedure, but a full first-order constraint solver which for every first-order formula gives an equivalent solved formula in which the solutions of the free variables are expressed in a clear and explicit way. The main ideas behind this solver come from the works of T. Dao [START_REF] Dao | Resolution de contraintes du premier ordre dans la theorie des arbres finis ou infinis[END_REF] on the theory of finite or infinite trees.

(2) A practical contribution which consists in a full CHR implementation of our algorithm. Constraint Handling Rules (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 | CHR Website[END_REF] is a concurrent committedchoice constraint logic programming language consisting of guarded rules that transform multi-sets of atomic formulas (constraints) into simpler ones until exhaustion. CHR was initially developed for solving constraints, but has matured into a general-purpose concurrent constraint language over the last decade, because it can embed many rule-based formalisms and describe algorithms in a declarative way. Moreover, the clean semantics of CHR facilitates non-trivial program analysis and transformation. The power and complexity of the 16 rules of our solver posed a challenge for CHR and its programmer. We show how to implement nesting of local constraint stores in CHR, as well as the debated negation-as-absence (the correspondence to negationas-failure in Prolog). We distinguish between operation and data constraints and encode necessary control (phases of the algorithm) in constraints relying on the refined operational semantics of CHR systems.

The paper is organized in four sections followed by a conclusion. This introduction is the first section. In Section 2, we present our 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. In section 3, we present structured formulas that we call working formulas and show some of their properties. We end this section by a general algorithm solving any first-order constraint in T . This algorithm handles our working formulas and is given in the form of 16 rewriting rules. It transforms any firstorder formula into a disjunction of simple formulas in which 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, we present in Section 4 our CHR implementation and show how to implement the complex nested structure of our working formulas as well as the different controls which enable the algorithm to move from one phase to another.

THE THEORY T OF FINITE OR INFI-NITE TREES

Syntax

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 with 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 (t1, . . . , tn),

or a formula, i.e. of one of the eleven forms: s = t, r(t1, . . . , tn), true, false, ¬ϕ, (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ), (ϕ ↔ ψ), (∀x ϕ), (∃x ϕ).

(2) In (1), x is taken from V, f is an n-ary function symbol taken from S and the ti's are shorter terms. In (2), s, t and the ti's are terms, r is an n-ary relation symbol taken from S and ϕ and ψ are shorter formulas. 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, x0 = x1, x0 = f (x1, ..., xn), r(x1, ..., xn), where all the xi'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. We will also use the quantifiers ∃? (at most one) and ∃! (one and only one).

Axioms

Let F be a set of function symbols containing an infinity of distinct n-ary function symbols which are not constants 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(ȳ)) ∀x∀ȳ f (x) = f (ȳ) → V i xi = yi ∀x∃!z V i zi = ti[xz] ∀x∀u ¬(u = t[u, x] ∧ finite(u)) ∀x∀u (u = f (x) ∧ finite(u)) ↔ (u = f (x) ∧ V i finite(xi))
where f and g are distinct function symbols taken from F , x is a vector of possibly non-distinct variables xi, ȳ is a vector of possibly non-distinct variables yi, z is a vector of distinct variables zi, ti[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.

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. A more general decision procedure was recently proposed by K. Djelloul in the frame of decomposable theories [START_REF] Djelloul | Decomposable theories[END_REF].

SOLVING FIRST-ORDER CON-STRAINTS IN T

Normalized and working formulas

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: (1) The quantified variable of ϕ have distinct names that are different from those of the free variables. (2) For all variables x, y and all sub-formulas ϕi of ϕ, if y has a free occurrence in ϕi and x has a bound occurrence in ϕi then x ≻ y. We show 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 ϕ. Definition 3.1.1. Let v1, ..., vn, u1, ..., um be variables. A basic formula is a formula of the form

( n î=1 vi = ti) ∧ ( m î=1 finite(ui)) (3)
in which all the equations vi = ti are flat. Note that if n = m = 0 then (3) is reduced to true. The basic formula [START_REF] Colmerauer | Prolog and infinite trees[END_REF] is called solved if all the variables v1, ..., vn, u1, ..., um are distinct and for each equation of the form x = y we have x ≻ y. If α is a basic formula then we denote by: (i) Lhs(α) the set of the variables which occur in the left hand sides of the equations of α. (ii) F IN I(α) the set of the variables which occur in a sub-formula of α of the form finite(x).

Definition 3.1.2. Let α be a basic formula and x a vector of variables. The reachable variables and equations of α from the variable x0 are those which occur in a sub-formula of α of the form:

x0 = t0(x1) ∧ x1 = t1(x2) ∧ ... ∧ xn-1 = tn-1(xn),
where xi+1 occurs in the term ti(xi+1). The reachable variables and equations of ∃x α are those which are reachable in α from the free variables of ∃x α.

A sub-formula of α of the form finite(u) is called reachable in ∃x α if u ∈ x or u is a reachable variable of ∃x α. Definition 3.1.3. A normalized formula ϕ of depth d ≥ 1 is a formula of the form ¬(∃x α ∧ V i∈I ϕi)
, with I a finite (possibly empty) set, α a basic formula and the ϕ ′ i s normalized formulas of depth di with d = 1 + max{0, d1, ..., dn}.

Property 3.1.4. Every formula ϕ is equivalent in T to a normalized formula. Definition 3.1.5. A general solved formula is a normal- ized formula of the form ¬(∃x α∧ V 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 are reachable in ∃x α.

4. For all i ∈ {1, ..., n}, all the variables of ȳi are reachable in ∃ȳi βi.

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 α.

Property 3.1.6. Let ϕ be a general solved formula. If ϕ has no free variables then ϕ is the formula ¬(∃ε true) else neither T |= ¬ϕ nor T |= ϕ. Definition 3.1.7. 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, (4)
satisfies the k first conditions of the condition list bellow. In [START_REF] Colmerauer | Prolog, Theoretical Basis and Current Developments[END_REF] α is a basic formula, q is a conjunction of working formulas of the form V n i=1 ¬ k i (∃ȳi βi ∧ qi), with n ≥ 0, βi a basic formula, qi a conjunction of working formulas, and in the below condition list α ′ is the basic formula of the immediate top-working formula 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(α).

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 α.

An initial 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 .

Property 3.1.8. Let p be the final formula

¬ 5 (∃x α ∧ V n i=1 ¬ 5 (∃ȳi βi) The formula ¬(∃x α ∧ V 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 α.

The Rules

We present in Fig 1 . the rewriting rules which transform an initial working formula of any depth d to a conjunction of final formulas, equivalent in T . In these rules 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. Moreover, u ≻ v, f and g are 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 (x1, ..., xn) with f an n-ary function symbol taken from F . In rule [START_REF] Colmerauer | An introduction to Prolog III[END_REF], the equations of a have distinct left hand sides and for each equation of the form u = v we have u ≻ v. In rule [START_REF] Djelloul | Decomposable theories[END_REF], the variable u is reachable from u in a. In rule [START_REF] Duck | The Refined Operational Semantics of Constraint Handling Rules[END_REF], the variable u is non-reachable from u in a. Moreover, if f is a constant then n = 0. In rule [START_REF] Fruehwirth | Theory and Practice of Constraint Handling Rules[END_REF], a is a solved basic formula. In rule [START_REF] Fruehwirth | Parallelizing Union-Find in Constraint Handling Rules Using Confluence[END_REF], 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 [START_REF] Meister | Complexity of the CHR Rational Tree Equation Solver[END_REF], n ≥ 0 and for all i ∈ {1, ..., n} the formula bi 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.

(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 ∧ V 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) ∧ V 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 ∧ V n i=1 ¬ 5 (∃ȳi bi)) =⇒ ¬ 5 (∃x ′ a ′ ∧ V i∈K ¬ 5 (∃ȳ ′ i b ′ i ) * ) (16) ¬ 4 2 6 6 4 ∃x a ∧ q∧ ¬ 5
" ∃ȳ b∧

V n i=1 ¬ 5 (∃zi ci) # 3 7 7 5 =⇒ " ¬ 4 (∃x a ∧ q ∧ ¬ 5 (∃ȳ b))∧ V n i=1 ¬ 4 (∃xȳ zi ci ∧ q0) * # Fig 1.
Transformation of an initial working formula into a final working formula.

• x′′ is the vector the variables of x which are nonreachable in ∃x a and do not occur in the left hand sides of the equations of a.

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

• a ′′′ is the conjunction of the equations which are nonreachable in ∃x a.

• b * i is the formula obtained by removing from bi 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 V i∈K ¬ 5 (∃ȳ ′ i b ′ i ) * is the formula V 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 [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF], n > 0 and q0 is the formula q in which all the occurrences of ¬ k have been replaced by ¬ 0 . The formula

V n i=1 ¬ 4 (∃xȳzi ci ∧ q0) * is the formula V n i=1 ¬ 4 (∃xȳzi ci ∧ q0
) in which we have renamed the quantified variables so that they satisfy the discipline of the formulas of T .

The main idea behind this algorithm consists in (i) a topdown simplification and propagation of constraints. In each level, quantified basic formulas are locally solved by the rules (1)... [START_REF] Fruehwirth | Theory and Practice of Constraint Handling Rules[END_REF] and propagated to the embedded sub-formulas by rule [START_REF] Fruehwirth | Essentials of Constraint Programming[END_REF]. Finiteness is checked by rule (9), inconsistent sub-formulas are removed by rule [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF] and basic formulas are restored by rule [START_REF] Fruehwirth | Parallelizing Union-Find in Constraint Handling Rules Using Confluence[END_REF]. (ii) a bottom-up elimination of quantifiers and reduction of the depth of working formulas done by the rules ( 15) and ( 16). Property 3.2.1. Every repeated application of our rewriting rules on an initial working formula p terminates and produces a conjunction of final formulas equivalent to p in T .

The Solving Algorithm

Let p any formula. Solving p in T proceeds as follows:

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

(2) Transform p1 into the following working formula p2

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

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

V n i=1 ¬ 5 (∃xi αi ∧ V n i j=1 ¬ 5 (∃ȳij βij)).
According to Property 3.1.8, the formula p3 is equivalent in T to the following wnfv conjunction p4 of general solved formulas

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

p is equivalent in T to ¬ V n i=1 ¬(∃xi αi ∧ V n i j=1 ¬(∃ȳij β * ij )), which is equivalent to the following disjunction p5 n _ i=1 (∃xi αi ∧ n i ĵ=1 ¬(∃ȳij β * ij )).
This is the solved form of the formula p where the solutions of the free variables are expressed in a clear and explicit way. Moreover, according to the form of p2 and using the properties 3.1.6 and 3.1.8, we show that if T |= p then p5 is the formula ∃ε true, and if T |= ¬p then p5 is the formula false (obtained with n = 0, i.e. the empty disjunction). We can now present our main theorem, from which we deduce the completeness of T :

Theorem 3.3.1. Every formula is equivalent in T either to true, or to false, or to a disjunction of general solved formulas 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.

IMPLEMENTATION OF OUR ALGO-RITHM

Our 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, almost all of them belonging to computations for the complicated rules ( 15) and ( 16) of our algorithm. 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. 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/.

Constraint Handling Rules (CHR) Implementation

Execution of CHR

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 | CHR Website[END_REF] manipulates constraints that reside in a constraint store. It contains all information necessary for computation. Let H, C and B denote conjunctions of constraints. A simplification rule H ⇔ C B replaces instances of the CHR constraints H by B provided the guard 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: H1\H2 ⇔ C B removes macthed constraints H2 but keeps constraints H1.

The constraints of the store comprise the state of an execution. Starting from an arbitrary initial store/state (also called goal, query, problem), CHR rules are applied exhaustively, until a fixpoint is reached. If new constraints arrive, rules are reconsidered for application. A final store/state (also called answer, solution) is one where either no rule application is possible anymore or where the constraints are inconsistent.

In more detail, a rule is applicable, if its head constraints are matched by constraints in the current goal one-by-one and if, under this matching, the guard of the rule is logically implied by the constraints in the store. Any of the applicable rules can be applied, and the application cannot be undone, it is committed-choice. Trivial non-termination of propagation rule applications is avoided by applying a propagation rule at most once to the same constraints [START_REF] Abdennadher | Operational Semantics and Confluence of Constraint Propagation Rules[END_REF].

As in Prolog, 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 in the order they are written, and when it matches a head constraint of a rule, it will look for the other, partner constraints of the head in the constraint store and check the guard until an applicable rule is found. We consider such a constraint to be active. If the active constraint has not been removed after trying all rules, it will be put into the constraint store. Constraints from the store will be reconsidered (woken) if newly added constraints constrain variables of the constraint, because then rules may become applicable since their guards now hold.

CHR Constraints

The implementation consists of 18 constraints: 2 main constraints that encode the tree data structure of the working formulas and the atomic formulas, 9 auxiliary constraints that perform reachability analysis, variable renaming and copying of formulas, and 7 constraints that encode execution control information, mainly for rules [START_REF] Meister | Complexity of the CHR Rational Tree Equation Solver[END_REF] and [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF].

The two main constraints are nf/4 for the negated quantified basic formulas and of/2 for the equations and the relation finite. In more detail, nf(ParentId,Id,Phase,ExVars) describes a negated quantified basic formula with its Id and the Id of its parent node, the phase it is in 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 ) that belongs to the negated sub-formula with the identifier Id.

For identifiers and problem variables, logical variables are used. The main reason is that most CHR implementations index on logical variables and that new logical variables can be introduced by just using them. The order on the problem variables is implemented by using a built-in ordering mechanism of CHR in Sicstus Prolog, that will order the logical variables chronologically in the order of their introduction. This implies that the nf/4 constraints have to be introduced in a top-down manner.

It is easy to represent any working formula ϕ using conjunctions of nf/4 and of/2 constraints. For that, 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. An example is given in Fig 2.

CHR Rules

In our algorithm, we can distinguish two main parts that are iterated until a solved normal form is reached: (i) In the first part, given a formula (local store), the equations of its parent are copied into it by rule [START_REF] Fruehwirth | Essentials of Constraint Programming[END_REF], then the local store is simplified by rules (1) to ( 5), finiteness is checked by rules ( 6) to [START_REF] Fruehwirth | Theory and Practice of Constraint Handling Rules[END_REF], and finally rule (13) replaces certain local equations by their counterpart equations from the parent. (ii) In the second part, rule ( 14), ( 15) and ( 16) apply and change the structure of the formula in a significant way by copying sub-formulas.

In part 1, when we consider the phase labels of the nf/4 CHR constraint, in the initial formula, the top-most formula will have phase 4 and all sub-formulas the level 0. The computation is triggered by the presence of the top-most formula together with a direct sub-formula. When rules (1) to [START_REF] Fruehwirth | Parallelizing Union-Find in Constraint Handling Rules Using Confluence[END_REF] have been applied to it, the sub-formula will also be at phase 4 and can now in turn trigger the simplification of the equations in its direct sub-formulas. This means that in part 1, computation proceeds top-down in the tree repre- .

¬ 0 (∃ε u = s(v))∧ ¬ 0 (∃w1 u = s(w1) ∧ w1 = s(v))∧ ¬ 5 (∃ε v = s(u) ∧ u = 1 ∧ » ¬ 5 (∃ε v = s(u) ∧ u = 1 ∧ finite(w1))∧ ¬ 5 (∃w3 v = s(u) ∧ u = 1 ∧ w2 = s(w3) ∧ finite(w3)) - ) 3
The preceding working formula can be expressed using the following conjunction of constraints:

nf(Q, P1, 4, [U]), U = 1 of P1, nf(P1, P2, 0, [ ]), U = S(V) of P2, nf(P1, P3, 0, [W1]), U = S(W1) of P3, W1 = S(V) of P3, nf(P1, P4, 5, [ ]), V = S(U) of P4, U = 1 of P4 nf(P4, P5, 5, [ ]), V = S(U) of P5, U = 1 of P5, finite(W1) of P5 nf(P4, P6, 5, [W3]), V = S(U) of P6, U = 1 of P6, W2 = S(W3) of P6, finite(W3) of P6
senting the structure of the nested formulas. At the end of part 1, all formulas will be in phase 4.

The rules of part 1, i.e. ( 1) to [START_REF] Fruehwirth | Parallelizing Union-Find in Constraint Handling Rules Using Confluence[END_REF], have a rather direct translation into CHR rules.

% 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) | P=true. (5) @ nf(Q,P,1,Xs), U=F of P \ U=G of P <=> samefunctor(F,G) | same_args(F,G,P). % 1-2 enter next phase after solving (6) @ nf(Q,P,1,Xs) <=> nf(Q,P,2,Xs). % rules for finite/2 (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).

% 2-3 enter next phase after finiteness check (11) @ nf(Q,P,2,Xs) <=> nf(Q,P,3,Xs). % 4/0-4/1 copy down before solving (12a) @ nf(Q,P,4,Xs), A of P, nf(P,P1,0,Ys) ==> A of P1. (12b) @ nf(Q,P,4,Xs) \ nf(P,P1,0,Ys) <=> nf(P,P1,1,Ys). % 4/3-4/4 replace down after solving (13a) @ nf(Q,P,4,Xs),U=V of P, nf(P,P1,3,Ys)\ U=G of P1 <=> V\==G | U=V of P1.

(13b)@ nf(Q,P,4,Xs) \ nf(P,P1,3,Ys) <=> nf(P,P1,4,Ys).

Note that rules (1) to ( 5) are a direct implementation of an 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]. These rules are similar to the more general rational tree solver that is a classical example for CHR code. By applying results of [START_REF] Meister | Complexity of the CHR Rational Tree Equation Solver[END_REF], we can show that the worst-case time complexity of the rules in the first part of the algorithm is quadratic in the size of the equations in the local formula.

In the rules (2) and (3), the predicate gt(U,V) is used to check if we have U ≻ V. In the rules (4) and ( 5), the predicates samefunctor(F,G) and notsamefunctor(F,G) are used to check if the terms F and G start by same or distinct function symbols. Note also that in rule (4) we let P=true. Binding the identifier P removes all equations from the local store associated with it using a simplification rule E of true <=> true. Instead of relying on Prolog's built-in syntactic equality =, we could also have used a CHR constraint, say remove(P) to the same effect.

In rule (9+10) reach args(U,T,P) checks reachability of U from itself in P. If so, P wil be set to true and thus the local store will be removed, implementing rule [START_REF] Djelloul | Decomposable theories[END_REF]. Otherwise, if P is still free, the subsequent finite args(U,T,P) will propagate down the finite relation from U to its arguments, implementing rule [START_REF] Duck | The Refined Operational Semantics of Constraint Handling Rules[END_REF].

Part 2, on the contrary to part 1, proceeds bottom-up, starting at the leaves (with n = 0 in rule ( 15)). Leaf formulas go from phase 4 to 5. Each formula with a phase 4 formula as the top one and only phase 5 formulas as subformulas are rewritten in part 2 (with n = 0 in rule ( 15)) into formula with phase 5 formula as top-formula and only phase 5 formulas as sub-formulas. In rule [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF], formulas may be copied and the new formulas are introduced with phase 4 and 0 (all the n¬ k of q are changed into ¬ 0 ) which causes a local application of part 1 of the algorithm and so on. The phase change continues going up in the tree structure of the working formulas until all working formulas are in phase 5 and have a depth less or equal to 2.

A more or less direct translation of rules of the algorithm was sufficient so far, but it is by far not sufficient for the rules ( 14) to ( 16) of part 2 of the algorithm. For rule [START_REF] Maher | Complete axiomatization of the algebra of finite, rational and infinite trees[END_REF]:

¬ 4 (∃x a ∧ q ∧ ¬ 5 (∃ȳ a)) =⇒ true,
the implementation is easy when nested negation-as-absence is used to verify that there is no constraint in the subformula that is not in the main formula. Negation-asabsence can be directly encoded in CHR implementations, but then it requires two additional rules per negation. Instead, we have chosen to use the CHR library builtin find constraint(Var,Pattern,Match) of the Sicstus-Prolog CHR library that returns on backtracking all constraints Match that match the Pattern and that are indexed on the variable Var together with negation-as-failure provided by the Prolog built-in \+. For the rules ( 15) and ( 16), all primed expressions have to be computed, some quantified variables must be renamed and many nf/4 constraints and their equations should be copied and updated. 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. This is by far the most complicated and extensive part of our CHR implementation which was finally done using 40 CHR rules. In order no to overburden the reader with technical details, we omit the description of those 40 rules in this article.

CONCLUSION

We presented in this paper two contributions : (1) A general algorithm solving any first-order constraint in an extended theory T of finite or infinite trees. The algorithm is in the form of 16 rewriting rules and its correctness implies the completeness of T . (2) A full CHR implementation of our algorithm. We discussed programming patterns for maintaining a hierarchy of local stores and for control using phases by constraints, and desirable program features like the debated negation-as-absence. Simpagation rules proved useful to perform iterations that modify the constraint store.

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 shown that the complexity of all algorithms solving first-order constraints over finite or infinite trees has a non-elementary complexity. This is why we have used two strategies in the algorithm: a top down propagation of constraints and a bottom-up elimination of quantifiers and distribution. This technique enables us to remove the inconsistent working formulas and to not lose time with solving huge working formulas which contradict their top-working formulas.

Future work will aim at an even more declarative implementation that is directly amenable to established CHR analysis techniques for termination, complexity and confluence properties. We 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 get 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].

So far, the CHR implementation has not been optimized. To improve efficiency we could enforce the data-only nature of the equations (the constraint of/2) by declaring it passive in each rule. This compiler pragma of CHR in Sicstus Prolog avoids to generate code for the occurrence of a passive constraint in the head of the rule. Another direction would be to enable input and output of formulas in latex, based on the work of literate CHR. This will enable us to test easily our algorithm on big examples and compare the performances with those obtained using a decision procedure for decomposable theories [START_REF] Djelloul | Decomposable theories[END_REF].

Fig 2 .

 2 Fig 2. An example of a working formula expressed using the constraints of/2 and nf/4.

4/ 5 -

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

Acknowledgments Khalil Djelloul thanks the DFG research project GLOB-CON for funding and supporting his research. Particular thanks also to Marc Meister and Hariolf Betz for their kind reviews of this article.