Khalil Djelloul

Thi-Bich-Hanh Dao

Extension of First-Order Theories into Trees

We present in this paper an automatic way to combine any first-order theory T with the theory of finite or infinite trees. First of all, we present a new class of theories that we call zero-infinite-decomposable and show that every decomposable theory T accepts a decision procedure in the form of six rewriting rules which for every first order proposition give either true or false in T . We present then the axiomatization T * of the extension of T into trees and show that if T is flexible then its extension into trees T * is zero-infinite-decomposable and thus complete. The flexible theories are theories having elegant properties which enable us to eliminate quantifiers in particular cases.

Introduction

The theory of finite or infinite trees plays a fundamental role in programming. Recall that Alain Colmerauer has described the execution of Prolog II, III and IV programs in terms of solving equations and disequations in this theory [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 | the manuel of Prolog IV[END_REF]. He has first introduced in Prolog II the unification of infinite terms together with a predicate of non-equality [START_REF] Colmerauer | A view of the origins and development of Prolog[END_REF]. He has then integrated in Prolog III the domain of rational numbers together with the operations of addition and subtraction and a linear dense order relation without endpoints [START_REF] Colmerauer | Total precedence relations[END_REF][START_REF] Colmerauer | Prolog in 10 figures[END_REF]. He also gave a general algorithm to check the satisfiability of a system of equations, inequations and disequations on a combination of trees and rational numbers. Finally, in Prolog IV, the notions of list, interval and boolean have been added [START_REF] Colmerauer | Specification of Prolog IV[END_REF][START_REF] Benhamou | the manuel of Prolog IV[END_REF].

We present in this paper an idea of a general extension of the model of Prolog IV by allowing the user to incorporate universal and existential quantifiers to Prolog closes and to decide the validity or not validity of any first-order proposition (sentence) in a combination of trees and first-order theories. For that:

(1) we give an automatic way to generate the axiomatization of the combination of any first order theory T with the theory of finite or infinite trees,

(2) we present simple conditions on T and only on T so that the combination of T with the theory of finite or infinite trees is complete and accepts a decision algorithm in the form of six rewriting rules which for every proposition give either true or false.

One of major difficulties in this work resides in the fact that the two theories can possibly have non-disjoint signatures. Moreover, the theory of finite or infinite trees does not accept full elimination of quantifiers.

The emergence of general constraint-based paradigms, such as constraint logic programming [START_REF] Jaffar | Constraint logic programing: a survey[END_REF], constrained resolution [START_REF] Burckert | A resolution principle for constraint logics[END_REF] and what is generally referred to as theory reasoning [START_REF] Baumgartner | A unified approach to theory reasoning[END_REF], rises the problem of combining decision procedure for solving general first order constraints. Initial combinations results were provided by R. Shostak in [START_REF] Shostak | A practical decision procedure for arithmetic with function symbols[END_REF] and in [START_REF] Shostak | Deciding combinations of theories[END_REF]. Shostak's approach is limited in scope and not very modular. A rather general and completely modular combination method was proposed by G. Nelson and D. Oppen in [START_REF] Nelson | Simplification by co-operating decision procedures[END_REF] and then slightly revised in [START_REF] Nelson | Combining satisfiability procedures by equality sharing[END_REF]. Given, for i = 1, ..., n a procedure P i that decides the satisfiability of quantifierfree formulas in the theory T 1 ∪ ... ∪ T n . A declarative and non-deterministic view of the procedure was suggested by Oppen in [START_REF] Oppen | Complexity, convexity and combinations of theories[END_REF]. In [START_REF] Tinelli | A new correctness proof for the Nelson-Oppen combination procedure[END_REF], C. Tinelli and H.Harandi followed up on this suggestion describing a non-deterministic version of the Nelson-Oppen approach combination procedure and providing a simpler correctness proof. A similar approach had also been followed by C. Ringeissen in [START_REF] Ringeissen | Combinaison de resolution de contraintes[END_REF] which describes the procedure as a set of a derivation rules applied nondeterministically.

All the works mentioned above share one major restriction on the constraint languages of the component reasoners: they must have disjoint signatures, i.e. no function and relation symbols in common. (The only exception is the equality symbol which is however regarded as a logical constant). This restriction has proven really hard to lift. A testament of this is that, more than two decades after Nelson and Oppen's original work, their combination results are still state of the art.

Results on non-disjoint signatures do exists, but they are quit limited. To start with, some results on the union of non-disjoint equational theories can be obtained as a byproduct of the research on the combination of term rewriting systems. Modular properties of term rewriting systems have been extensively investigated (see the overviews in [START_REF] Ohelbush | Modular properties of composable term rewriting systems[END_REF] and [START_REF] Gramlich | On termination and confluence properties of disjoint and constructor sharing conditional rewrite systems[END_REF]). Using some of these properties it is possible to derive combination results for the word problem in the union of equational theories sharing constructors 3 . Outside the work on modular term rewriting, the first combination result for the word problem in the union of non-disjoint constraint theories were given in [START_REF] Domenjoud | Combination techniques for nondisjoint equational theories[END_REF] as a consequence of some combination techniques based on an adequate notion of (shared) constructors. C. Ringeissen used similar ideas later in [START_REF] Ringeissen | co-operation of decision procedure for the satisfiability problem[END_REF] to extend the Nelson-Oppen method to theories sharing constructors in a sense closed to that of [START_REF] Domenjoud | Combination techniques for nondisjoint equational theories[END_REF].

Recently, C. Tinelli and C. Ringeissen have provided some sufficient conditions for the Nelson-Oppen combinability by using a concept of stable Σ-freeness [START_REF] Tinelli | Unions of non-disjoint theories and combinations of satisfiability procedures[END_REF], a natural extension of Nelson-Oppen's stable-infiniteness requirement for theories with non-disjoint signatures. As for us, we present a natural way to combine the theory of finite or infinite trees with any first order theory T which can possibly have a non-disjoint signature. A such theory is denoted by T * and does not accept full elimination of quantifiers which makes the decision proce-dure not evident. To show the completeness of T * we give simple conditions on T and only on T so that its combination with the theory of finite or infinite trees, i.e. T * , is complete and accepts a decision procedure which using only six rewriting rules is able to decide the validity or not validity of any first order constraints in T * . This paper is organized in five sections followed by a conclusion. This introduction is the first section. In Section 2, we recall the basic definitions of signature, model, theory and vectorial quantifier. In section 3, after having presented a new quantifier called zero-infinite, we preset a new class of theories that we call zero-infinite-decomposable. The main idea behind this class of theories consists in decomposing each quantified conjunction of atomic formulas into three embedded sequences of quantifications having very particular properties, which can be expressed with the help of three special quantifiers denoted by ∃?, ∃!, ∃

Ψ (u)
o ∞ and called at-most-one, exactly-one, zero-infinite. We end this section by six rewriting rules which for every zero-infinite-decomposable theory T and for every proposition ϕ give either true or false in T . The correctness of our algorithm shows the completeness of the zero-infinite-decomposable theories. In Section 4, we give a general way to generate the axioms of T * using those of T and show that if T is flexible then T * is zero-infinite-decomposable and thus complete. The flexible theories are theories having elegant properties which enable us to eliminate quantifiers in particular cases. We end this section by some fundamental flexible theories.

The zero-infinite-decomposable theories, the decision procedure in zero-infinitedecomposable theories, the axiomatization of T * and the flexible theories are our main contribution in this paper. A full version of this paper with detailed proofs can be found in [START_REF] Djelloul | Extension of first order theories into trees[END_REF] and in the Ph.D thesis of K. Djelloul [START_REF] Djelloul | Complete theories around trees[END_REF] (chapters 3 and 4).

Preliminaries

Let V be an infinite set of variables. Let S be a set of symbols, called a signature and partitioned into two disjoint sub-sets: the set F of function symbols and the set R of relation symbols. To each function symbol and relation is linked a non-negative integer n called its arity. An n-ary symbol is a symbol of arity n. A 0-ary function symbol is called a constant. An S-formula is an expression of the one of the eleven following forms:

s = t, rt 1 . . . t n , true, false, ¬ϕ, (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ), (ϕ ↔ ψ), (∀x ϕ), (∃x ϕ), (1)
with x ∈ V , r an n-ary relation symbol taken from F , ϕ and ψ shorter Sformulas, s, t and the t i 's S-terms, that are expressions of the one of the two following forms x, f t 1 . . . t n , with x taken from V , f an n-ary function symbol taken from F and the t i shorter

S-terms

The S-formulas of the first line of (1) are called atomic, and flat if they are of the one of the five following forms:

true, false, x 0 = f x 1 ...x n , x 0 = x 1 , rx 1 ...x n ,
with the x i 's possibly non-distinct variables taken from V , f ∈ F and r ∈ R.

If ϕ is an S-formula then we denote by var(ϕ) the set of the free variables of ϕ. An S-proposition is an S-formula without free variables. The set of the S-terms and the S-formulas represent a first-order language with equality.

An S-structure is a couple M = (D, F ), where D is a non-empty set of individuals of M and F a set of functions and relations in D. We call instantiation or valuation of an S-formula ϕ by individuals of M , the (S ∪D)-formula obtained from ϕ by replacing each free occurrence of a free variable x in ϕ by the same individual i of D and by considering each element of D as 0-ary function symbol.

An S-theory T is a set of S-propositions. We say that the S-structure M is a model of T if for each element ϕ of T , M |= ϕ. If ϕ is an S-formula, we write T |= ϕ if for each S-model M of T , M |= ϕ. A theory T is called complete if for every proposition ϕ, one and only one of the following properties holds:

T |= ϕ, T |= ¬ϕ.
Let M be a model. 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 .

Zero-infnite-decomposable theories

In this section, let us fix a signature S * = F * ∪ R * . Thus, we can allow ourself to remove the prefix S * from the following words: formulas, equations, theories and models. We will also use the abbreviation wnfv for "without new free variables". We say that an S-formula ϕ is equivalent to a wnfv S-formula ψ in T if T |= ϕ ↔ ψ and ψ does not contain other free variables than those of ϕ.

Zero-infinite quantifier [15]

Let M be a model and T a theory. Let Ψ (u) be a set of formulas having at most one free variable u. Let ϕ and ϕ j be M -formulas. We write

M |= ∃ Ψ (u) o ∞ x ϕ(x), (2)
if for each instantiation ∃x ϕ ′ (x) of ∃x ϕ(x) by individuals of M one of the following properties holds:

the set of the individuals i of M such that M |= ϕ ′ (i), is infinite, -for every finite sub-set {ψ 1 (u), .., ψ n (u)} of elements of Ψ (u), the set of the individuals i of M such that M |= ϕ ′ (i) ∧ j∈{1,...,n} ¬ψ j (i) is infinite.

We write T |= ∃

Ψ (u) o ∞ x ϕ(x), if for every model M of T we have M |= ∃ Ψ (u)
o ∞ x ϕ(x). This infinite quantifier holds only for infinite models, i.e. models whose set of elements are infinite. Note that if Ψ (u) = {false} then (2) simply means that if M |= ∃x ϕ(x) then M contains an infinity of individuals i such that M |= ϕ(i). The intuitions behind this definition come from an aim to eliminate a conjunction of the form i∈I ¬ψ i (x) in complex formulas of the form ∃x ϕ(x) ∧ i∈I ¬ψ i (x) where I is a finite (possibly empty) set and the ψ i (x) are formulas which do not accept full elimination of quantifiers.

Zero-infinite-decomposable theory [15]

A theory T is called zero-infinite-decomposable if there exists a set Ψ (u) of formulas, having at least one free variable u, a set A of formulas closed under conjunction, a set A ′ of formulas of the form ∃xα with α ∈ A, and a sub-set A ′′ of A such that:

1. every formula of the form ∃x α∧ψ, with α ∈ A and ψ a formula, is equivalent in T to a wnfv formula of the form:

∃x ′ α ′ ∧ (∃x ′′ α ′′ ∧ (∃x ′′′ α ′′′ ∧ ψ)), with ∃x ′ α ′ ∈ A ′ , α ′′ ∈ A ′′ , α ′′′ ∈ A and T |= ∀x ′′ α ′′ → ∃!x ′′′ α ′′′ , 2. if ∃x ′ α ′ ∈ A ′ then T |= ∃?
x ′ α ′ and for every free variable y in ∃x ′ α ′ , one at least of the following properties holds:

-T |= ∃?yx ′ α ′ , -there exists ψ(u) ∈ Ψ (u) such that T |= ∀y (∃x ′ α ′ ) → ψ(y), 3. if α ′′ ∈ A ′′ then
the formula ¬α ′′ is equivalent in T to a wnfv formula of the form i∈I α i with α i ∈ A, -for every x ′′ , the formula ∃x ′′ α ′′ is equivalent in T to a wnfv formula which belongs to A ′′ , -for every variable x ′′ , T |= ∃ [START_REF] Clark | Negation as failure. Logic and Data bases[END_REF]. every conjunction of flat formulas is equivalent in T to a wnfv disjunction of elements of A, 5. if the formula ∃x ′ α ′ ∧ α ′′ with ∃x ′ α ′ ∈ A ′ and α ′′ ∈ A ′′ has no free variables then x is the empty vector, α ′ is the formula true and α ′′ is either the formula true or false.

Ψ (u) o ∞ x ′′ α ′′ ,

A decision procedure for zero-infinite-decompoable theories [14]

Let T be a zero-infinite-decomposable theory. The sets Ψ (u), A, A ′ and A ′′ are known and fixed.

¬(∃x ′ α ′ ∧ α ′′ ∧ i∈I ¬(∃ȳ ′ i β ′ i )), (3)
with I a finite possibly empty set, Proof. We give bellow six rewriting rules which transform a normalized formula of any depth d into a conjunction of final formulas equivalent in T . To apply the rule p 1 =⇒ p 2 on a normalized formula p means to replace in p, the subformula p 1 by the formula p 2 , by considering the connector ∧ associative and commutative.

∃x ′ α ′ ∈ A ′ , α ′′ ∈ A ′′ , ∃ȳ ′ i β ′ i ∈ A ′ , α ′′ is different
(1) ¬ ∃x α ∧ ϕ∧

¬(∃ȳ true) =⇒ true (2) ¬ ∃x α ∧ false ∧ ϕ =⇒ true (3) ¬ ∃x α∧ i∈I ¬(∃ȳ i β i ) =⇒¬ ∃x ′ x′′ α ′ ∧ α ′′ ∧ i∈I ¬(∃x ′′′ ȳi α ′′′ ∧ β i ) (4) ¬ ∃x α ∧ ϕ∧ ¬(∃ȳ ′ β ′ ∧ β ′′ ) =⇒ ¬(∃x α ∧ ϕ ∧ ¬(∃ȳ ′ β ′ ))∧ i∈I ¬(∃xȳ ′ α ∧ β ′ ∧ β ′′ i ∧ ϕ) (5) ¬ ∃x α∧ i∈I ¬(∃ȳ ′ i β ′ i ) =⇒¬ ∃x ′ α ′ ∧ α ′′ * i∈I ′ ¬(∃ȳ ′ i β ′ i ) (6) ¬     ∃x α ∧ ϕ∧ ¬ ∃ȳ ′ β ′ ∧ β ′′ ∧ i∈I ¬(∃z ′ i δ ′ i )     =⇒ ¬(∃x α ∧ ϕ ∧ ¬(∃ȳ ′ β ′ ∧ β ′′ ))∧ i∈I ¬(∃xȳ ′ zi α ∧ β ′ ∧ β ′′ ∧ δ ′ i ∧ ϕ)
with α an element of A, ϕ a conjunction of normalized formulas and I a finite possibly empty set. In the rule (3), the formula ∃x α is equivalent in T to a decomposed formula of the form ∃x

′ α ′ ∧ (∃x ′′ α ′′ ∧ (∃x ′′′ α ′′′ )) with ∃x ′ α ′ ∈ A ′ , α ′′ ∈ A ′′ , α ′′′ ∈ A, T |= ∀x ′′ α ′′ → ∃!x ′′′ α ′′′ and ∃x ′′′ α ′′′ different from ∃ε true.
All the β i 's belong to A. In the rule (4), the formula ∃x α is equivalent in T to a decomposed formula of the form ∃x ′ α ′ ∧ (∃x ′′ α ′′ ∧ (∃ε true)) with ∃x ′ α ′ ∈ A ′ and α ′′ ∈ A ′′ . The formula ∃ȳ ′ β ′ belongs to A ′ . The formula β ′′ belongs to A ′′ and is different from the formula true. Moreover, T |= (¬β ′′ ) ↔ i∈I β ′′ i with β ′′ i ∈ A. In the rule ( 5), the formula ∃x α is not of the form ∃x α 1 ∧ α 2 with ∃x α 1 ∈ A ′ and α 2 ∈ A ′′ , and is equivalent in T to a decomposed formula of the form

∃x ′ α ′ ∧ (∃x ′′ α ′′ ∧ (∃ε true)) with ∃x ′ α ′ ∈ A ′ and α ′′ ∈ A ′′ . Each formula ∃ȳ ′ i β ′ i belongs to A ′ . The set I ′ is the set of the i ∈ I such that ∃ȳ ′ i β ′ i does not contain free occurrences of a variable of x′′ . Moreover, T |= (∃x ′′ α ′′ ) ↔ α ′′ * with α ′′ * ∈ A ′′ . In the rule (6), I = ∅, ∃ȳ ′ β ′ ∈ A ′ , ∃z ′ i δ ′ i ∈ A ′ and β ′′ ∈ A ′′ .
Let ψ be a formula without free variables, the decision of ψ proceeds as follows:

1. Transform the formula ψ into a normalized formula ϕ which is equivalent to ψ in T . 2. While it is possible, apply the rewriting rules on ϕ. At the end, we obtain a conjunction φ of final formulas.

According to Property 3.3.5, the application of the rules on a formula ψ without free variables produces a wnfv conjunction φ of final formulas, i.e. a conjunction φ of final formulas without free variables. According to Property 3.3.4, φ is either the formula true, or the formula ¬true, i.e. the formula false. Their nodes are labeled by the symbols 0,1,s,f, of respective arities 0,0,1,2, taken from a set F of functional symbols which we assume to be infinite. While the first tree is a finite tree (it has a finite set of nodes), the two others are infinite trees and have an infinite set of nodes. We denote by A the set of all trees4 constructed on F . We introduce in A a set of construction operations5 , one for each element f ∈ F , which is the mapping (a 1 , ..., a n ) → b, where n is the arity of f and b the tree whose initial node is labeled by f and the sequence of suns is (a 1 , ..., a n ), and which be schematized as:

We thus obtain the structure of finite or infinite trees constructed on F , which we denote by (A, F ).

Theory of finite or infinite trees

Let S be a signature containing only an infinite set of function symbols F . Michael Maher has the S-theory of finite or infinite trees [START_REF] Maher | Complete axiomatization of the structure of finite, rational and infinite trees[END_REF]. The axiomatization of this S-theory is the set of the S-propositions of the one of the following forms:

∀x∀ȳ f x = f ȳ → i x i = y i , 2 ∀x∀ȳ ¬f x = g ȳ, 3 ∀x∃!z i z i = f i (z, x),
with f and g two distinct function symbols taken from F , x a vector of variables x i , ȳ a vector of variables y i , z a vector of distinct variables z i and f i (x, z) an S-term which begins with an element of F followed by variables taken from xz.

The first axiom is called axiom of explosion, the second one is called axiom of conflict of symbols and the last one is called axiom of unique solution.

We show that this theory has as model the structure of finite or infinite trees [START_REF] Dao | Résolution de contraintes du premier ordre dans la théorie des arbres finis or infinis[END_REF]. For example, using axiom 3, we have T |= ∃!xy x = f 1y ∧ y = f 0x. The individuals x and y represents the two following trees in the structure of finite or infinite trees: Let T be an S-theory. The extension of the S-theory T into trees is the S *theory by T * and whose set of axioms is the infinite set of the following S * -propositions, with x a vector of variables x i and ȳ a vector of variables y i :

1. Explosion: for all f ∈ F * :

∀x∀ȳ ¬pf x ∧ ¬pf ȳ ∧ f x = f ȳ → i x i = y i 2.
Conflict of symbols: Let f and g be two distinct function symbols taken from

F * : ∀x∀ȳ f x = g ȳ → pf x ∧ pg ȳ 3. Unique solution ∀x∀ȳ ( i px i ) ∧ ( j ¬py j ) → ∃!z k (¬pz i ∧ z k = t k (x, ȳ, z))
where z is a vector of distinct variables z i , t k (x, ȳ, z) an S * -term which begins by a function symbol f k ∈ F * followed by variables taken from x, ȳ, z, moreover, if f k ∈ F , then the S * -term t k (x, ȳ, z) contains at least a variable from ȳ or z 4. Relations of R: for all r ∈ R,

∀x rx → i px i 5. Operations of F : for all f ∈ F , ∀x pf x ↔ i px i (if f is 0-
∀x ¬x < x, 2 ∀x∀y∀z (x < y ∧ y < z) → x < z, 3 ∀x∀y x < y ∨ x = y ∨ y < x, 4 ∀x∀y x < y → (∃z x < z ∧ z < y), 5
∀x∀ȳ ¬pf x ∧ ¬pf ȳ ∧ f x = f ȳ → i x i = y i 2 ∀x∀ȳ f x = g ȳ → pf x ∧ pg ȳ 3 ∀x∀ȳ ( i px i ) ∧ ( j ¬py j ) → ∃!z k (¬pz i ∧ z k = f k (x, ȳ, z)) 4 ∀x∀y x < y → (px ∧ py), 5 ∀x ¬pf x, 6 ∃x px, 7 ∀x px → ¬x < x, 8 ∀x∀y∀z px ∧ py ∧ pz → ((x < y ∧ y < z) → x < z), 9 ∀x∀y (px ∧ py) → (x < y ∨ x = y ∨ y < x), 10 ∀x∀y (px ∧ py) → (x < y → (∃z pz ∧ x < z ∧ z < y)), 11 ∀x px → (∃y py ∧ x < y), 12 ∀x px → (∃y py ∧ y < x),
where f and g are distinct function symbols taken from F * , x, y, z variables, x a vector of variables x i , ȳ a vector of variables y i , z a vector of distinct variables z i and f k (x, ȳ, z) a term which begins by an element f k of F * followed by variables taken from xȳz.

Completeness of T *

We have given a general axiomatization of T * using the axioms of T , what about the completeness of T * ? Are all the extensions into trees complete theories? While in [START_REF] Djelloul | About the combination of trees and rational numbers in a complete first-order theory[END_REF] we have shown the completeness of a combination of trees and rational numbers, in this paper the challenge is to use general properties that hold not only for rational numbers but for a large set of different theories T i and that make T * i and thus complete. Let S = F ∪ R be a signature and T an S-theory. Let S * = F * ∪ R * be another signature with F * an infinite set of function symbols containing F and R * = R ∪ {p}. Let T * be the S * -theory of the extension of T into trees. Suppose that the variables of V are ordered by a linear dense order relation without endpoints denoted ≻.

  from the formula false, all the β ′ i 's are different from the formulas true and false. Property 3.3.4 Let ϕ be a conjunction of final formulas without free variables. The conjunction ϕ is either the formula true or the formula ¬true. Property 3.3.5 Every normalized formula is equivalent in T to a conjunction of final formulas.

Corollary 3 . 3 . 6

 336 If T is zero-infinite-decomposable then T is complete and accepts a decision procedure in the form of six rewriting rules which for every give either true or false in T .4 Extension of first-order theories into trees4.1 The structure of finite or infinite treesTrees are well known objects in the computer science world. Here are some of them:

4. 3

 3 Axiomatization of the theory T + T ree or T * Let us fix now a signature S containing a set F of function symbols and a set R of relation symbols, as well as a signature S * containing: -an infinite set F * = F ∪ F A where F A is an infinite set of function symbols disjoint from F . -a set R * = R ∪ {p} of relation symbols, containing R, and an 1-ary relation symbol p.

  ∀x ∃y x < y, 6 ∀x ∃y y < x. Let now F * be an infinite set of function symbols and R * = {<, p} a set of relation symbols containing the 2-ary relation symbol < and the 1-ary relation symbol p. Let S * be the signature F * ∪ R * . According to the transformations of axioms given in Section 4.3, the axiomatization of the extension of the theory T ord into trees is the S * -theory T ord * whose axioms are the following propositions: 1

5. 1

 1 Flexible theory Definition 5.1.1 We call leader of an S-equation α the greatest variable x in α, according to the order ≻, such that T |= ∃!xα. Definition 5.1.2 A conjunction of S-atomic formulas α is called formated in T if α does not contain sub-formulas of the form f 1 = f 2 or rf 1 ...f n or y = x, where all the f i 's are 0-ary function symbols taken from F , r ∈ R and x ≻ y, -each S-equation of α has a distinct leader which has no occurrences in other S-equations or S-relations of α, -if α ′ is the conjunction of all the S-equations of α then for all x ∈ var(α ′ ) we have T |= ∃?x α ′ . Definition 5.1.3 The theory T is called flexible if for each conjunction α of S-equations and for each conjunction β of S-relations:1. α ∧ β is equivalent in T to a formated conjunction of atomic formulas wnfv, 2. the S-formula ¬β is equivalent in T to a disjunction wnfv of S-equations and S-relations, 3. for all x ∈ V the S-formula ∃x β is equivalent in T to false, or to a wnfv conjunction of S-relations, -for all x ∈ V , we haveT |= ∃ {f aux} o ∞ x β.Let us now present our main result Theorem 5.1.4 If T is flexible then T * is zero-infinite-decomposable.

  Definition 3.3.1 A normalized formula ϕ of depth d ≥ 1 is a formula of the form ¬(∃x α ∧ i∈I ϕ i ), where I is a finite possibly empty set, α ∈ A, the ϕ i are normalized formulas of depth d i with d = 1 + max{0, d 1 , ..., d n }, and all the quantified variables have distinct names and different form those of the free variables. Every formula is equivalent in T to a normalized formula.

	Property 3.3.2 Definition 3.3.3 A final formula is a normalized formula of the form

  ary then this axiom is written pf ) 6. Elements not in T : for all f ∈ F * -F , Extension into trees of the axioms of T : all axioms obtained by the following transformations of each axiom ϕ of T : While it is possible replace all subformula of ϕ which is of the form ∃x ψ, but not of the form ∃x ( px i ) ∧ ψ ′ , by ∃x ( px i ) ∧ ψ and every sub-formula of ϕ which is the form ∀x ψ, but not of the form ∀x( px i ) → ψ ′ , by ∀x ( px i ) → ψ.Let F be an empty set of function symbols and let R be a set of relation symbols containing only the relation symbol < of arity 2. If t 1 and t 2 are terms, then we write t 1 < t 2 for < (t 1 , t 2 ). Let T ord be the theory of linear dense order relation without endpoints, whose signature is S = F ∪ R and whose axioms are the propositions:

	∀x ¬pf	x
	7. Existence of an element satisfying p (only if F does not contain 0-ary function
	symbols):
	∃x px,
	8. 4.4 Example: Extension of linear dense order relations without
	endpoints into trees

The word problem in an equational theory T is the problem of determining whether a given equation s = t is valid in T , or equivalently, whether a disequation ¬(s = t) is (un)satisfiable in T . In a term rewriting system, a constructor is a function symbol that does not appear as the top symbol of a rewrite rule's left-hand-side.

More precisely, we define first a node to be a word constructed on the set of strictly positive integers. A tree a on F , is then a mapping of type a : E → F , where E is a non-empty set of nodes, each one i1 . . . i k (with k ≥ 0) satisfies two conditions: (1) if k > 0 then i1 . . . i k-1 ∈ E and (2) if the arity of a(i1 . . . i k ) is n, then the set of the nodes E of the form i1 . . . i k i k+1 is obtained by giving to i k+1 the values 1, ..., n.

In fact, the construction operation linked to the n-ary symbol f of F is the mapping (a1, ..., an) → b, where the ai's are any trees and b is the tree defined as follows from the ai's and their set of nodes Ei's: the set E of nodes of a is {ε} ∪ {ix|x ∈ Ei and i ∈ {1, ..., n} and, for each x ∈ E, if x = ε, then a(x) = f and if x is of the form iy, with i being an integer, a(x) = ai(y).

This article was processed using the L A T E X macro package with LLNCS style

Acknowledgments We thank Alain Colmerauer for our many discussions and his help in this work. We thank him too for the quality of her remarks and advice on how to improve the organization of this paper. We dedicate to him this paper with our best wishes for a speedy recovery.

We present in this section the axiomatization of some fundamental flexible theories. Full proofs can be found in [START_REF] Djelloul | Complete theories around trees[END_REF].

Infinite Clark equational theory: Let Cl be a theory together with an empty set of function and relation symbols and whose axioms is the infinite set of propositions of the following form:

where all the variables x 1 ...x n are distinct and (n = 0). The form ( 4) is called diagram of axiom and for each value of n there exists an axiom of Cl. This theory Cl has been introduced by Clark [START_REF] Clark | Negation as failure. Logic and Data bases[END_REF] and has an infinite set of models each one containing an infinite set of distinct individuals.

Additive rational or real numbers theory with addition and subtraction: Let F = {+, -, 0, 1} be a set of function symbols of respective arities 2, 1, 0, 0. Let R = ∅ be an empty set of relation symbols. The theory Ra of additive rational or real numbers together with addition and subtraction consists in the infinite set of propositions of the following form:

with n an non-null integer. This theory has two usual models: rational numbers Q with addition and subtraction in Q and real numbers R with addition and subtraction in R.

Linear dense order theory without endpoints: Let F be an empty set of function symbols and R a set of relation symbols containing only the binary relation symbol <. The theory T ord be the theory of the linear dense order without endpoints consists in the set of propositions of the following form:

Ordered additive rational or real numbers theory with addition and subtraction: Let F = {+, -, 0, 1} be a set of function symbols of respective arities 2, 1, 0, 0. Let R = {<} be a set of relation symbols containing only the binary relation symbol <. The theory T ad of ordered additive rational or real numbers theory with addition and subtraction consists in the infinite set of propositions of the following form:

11 ∀x ∃y x < y, 12 ∀x ∃y y < x, 13 ∀x ∀y ∀z x < y → (x + z < y + z), 14 0 < 1.

with n a non-null integer.

Conclusion

We have defined in this paper a general idea for the extension of the models of Prolog by giving an automatic way to combine any first order theory T with the theory of finite or infinite trees. To show the completeness of T * we have introduced the flexible theories and have shown that if T is flexible then T * zero-infinite-decomposable. The zero-infinite-decomposable theories are first order theories having elegant properties which enable us to decide the validity of any proposition using only six rewriting rules. The main idea behind this rules consists in a local decomposition of quantified conjunctions of hybrid atomic formulas, a partial elimination of quantifiers using the properties of the vectorial quantifiers, and a special distribution to decrease the depth of the formulas.

There exists many practical applications of the extensions into trees of first order theories. First-order constraints on trees can be expressed in a simpler way when they are in the extension into trees of another structure. For example, the constraints representing the moves in two players games introduced by Alain Colmerauer and Thi-Bich-Hanh Dao [START_REF] Colmerauer | Expressiveness of full first-order constraints in the structure of finite or infinite trees[END_REF][START_REF] Dao | Résolution de contraintes du premier ordre dans la théorie des arbres finis or infinis[END_REF] can be represented by a simpler constraint in the extension into trees of the integers together with the operations of addition and subtraction and a linear dense order relation.

On the other hand, our decision algorithm can decide the validity or not validity of big and complex propositions and can also be applied on formulas having free variables and produces in this case a boolean combination of basic formulas which does not accept full elimination of quantifiers. Unfortunately, this algorithm is not able to detect formulas having free variables and being always equivalent to false or true in T * . It does not warrant that a final formula having at least one free variable is neither true nor false in T * and can not present the solutions of the free variables in a clear and explicit way. This is why our algorithm is called decision procedure and not a general algorithm for solving first order constraints. It would be interesting to transform our decision procedure into a general algorithm for solving any first order constraint in T and which presents the solutions of the free variables in a clear and explicit way, as it has been done in [START_REF] Colmerauer | Expressiveness of full first-order constraints in the structure of finite or infinite trees[END_REF][START_REF] Dao | Résolution de contraintes du premier ordre dans la théorie des arbres finis or infinis[END_REF] for the theory of finite trees and finite or infinite trees. This kind of algorithm needs another work completely different from this one, by introducing syntactic and semantic definitions much more complex than the definition of flexible theories given in this paper. The implementation of a such algorithm will enable us to extend the Prolog language by allowing the user to solve any complex first order constraint, with or without free variables, in many combinations of theories around trees.

Currently, we are trying to proof that every extension of a complete theory into trees is complete and may be zero-infinite-decomposable. For that, we expect to add new vectorial quantifiers in the decomposition such as ∃ n which means there exists n and ∃ Ψ (u) n,∞ which means there exists n or infinite, in order to increase the size of the set of the zero-infinite-decomposable theories and may be get a much more simple definition than the one defined in this paper. We plan also with Thom Fruehwirth [START_REF] Fruehwirth | Essentials of constraints programming[END_REF] to add to CHR a general mechanism to treat our normalized formulas. This will enable us to implement quickly and easily our algorithms and get a general idea on the expressiveness of first order constraints in combinations of trees and first order theories.


Anderson S Nunes
email: anderson@esss.com.br

Olivier Chadebec

Gérard Meunier

Patrick Kuo-Peng

Magnetic devices analysis by Face FEM coupled with standard reluctance network

Keywords: Reluctance network, Finite Element Method (FEM), face shape functions, Face FEM

A Finite Element Method (FEM) mesh is converted to a reluctance network through an original magnetostatic formulation based on face shape functions. This meshed reluctance network is coupled with an standard one, characterizing a 0D system. Both approaches are fully-compatible and the hybridized problem can be solve with a single circuit solver. The approach is tested in 2D on a magnetic circuit with an air gap and compared to classical FEM nodal formulation.

I. INTRODUCTION

Optimizing electromagnetic devices can require a large amount of data that might be provided by numerical simulations. Many numerical methods are used to model electromagnetic devices, but the RNM (Reluctance Network Method) and FEM (Finite Element Method) are the most widely used for magnetostatic modeling.

The FEM is well known by its flexibility and generality, once the mathematical formulations are based on a mesh. Furthermore, it is noticeable the knowledge base available for this method, for instance [START_REF] Bastos | Magnetic Materials and 3D Finite Element Modeling[END_REF]. However, it leads to an high number of degrees of freedom and so quite long computation times.

On the other hand, the RNM is one of the most primitive methods for magnetic modeling and its application is based on a reluctance network. This method has remained useful due to its coherent results obtained with low computational effort and low computational simulation time [START_REF] Sykulski | Computational Magnetics, ser. International journal of numerical modelling[END_REF] and has been largely applied to model power transformers [3] [4]. This method is also largely applied to model rotating electrical machines [START_REF] Petrichenko | Contribution à la modélisation et à la conception optimale des turbo-alternateurs de faible puissance[END_REF][6] [START_REF] Tang | Analytical modeling of flux-switching machines using variable global reluctance networks[END_REF] and transmission lines [START_REF] Bormann | Reluctance network treatment of skin and proximity effects in multi-conductor transmission lines[END_REF]. Nevertheless, it is important to notice that these applications are based on a reluctance network defined manually, that might imply an hard, long and non-general task.

In [START_REF] Dular | Dual finite element formulations for lumped reluctances coupling[END_REF] is presented a methodology that couples nodal/edge FEM with external reluctances network. In this paper, we go a step forward by proposing a formulation fully-compatible with both numerical approaches and solved with a single 0D circuit solver.

Finally, the results of modeling a actuator with the classical nodal FEM and with the proposed methodology are compared.

II. MAGNETOSTATIC FACE FEM FORMULATION

The magnetostatic fields might be described by the Ampère's (1) and Gauss (2) laws and the constitutive relation for magnetic materials [START_REF] Lopez-Fernandez | Stray losses control in shell type transformers. part ii: Method of threedimensional network solution[END_REF].

curl H = J (1) div B=0 (2) B = µH (3)
where the magnetic field H, in A/m, is composed by the fields H 0 , due to an imposed current density source J 0 , and H m that can be obtained from the gradient of the magnetic scalar potential V r , as presented in [START_REF] Petrichenko | Contribution à la modélisation et à la conception optimale des turbo-alternateurs de faible puissance[END_REF].

H = H 0 + H m (4) H m = -∇V r (5)
Thus, applying (5) in ( 4) and integrating the resulting equation along a domain Ω, it is possible to obtain [START_REF] Fukuoka | A method for optimizing the design of spm type magnetic gear based on reluctance network analysis[END_REF], for which W is the face interpolation function.

Ω W i • H dΩ + Ω W i • ∇V r dΩ = Ω W i • H 0 dΩ (6)
Since the magnetic induction B, in T , is given by [START_REF] Tang | Analytical modeling of flux-switching machines using variable global reluctance networks[END_REF], the left side of ( 6) is rewritten as [START_REF] Bormann | Reluctance network treatment of skin and proximity effects in multi-conductor transmission lines[END_REF].

B = n f j=1 W i Φ i (7)
Ω W i • HdΩ = n f j=1 Ω υW i • W j dΩ Φ j (8)
where j and i are the faces index, nf is the number of faces, υ is the magnetic reluctivity, and Φ is the magnetic flux.

Applying the divergence theorem in the second term of (6) and evaluating it along two adjacent elements Ω a and Ω b , leads to [START_REF] Dular | Dual finite element formulations for lumped reluctances coupling[END_REF]. Taking into account that the normal component of the function W is constant along the face shared by Ω a and Ω b , its second term becomes null and it can be rewritten as (10).

Ωa+Ω b W i • ∇V r dΩ = Γa-Γ b V r W i • ndΓ- Ωa+Ω b V r ∇ • W i dΩ (9) Ω W i • ∇V r dΩ = - Ωa+Ω b V r ∇ • W i dΩ (10)
This equation can be split in terms of Ω a and Ω b , where the flux direction is defined from Ω a to Ω b . Then, considering that ∇ • w i is the inverse of the element volume, it is possible to obtain (11).

Ω W i • ∇V r dΩ = V r a -V r b (11)
The third term of ( 6) is the magnetic field due to an imposed current density J 0 , which can be obtained using Biot-Savart law, for instance.

Finally, lets rewrite ( 6) as the following matrix system

[ ] [Φ] -[∆V M ean ] = [H 0 ] (12)
where [ ] is a reluctance matrix,[Φ] is the unknown flux matrix, [∆V M ean ] is the magnetic potential jump between two reluctances and [V 0 ] contains the f mm sources. Besides the matrix system is stated, ( 2) is not solved yet. Nevertheless, the B free divergence is constrained solving (12) as a circuit system , where the Kirchhoff's current law is imposed. It suggests that the solution can be obtained by the use of a 0D circuit solver.

III. MODEL AND RESULTS

In order to compare the results obtained with the proposed methodology, a simple magnetic circuit with an air gap is analyzed using the well established nodal first order FEM, based on magnetic vector potential A. The magnetic induction distribution is presented in Fig. 1.

Fig. 1: Magnetic induction distribution obtained with classical FEM

Then, this model is reduced to a 0D model, i.e most of the magnetic circuit is modeled by an classical reluctance network and just the air gap region is meshed (i.e. the region where the equivalent reluctance network is not so easy to define), as presented in Fig. 2. Then the problem is solved by a circuit solver and magnetic induction is interpolated using [START_REF] Tang | Analytical modeling of flux-switching machines using variable global reluctance networks[END_REF], resulting in Fig. 3.

The maximum magnetic induction in the air gap obtained with the proposed methodology is 0.625 T and with the classical FEM is 0.606 T, that represents a difference of 3.13%.

IV. CONCLUSION

This paper has presented a methodology capable to convert a FEM mesh into a reluctance network, allowing its easy coupling with a classical network obtained analytically. The original model was reduced to a 0D system keeping coherent results.

Fig. 2 :

 2 Fig. 2: Networks coupling


B Monjardet
email: monjarde@univ-paris1.fr

SOME ORDER DUALITIES IN LOGIC, GAMES AND CHOICES

Keywords: antiexchange closure operator, closure system, Galois connection, implicational system, Galois lattice, path-independent choice function, preference aggregation rule, simple game. JEL classification: C00, D71

We first present the concept of duality appearing in order theory, i.e. the notions of dual isomorphism and of Galois connection. Then we describe two fundamental dualities, the duality extension/intention associated with a binary relation between two sets, and the duality between implicational systems and closure systems. Finally we present two "concrete" dualities occuring in social choice and in choice functions theories.

Introduction

In the index of the Encyclopaedia of Mathematics (Kluwer, 1987) the terms duality or dual appear about 120 times. Here we will only consider the duality occurring in order theory. Why order duality matters ? for a very simple reason. When one can show that two sets of objects are two dual posets, then one can automatically transfer any result on one of these posets to the other. We will begin by recalling the notion of dual posets and the notion of Galois connection, a useful tool to obtain dual posets. Then we will present two significant dualities obtained through a Galois connection: the "extension/intention" duality associated to a binary relation and the duality between implicational systems and closure systems. The first one is applied to an example in social choice theory. The second one generalizes the well known duality between posets and T 0 -topologies (or distributive lattices). We will finally present a duality between path-independent choice functions and anti-exchange closure operators. Some other uses of order duality are mentionned in the conclusion.

N.B. Unless explicitly stated, all the sets considered in this paper are finite.

Order Duality and Galois Connection

A partially ordered set (or poset) P = (X, P ) is a set X equipped with a reflexive, transitive and antisymmetric binary relation P . Often, we shall only denote such a poset by (P, ) or simply by P. Moreover, we write x ¡ P or F ¢ P rather than x ¡ X or F ¢ X . The dual of the poset P = (X, ) is the poset P d = (X, £ ), where x £ y if and only if y x.

A map f from a poset P = (X, P ) to a poset Q = (Y, Q ) is isotone (respectively antitone) if

x P y implies f(x) Q f(y) (respectively x P y implies f(x) £ Q f(y)).

Two posets P and Q are isomorphic if there exists an isomorphism beetwen them, i.e. a bijective map f from P to Q which is isotone as well as its inverse f -1 (equivalently, a bijective map f from

P to Q atisfying x P y if and only if f(x) Q f(y)).

Definition 1

Two posets P and Q are dual if there exists a dual isomorphism beetwen them, i.e. a bijective map f from P to Q satisfying x P y if and only if f(x) £ Q f(y).

Observe that the posets P = (X, ) and P d = (X, £ ) are dual since the identity map is a dual isomorphism between them, and that P and Q are dual if and only if there exists an isomorphism between P and Q d .

Many interesting dual posets can be obtained through a Galois connection between two posets, a notion that we define below, after recalling the notions of closure operator and closure system. Definition 2 A closure operator ¤ on a poset P is a map from P to itself which is isotone, extensive and idempotent (x ¥ ¤ (x) = ¤ 2 (x)). The fixed points of ¤ are called the closed elements of P. A closure sytem C on a poset P is a subset C of P such that for each x in P, the set {y ¦ C : x ¥ y} has a least element denoted by ¤ C (x).

It is well known that the set of all closure operators and the set of all closure systems defined on a poset are in a one-to-one correspondence (by the two inverse bijective maps associating to a closure operator the set of its fixed points and to a closure system the application x § ¤ C (x)).

Definition 3

A Galois connection between two posets P and Q is an ordered pair (f,g) of maps

f : P § Q g : Q § P satisfying the following condition: for all x ¦ P and y ¦ Q, x ¥ g(y) if and only if y ¥ f(x).
An equivalent definition uses the composite maps fog denoted by fg(fg(x) = f(g(x))) and gof denoted by gf: (f,g) is a Galois connection if and only if the maps f and g are antitone, and the maps fg and gf are extensive. Now one can state the easily proved but significant result:

Theorem 4

Let (f,g) be a Galois connection between two posets P and Q. Then 1) gf is a closure operator on P and fg is a closure operator on Q ;

2) the two closure systems gf(P) on P and fg(Q) on Q are two dual posets.

One can add that g(Q) = gf(P), f(P) = fg(Q) and that the two inverse dual isomorphims between gf(P) and fg(Q) are given by the restrictions of f and g to the two posets g(Q) and f(P).

A special case of this result occurs when P and Q are two lattices. Recall that a meet-semilattice (respectively a join-semilattice) is a poset where any two elements x and y have a meet x¨y, i.e. a greatest lower bound (respectively a join, i.e. a lowest upper bound x© y) and that a lattice (L, ) is both a meet-semilattice and a join-semilattice. Then one has:

Theorem 5

Let (f,g) be a Galois connection between two lattices L and L'. Then 1) gf is a closure operator on L and fg is a closure operator on L', 2) the two closure systems gf(L) and fg(L') are two dual lattices.

One can add that the lattice gf(L) (respectively fg(L')) is a meet-subsemilattice of L (respectively of L') and that its least element is f( 1

L ) (respectively g(1 L' )).
This result can be in particular applied when L = (2 E , ) (respectively L' = (2 F , )) is the Boolean lattice of all the subsets of a set E (respectively of a set F) ordered by set inclusion. We begin by recalling what becomes the definition of a closure system in the case of the lattice L =

(2 E , ). Note that we say that such a closure system is defined on E although it is in fact a subset of 2 E .

Definition 6

A closure system on E ( is a family C of subsets of E satisfying the two following conditions:

1) E C, 2) C 1 ,C 2 C C 1 C 2 C.
Then, (C, ) is a lattice whose the meet operation is the set intersection, whereas the join operation is given by

C 1 C 2 = {C C : C 1 C 2 C . Remarks 1)
The ("abstract") notion of Galois connection (or connexion) is due to Öre (Öre,1944).

The term Galois connection refers to the existence of such a connection (between subfields and subgroups) in the Galois theory of equations. Before Öre, Birkhoff (1940) has considered the ("concrete") Galois connection associated to a binary relation and defined in the next section (in fact Öre showed that any Galois connection can be obtained as such a Galois connection). 2) Proofs of Theorems 4 and 5 can be found in, for example, [START_REF] Barbut | Ordre et Classification, Algèbre et Combinatoire[END_REF] and [START_REF] Szasz | Introduction to Lattice Theory[END_REF].

The Galois Connection associated with a Binary Relation and the

Extension/Intention Duality

When R is a binary relation between the two sets E and F, we say that the triple (E, F, R) is a bigraph. The following theorem, due to Birkhoff, is an example of an easily proven but fundamental result.

Theorem 7

Let (E, F, R) be a bigraph. One defines a Galois connection (f,g) between the lattices (2 E , ) and

(2 F , ) by setting for X E and Y F f(X) = {y F : xRy for every x X} ; g(Y) ={x E : xRy for every y Y}.

Let (X,Y) be such that X E (respectively Y F) is a closed set in the associated closure system gf(2 E ) on E (respectively fg(2 F ) on F) and such that X = g(Y) (and Y = f(X)). Then, it
follows from Theorem 7 that 1) for all x X, y Y, xRy,

2) for all x ! X, there exists y Y such that xR c y (i.e. (x,y) ! R),

3) for all y ! Y, there exists x X such that xR c y.

These facts induce the below definition:

Definition 8

Let (E, F, R) be a bigraph. The ordered pair (X,Y), where X = g(Y) and Y = f(X) are two corresponding closed sets in the Galois connection associated with the bigraph is called a concept of (E, F, R). X is called the extension (or the extent) of the concept (X,Y) and Y is called its intention (or its intent).

Indeed, when E is a set of objects, F a set of attributes and R the relation "the object x has the attribute y", a concept is a set of objects and a set of attributes such that these objects are the only ones satisfying all these attributes and these attributes are the only ones satisfied by all these objects. So, it is not inadequate to use the traditional terms used in logic of extension and intention.

Ordered by set-inclusion the two sets of extensions and intentions are two posets. It results from the properties of a Galois connection between two lattices (Theorem 5) that one has the following result:

Corollary 9

Let (E, F, R) be a bigraph. The two posets of extensions and intentions associated with the Galois connection induced by this bigraph are two dual lattices.

Then, if one defines an "order of generality" between two concepts (X,Y) and (X',Y') by:

(X,Y) " (X',Y') if X # X'and Y $ Y'
(i.e. if the extension of the first concept is smaller and its intention bigger), one gets that the sets of concepts (ordered by this order) is a lattice isomorphic to the lattice of extensions and dually isomorphic to the lattice of intentions. This lattice called the Galois (or the concept) lattice of the bigraph (E, F, R) has many applications for instance in data analysis, formal concept analysis and knowledge representation theory (see for instance [START_REF] Barbut | Ordre et Classification, Algèbre et Combinatoire[END_REF][START_REF] Ganter | Formal concept analysis, Mathematical foundations[END_REF][START_REF] Valtchev | Construction automatique de taxonomies pour l'aide à la représentation de connaissances par objets[END_REF][START_REF] Valtchev | A partition-based approach towards constructing Galois (concept) lattices[END_REF].

In section 5, we will present two examples of a Galois connection associated with a bigraph, occuring in social choice theory and game theory.

Remark

According to Barbut's result [START_REF] Barbut | Note sur l'algèbre des techniques d'analyse hiérarchique[END_REF] any lattice L can be represented as the Galois lattice of a bigraph (see [START_REF] Barbut | Ordre et Classification, Algèbre et Combinatoire[END_REF].

4.The Duality between Implicational Systems and Closure Systems

We consider now a fundamental duality arising from a Galois connection between binary relations between subsets of a set and families of subsets of this set. In fact, it is a generalization of the well-known duality between posets and T 0 -topologies (or distributive lattices), arising from a Galois connection between binary relations on a set and families of subsets of this set.

We first begin by giving a name to a binary relation between subsets of a set. Definition 10

An implicational system % on a set S is a binary relation on 2

S : % '& 2 S( 2 S .
(X,Y) ) % will be denoted by X 0 Y (% ), and one says that (X,Y) is an implication and that X implies Y (w.r.t. % ).

One defines a % -closed set by:

C & S is a % -closed set if for every X & S, [X & C and X 0 Y (% 1 2 3 [Y & C].
We set f(% ) = C4 = {% -closed sets C}.

Let now C be a set system on S (i.e. a family of subsets of S). One defines an implicational system on S, denoted by 5 C , by :

X 0 Y ( 6 C ) if Y & C for every C ) C such that X 7 C. We set g(C) = 5 C .
Then we have the following result due to [START_REF] Doignon | How to build a knowledge space by querying an expert[END_REF] and Muller (1989) (see also [START_REF] Doignon | Combinatorial representations and convex dimension of convex geometries[END_REF].

Theorem 11

Let (2 2 S8 2 S , 7 ) and (2 2 S , 7 ), be the Boolean lattices of all implicational systems and of all set systems on S. The ordered pair (f,g), with f(% ) = C4 and g(C) = 5 C , is a Galois connection between these two lattices.

The implicational systems closed for the associated closure operator gf on 2 S( 2 S are the socalled full implicational systems, defined below:

Definition 12

A full implicational system is an implicational system 6 satisfying the three following properties : for all X, Y,

Z & S, 1) X 9 Y 3 X 0 Y (5 ) 2) X 0 Y (5 )@ Y 0 Z (5 ) 3 X 0 Z (5 )
3) X 0 Y (5 )@ Z 0 T (5 ) 3 XA Z 0 YA T (5 ). On the other hand, it is easy to check that the set systems closed for the associated closure operator fg on 2 S are the closure sytems on S. So, it results from the properties of a Galois connection that:

Corollary 13

The poset of all full implicational systems on S and the poset of all closure systems on S are two dual lattices.

Remarks 1) In early works of Tarski (for instance [START_REF] Tarski | Fundamentale Begriffe der Methodologie der Deductiven Wissenchaften[END_REF], see also Martin and Pollard's book, 1996) the consequence relation of a logical deductive system is defined as a closure operator on an infinite set S satisfying a "finitary" axiom. Other logicians (like Hertz,1929[START_REF] Scott | Completeness and axiomatizability in many-valued logics[END_REF] defined it as a binary relation between sets and, later, a one-to-one correspondence between Scott's "informations systems" and "algebraic B -structures" has been displayed (see [START_REF] Davey | Introduction to lattices and order[END_REF]). In the finite case, this correspondence becomes exactly the one-to-one correspondence between full implicational systems and closure systems. This last one has been first shown by [START_REF] Armstrong | Dependency structures of data base relationships[END_REF], who, in the context of relational data bases, called a full implicational system a full family of functional dependencies.

2) Particular cases of the above duality are the well-known dualities between preorders and topologies, and between partial orders and T 0 -topologies (or distributive lattices). See for instance, [START_REF] Barbut | Note sur l'algèbre des techniques d'analyse hiérarchique[END_REF]Monjardet, 1970, or Davey and[START_REF] Davey | Introduction to lattices and order[END_REF] This duality between preorders and topologies plays important roles in many situations, for instance in the study of the structure of the (distributive) lattices of stable marriages (see Gusfield and Irving's book, 1989).

3) There exists significant results on the bases of full implicational systems (or of closure operators), i.e. on the minimal sets of implications allowing to recover all the implications of the system (or, equivalently, all the closed sets). In particular, the existence of a canonical basis has been shown by [START_REF] Maier | The Theory of Relational Data Bases[END_REF][START_REF] Guigues | Familles minimales d'implications informatives résultant d'un tableau de données binaires[END_REF][START_REF] Guigues | Familles minimales d'implications informatives résultant d'un tableau de données binaires[END_REF] (see also [START_REF] Caspard | The lattice of closure systems, closure operators and implicational systems on a finite set: a survey[END_REF], where this result is presented in the context of the study of the lattice of all closure systems).

5.The Duality between Profiles of Preferences and Simple Games

We consider here the aggregation preference problem. There is a set A of alternatives, a set N of n voters and one assumes that the preference of a voter on the alternatives is given by a linear order (l.e. a complete partial order) L belonging to the set of all linear orders on A. P = N denotes the set of all possible profiles C = (L 1 ,...,L n ) of preferences of voters. In order to define a class of aggregation rules, we recall the notion of (monotonic) simple game.

Definition 14

A simple game on N is a (non-empty) set of subsets of N satisfying:

[T D and T E U] F [U D ].
We denote by G the set of all simple games on N.

Now one can associate with any simple game a preference aggregation function, i.e. a map from the set P of profiles of linear orders to the set of "collective" preference relations:

Definition 15

The preference aggregation function f associated with the simple game is given by: Thus, x is collectively preferred to y according to the preference aggregation function f if and only if the set of voters preferring x to y in the profile C belongs to the simple game . Then R (C ) is a complete and antisymmetric relation (a so-called tournament), but since it is not non necessarily transitive, it is not necessarily a linear order. Now we consider the binary relation between profiles and simple games which describes the "good" case where the collective preference relation is transitive, i.e. is a linear order.

Definition 16

Let P be the set of all profiles of linear orders and G the set of all simple games. One defines a binary relation R between P and G by : C R G R (C ) D . Thus, one can apply the results of section 3 on the Galois connection associated to a binary relation defined between two sets. So, there is a Galois connection (f,g) between the lattices (2 P , H ) and (2 G , H ) and two dual lattices of closed sets on P and G. The least elements of these two lattices, i.e. the closed sets f(2 P ) and g(2 G ) are characterized in the below result [START_REF] Monjardet | An axiomatic theory of tournament aggregation[END_REF].

Theorem 17

Let (f,g) be the Galois connection associated to the binary relation R defined between the Boolean lattices (2 P , H ) of all sets of preference profiles and (2 G , H ) of all sets of simple games. The least element of the lattice gf(2 P ) of closed sets on P is the set of profiles without cyclical subprofile (like, for instance xyz, yzx and zxy), and the least element of the lattice fg(2 G ) of closed sets on G is the set of ultrafilters on N, i.e. the set of simple games i = {T I N : i P T}, i P N.

This characterization result shows the duality between Guilbaud's Arrovian theorem (1952, see also [START_REF] Monjardet | Social choice theory and the "Centre de Mathématique Sociale[END_REF]) and Sen's possibility theorem (1966) for profiles of linear orders: the only preference aggregation rules defined by simple games providing a transitive collective preference for all profiles of linear orders are the dictatorial rules, and the only profiles for which all such rules provide always a linear order are the "value-restricted"profiles. (One will find other results on this duality in [START_REF] Monjardet | An axiomatic theory of tournament aggregation[END_REF].

Remark

Preference aggregation functions associated with simple games are a particular case of preference aggregation functions associated with effectivity functions, i.e. maps (satisfying some mild conditions) from the set of all subsets of the set N to the set of all set systems on the set S.

(in the case of simple games the image of a subset of N is either the empty set or the set of all non-empty subsets of S). But such a map is the same than a binary relation between 2 N and 2 S and so one can consider the Galois connection and the Galois lattice associated to this relation.

It is exactly what is made by Vannucci in several papers (1999,2002,2003) where he studies this Galois lattice and uses it to get new "structural" representations and desirabilty relations for effectivity functions.

6.The duality between convex geometries and path-independent choice operators

We consider now a significant duality between a class of closure operators and a class of choice operators which is not induced by a a Galois connection.

Definition 18

A closure operator Q on S is an antiexchange closure operator if it satisfies the following two properties:

-

Q (Ø) = Ø, -x,y R Q (X), x S y and y T Q (X + x) imply x R Q (X + y).
It is easy to check that the set of all antiexchange closure operators on S, ordered by the pointwise order between maps, is a meet-semilattice (without greatest element). An antiexchange closure operator Q P is associated with any poset P = (X, U ). It associates to any subset A of P, the set of all elements below or equal to an element of A ; formally Q P( A) = {y T S : there exists x T A with y U x}. We call such an antiexchange closure operator an order closure operator, and in particular, we call it a linear order closure operator when P is linearly ordered. The closed sets of an order closure operator Q P are the order ideals (called also down sets) of P, i.e. the subsets X of P such that y T X and x < y imply x T S.

Definition 19

A choice operator V on a set S is a map associating to any subset A of S a non empty subset V (A) contained in A. A choice operator is path independent if it satisfies the following property:

for all A, B subsets of S V (A W B) = V (V (A)W V (B)).
It is easy to check that the set of all path-independent choice operators on S, ordered by the pointwise order between maps, is a join-semilattice (without lowest element).

A path-independent choice operator V P is associated with any poset P = (X, U ). It is obtained by associating to any subset A of P the set of its maximal elements. Formally, V P( A) = {xT A : there does not exist exists y T A with x<y}. We call such a path-independent choice operator an order choice operator, and in particular, a linear order choice operator, if P is linearly ordered.

The chosen sets by an order choice operator X P are the antichains of P, i.e. the subsets of P which do not contain two elements x and y with x<y.

It is easy to understand that the obvious one-to-one correspondence between order ideals and antichains of a poset induce a one to one correspondence between order closure operators and order choice operators. But this is a particular case of a general result [START_REF] Monjardet | The duality between the anti-exchange closure operators and the path independent choice operators on a finite set[END_REF]:

Theorem 20

The join-semilattice of all the path-independent choice operators on a set S is dual of the meetsemilattice of all the antiexchange closure operators on S.

Then, we have for instance the consequence that the representation result of any antiexchange closure operator as a meet of linear closure operators obtained by Edelman and Saks (1988, see also Matalon, 1965, P.96) is the same (under the duality) that the representation result of any path-independent choice operator as a join of linear choice operators obtained by Aizerman and Malishevski (1981). Moreover the use of the duality allows to get interesting precisions on the way to get such representations (see [START_REF] Monjardet | The duality between the anti-exchange closure operators and the path independent choice operators on a finite set[END_REF].

.

Remarks

1) The notion of path-independent choice operator introduced in Plott, 1973, have been previously studied by [START_REF] Afriat | Principles of choice and preference[END_REF]. Aizerman and Malishevski's representation result quoted just above amounts to say that choices by such an operator can be obtained by the so-called "extremal choice" mechanism, where the agent collects the best choices obtained under different -linearly ordered-criteria (see [START_REF] Aizerman | Theory of choice[END_REF].

2) The fact that there exists a one-to-one correspondence between antiexchange closure operators and path-independent choice operators has been independently obtained by [START_REF] Koshevoy | Choice functions and abstract convex geometries[END_REF] and [START_REF] Johnson | Locally complete path independent choice functions and their lattices[END_REF]. It would be interesting to find a Galois connection inducing this correspondence.

3) The closure systems corresponding to the antiexchange closure operators are called the convex geometries and are characterized by two properties: the empty set Ø is closed, and for every closed set C (Y S) there exists x `C such that C a {x} is closed. Since the poset of all convex geometries on S (ordered by set inclusion) is dual of the meet-semilattice of all the antiexchange closure operators on S, it is a join-semilattice isomorphic to the join-semilattice of all path-independent choice operators on S.

Conclusion

As said in our introduction order duality matters since as soon as two sets of objects are shown be two dual posets, then any result on one of these posets can be tranferred to the other. We still illustrate this point by a last (rather trivial) duality: the meet-semilattice of all asymmetric binary relations on a set S is dual of the join-semilattice of all complete relations on S (by the map R b R cd = {(x,y) : (y,x) c R}). Then to work, for instance in social choice, with asymmetric prefences is totally equivalent to work with complete preferences, a fact that is not universally well understood.

  for every C D P, f (C ) = R (C ), where for all x,y D A, [xR (C )y ] G [{i D N : xL i y} D ].