Bastien Maubert
email: bastien.maubert@irisa.fr

François Schwarzentruber
email: francois.schwarzentruber@bretagne.ens-cachan.fr

Keywords: Dynamic epistemic logic, tableau method, computational complexity

Dynamic Epistemic Logic (DEL) deals with the representation of situations in a multi-agent and dynamic setting. It can express in a uniform way statements about:

(i) what is true about an initial situation (ii) what is true about an event occurring in this situation (iii) what is true about the resulting situation after the event has occurred.

After proving that what we can infer about (ii) given (i) and (iii) and what we can infer about (i) given (ii) and (iii) are both reducible to what we can infer about (iii) given (i) and (ii), we provide a tableau method deciding whether such an inference is valid. We implement it in LOTRECscheme and show that this decision problem is NEXPTIME-complete. This contributes to the proof theory and the study of the computational complexity of DEL which have rather been neglected so far.

Tableau Method and NEXPTIME-Completeness of DEL-Sequents 1

Guillaume Aucher 2,3

IRISA INRIA -University of Rennes 1

Rennes, France

Introduction

Dynamic Epistemic Logic (DEL) deals with the logical study in a multi-agent setting of knowledge and belief change, and more generally of information change [van Ditmarsch et al., 2007]. To account for these logical dynamics, the core idea of DEL is to split the task of representing the agents' beliefs into three parts: first, one represents their beliefs about an initial situation; second, one represents their beliefs about an event taking place in this situation; third, one represents the way the agents update their beliefs about the situation after (or during) the occurrence of the event. Consequently, one can express uniformly within the logical framework of DEL epistemic statements about:

(i) what is true about an initial situation, (ii) what is true about an event occurring in this situation, (iii) what is true about the resulting situation after the event has occurred.

From a logical point of view, this trichotomy begs the following three questions. Given (i) and (ii), what can we infer about (iii)? Given (i) and (iii), what can we infer about (ii)? Given (ii) and (iii), what can we infer about (i)? Providing formal tools that can be used to answer these questions is certainly of interest for human or artificial agents. Indeed, they could not only use them to plan their actions to achieve a given epistemic goal (the first and second questions actually correspond respectively to the problems of deductive and abductive planning in the situation calculus), but they could also use them to explain and determine a posteriori the causes that lead to a given situation. Nevertheless, to be applicable, these formal tools should lead to implementable decision procedures. To this aim, we provide a tableau method giving an answer to the first question. This is sufficient since we prove that the two other questions are in fact both reducible formally to the first one.

The paper is organized as follows. In Section 2, we define our three DELsequents corresponding to our three questions above, and we show that these DEL-sequents are interdefinable. In Section 3, we provide two terminating, sound and complete tableau methods. This leads us to define in Section 4 an algorithm in NEXPTIME, which we prove to be optimal by reducing a tiling problem known to be NEXPTIME-complete to our decision problem. A link to an implementation of our tableau method in LOTRECscheme is provided in Section 5. Finally, we conclude in Section 6 by a discussion of related works.

Dynamic Epistemic Logic: DEL-sequents

Representation of the initial situation: L-model

In the rest of this paper, Φ is a set of propositional letters called atomic facts which describe static situations, and Agt is a finite set of agents. A L-model is a tuple M = (W, R, V ) where:

• W is a non-empty set of possible worlds,

• R : Agt → 2 W ×W is a function assigning to each agent j ∈ Agt an accessibility relation on W ,

• V : Φ → 2 W is a function assigning to each propositional letter of Φ a subset of W . The function V is called a valuation.

We write w ∈ M for w ∈ W , and (M, w) is called a pointed L-model (w often represents the actual world). If w, v ∈ W , we write wR j v for R(j) (w, v) and R j (w) = {v ∈ W | wR j v}. Intuitively, wR j v means that in world w agent j considers that world v might correspond to the actual world. Then, we define the following epistemic language L that can be used to describe and state properties of L-models:

L : ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | B j ϕ
where p ranges over Φ and j over Agt. We define ϕ ∨ ψ = def ¬(¬ϕ ∧ ¬ψ) and ⟨B j ⟩ϕ = def ¬B j ¬ϕ. The symbol ⊤ is an abbreviation for p ∨ ¬p for a chosen p ∈ Φ. Let M be a L-model, w ∈ M and ϕ ∈ L. M, w |= ϕ is defined inductively as follows:

M, w |= p iff w ∈ V (p) M, w |= ϕ ∧ ψ iff M, w |= ϕ and M, w |= ψ M, w |= ¬ϕ iff not M, w |= ϕ M, w |= B j ϕ iff for all v ∈ R j (w), M, v |= ϕ We write M |= ϕ when M, w |= ϕ for all w ∈ M, and |= ϕ when for all L-model M, M |= ϕ. An L-formula ϕ is said to be valid if |= ϕ.
The formula B j ϕ reads as "agent j believes ϕ". Its truth conditions are defined in such a way that agent j believes ϕ holds in a possible world when ϕ holds in all the worlds agent j considers possible.

Representation of the event: L ′ -model

The propositional letters p ′ ψ describing events are called atomic events and range over Φ ′ = {p ′ ψ ψ ranges over L}. The reading of p ′ ψ is "an event of precondition ψ is occurring". A L ′ -model is a tuple M ′ = (W ′ , R ′ , V ′ ) where:

• W ′ is a non-empty set of possible events, • R ′ : Agt → 2 W ′ ×W ′ is a function assigning to each agent j ∈ Agt an accessibility relation on W ′ , • V ′ : Φ ′ → 2 W ′ is a function assigning to each propositionnal letter of Φ ′ a subset of W ′ such that for all w ′ ∈ W ′ , there is at most one p ′ ψ such that w ′ ∈ V (p ′ ψ ) (Exclusivity). We write w ′ ∈ M ′ for w ′ ∈ W ′ , and (M ′ , w ′ ) is called a pointed L ′ -model (w ′ often represents the actual event). If w ′ , v ′ ∈ W ′ , we write w ′ R ′ j v ′ for R ′ (j)(w ′ , v ′ ) and R ′ j (w ′ ) = {v ′ ∈ W ′ | w ′ R ′ j v ′ }. Intuitively, v ′ ∈ R j (w ′ ) means
that while the possible event represented by w ′ is occurring, agent j considers possible that the possible event represented by v ′ is actually occurring. Our definition of a L ′ -model is equivalent to the definition of an action signature in the logical framework of [START_REF] Baltag | Logic for epistemic programs[END_REF]]. 6 Just as we defined a language L for L-models, we also define a language L ′ for L ′ -models:

L ′ : ϕ ′ ::= p ′ ψ | ¬ϕ ′ | ϕ ′ ∧ ϕ ′ | B j ϕ ′ where p ′
ψ ranges over Φ ′ = {p ′ ψ ψ ∈ L} and j over Agt. In fact, L ′ was already introduced in [START_REF] Baltag | The logic of public announcements, common knowledge and private suspicions[END_REF]. In the sequel, formulas of L ′ are always indexed by the quotation mark ′ , unlike formulas of L. The truth conditions of the language L ′ are identical to the ones of the language L. Let M ′ be a

L ′ -model, w ′ ∈ M ′ and ϕ ′ ∈ L ′ . M ′ , w ′ |= ϕ ′ is defined inductively as follows: M ′ , w ′ |= p ′ ψ iff w ′ ∈ V ′ (p ′ ψ ) M ′ , w ′ |= ¬ϕ ′ iff not M ′ , w ′ |= ϕ ′ M ′ , w ′ |= ϕ ′ ∧ ψ ′ iff M ′ , w ′ |= ϕ ′ and M ′ , w ′ |= ψ ′ M ′ , w ′ |= B j ϕ ′ iff for all v ′ ∈ R j (w ′ ), M ′ , v ′ |= ϕ ′

Update of the initial situation by the event: product update

A L ′ -model induces the definition of a precondition function. The precondition Pre(w ′ ) of a possible event w ′ corresponds to the property that should be true at a world w of a L-model so that the possible event w ′ can 'physically' occur in this world w. The precondition function Pre :

W ′ → L induced by the L ′ -model M ′ = (W ′ , R ′ , V ′ ) is defined as follows: Pre(w ′ ) = ψ if there is p ′ ψ such that M ′ , w ′ |= p ′ ψ ; Pre(w ′ ) = ⊤ otherwise.
We then redefine equivalently in our setting the BMS product update of [START_REF] Baltag | The logic of common knowledge, public announcement, and private suspicions[END_REF] as follows. Let (M, w) = (W, R, V, w) be a pointed Lmodel and let (M ′ , w ′ ) = (W ′ , R ′ , V ′ , w ′ ) be a pointed L ′ -model such that M, w |= Pre(w ′ ). The product update of (M, w) and (M ′ , w ′ ) is the pointed L-model (M ⊗ M ′ , (w, w ′ )) = (W ⊗ , R ⊗ , V ⊗ , (w, w ′ )) defined as follows:

• W ⊗ = {(v, v ′ ) ∈ W × W ′ | M, v |= Pre(v ′ )}, • R ⊗ j (v, v ′ ) = {(u, u ′ ) ∈ W ⊗ | u ∈ R j (v) and u ′ ∈ R ′ j (v ′ )}, • V ⊗ (p) = {(v, v ′ ) ∈ W ⊗ | M, v |= p}.
This product update yields a new L-model (M, w)⊗(M ′ , w ′ ) representing how the new situation which was previously represented by (M, w) is perceived by the agents after the occurrence of the event represented by (M ′ , w ′ ).

6 If Σ = (W ′ , R ′ , (w ′ 1 , . . . , w ′ n )) is an action signature and ϕ 1 , . . . , ϕ n ∈ L, then the L ′ - model associated to (Σ, ϕ 1 , . . . , ϕ n ) is the tuple M ′ = (W ′ , R ′ , V ′ ) where V ′ (p ′ ψ ) = {w ′ i } if ψ = ϕ i , V ′ (p ′ ψ ) = W ′ -{w ′ 1 , . . . , w ′ n } if ψ = ⊤, and V ′ (p ′ ψ ) = ∅ otherwise.

Definitions of our DEL-sequents

Let ϕ, ϕ ′′ ∈ L and ϕ ′ ∈ L ′ . We define the logical consequence relations ϕ, ϕ ′ ϕ ′′ , ϕ, ϕ ′′ 2 ϕ ′ and ϕ ′ , ϕ ′′ 3 ϕ as follows. The second and third relations can be used for epistemic planning and goal regression respectively. ϕ, ϕ ′ ϕ ′′ iff for all pointed L-model (M, w), and

L ′ -model (M ′ , w ′ ) such that M, w |= Pre(w ′ ), M, w |= ϕ and M ′ , w ′ |= ϕ ′ , it holds that (M, w) ⊗ (M ′ , w ′ ) |= ϕ ′′ ϕ, ϕ ′′ 2 ϕ ′ iff for all pointed L-models (M, w), and (M ′′ , w ′′ ) such that M, w |= ϕ and M ′′ , w ′′ |= ϕ ′′ , if (M ′ , w ′ ) is a pointed L ′ -model such that M, w |= Pre(w ′ ) and (M, w) ⊗ (M ′ , w ′ ) is bisimilar to (M ′′ , w ′′ ), then M ′ , w ′ |= ϕ ′ ϕ ′ , ϕ ′′ 3 ϕ iff for all pointed L ′ -model (M ′ , w ′ ), and L-model (M ′′ , w ′′ ) such that M ′ , w ′ |= ϕ ′ and M ′′ , w ′′ |= ϕ ′′ , if (M, w) is a pointed L-model such that M, w |= Pre(w ′ ) and (M, w) ⊗ (M ′ , w ′ ) is bisimilar to (M ′′ , w ′′ ), then M, w |= ϕ
In fact, as the following proposition shows, our three DEL-sequent are interdefinable. Therefore, in the rest of this paper, we will focus only on providing a tableau method for the DEL-sequent ϕ, ϕ ′ ϕ ′′ . Tableau methods and complexity results for the other DEL-sequents can easily be adapted from the ones provided for this DEL-sequent.

Proposition 2.1 For all ϕ, ϕ ′′ ∈ L and ϕ ′ ∈ L ′ , ϕ, ϕ ′′ 2 ϕ ′ iff ϕ, ¬ϕ ′ ¬ϕ ′′ ϕ ′ , ϕ ′′ 3 ϕ iff ¬ϕ, ϕ ′ ¬ϕ ′′

Tableau method

We consider three formulae, ϕ ∈ L, ϕ ′ ∈ L ′ and ϕ ′′ ∈ L, and we want to adress the problem of deciding whether ϕ, ϕ ′ |= ϕ ′′ holds. To do so we equivalently decide whether there exist a pointed L-model (M, w) and a pointed

L ′ -model (M ′ , w ′ ) such that M, w |= Pre(w ′ ), M, w |= ϕ, M ′ , w ′ |= ϕ ′ and M ⊗ M ′ , (w, w ′ ) |= ¬ϕ ′′ .
We call this dual problem the satisfiability problem.

Tableau method description

The formulas that appear in our tableau method and that we call tableau formulas are of the following kind:

• (l ϕ): l is a label l w (resp. l w ′ ) that represents a world of the model M (resp. M ′ ) being constructed, and ϕ is a formula of L (resp. L ′ ) that should be true at M, w (resp. M ′ , w ′ ).

• (l w l w ′ ϕ ′′ ): l w represents a world w of M, l w ′ a world w ′ of M ′ , and ϕ ′′ is a formula of L that should be true at M ⊗ M ′ , (w, w ′ ). Moreover,

(l w l w ′ 0) means that (w, w ′ ) is not in M ⊗ M ′ . • (R l l ′ ) (resp. (R ′ l l ′ )): R (resp. R ′ ) is some R j (resp. R ′ j )
, l and l ′ represent two worlds w and u (resp. w ′ and u ′ ) such that wR j u (resp. w ′ R j u ′ ).

• ⊥: Denotes an inconsistency.

A tableau rule is represented by a numerator N above a line and a finite list of denominators D 1 , . . . , D k below this line, separated by vertical bars:

N D 1 | . . . | D k
The numerator and the denominators are finite sets of tableau formulas. A tableau for a triple (ϕ, ϕ ′ , ϕ ′′ ) of formulas is a finite tree with a set of tableau formulas at each node, and whose root is:

Γ 0 = {(l w ϕ), (l w ′ ϕ ′ ), (l w l w ′ ϕ ′′ )}
A rule with numerator N is applicable to a node carrying a set Γ if Γ contains an instance of N . If no rule is applicable, Γ is said to be saturated. We call a node n an end node if the set of formulas Γ it carries is saturated, or if ⊥∈ Γ. The tableau is extended the following way:

(i) Choose a leaf node n carrying Γ where n is not an end node, and choose a rule ρ applicable to n.

(ii) (a) If ρ has only one denominator, add the appropriate instanciation to Γ. (b) If ρ has k denominators with k > 1, create k successor nodes for n, where each successor i carries the union of Γ with an appropriate instanciation of denominator D i .

A branch in a tableau is a path from the root to an end node. A branch is closed if its end node contains ⊥, otherwise it is open. A tableau is closed if all its branches are closed, otherwise it is open. A triple (ϕ, ϕ ′ , ϕ ′′ ) is said to be consistent if no tableau for (ϕ, ϕ ′ , ϕ ′′ ) is closed, and a triple (ϕ, ϕ ′ , ϕ ′′ ) is a theorem, which we write ϕ, ϕ ′ ϕ ′′ , if there is a closed tableau for (ϕ, ϕ ′ , ¬ϕ ′′ ).

Tableau rules

Common rules for M, M ′ and M ′′ (l is either l w , l w ′ or l w l w ′ ):

(l ϕ ∧ ψ) (l ϕ) (l ψ) ∧ (l ¬(ϕ ∧ ψ)) (l ¬ϕ) | (l ¬ψ) ¬∧ (l ¬¬ϕ) (l ϕ) ¬ (l p)(l ¬p) ⊥ ⊥
where p ∈ Φ Specific rules for M and M ′ (l is either l w or l w ′ ):

(l ⟨B j ⟩ϕ) (R l l ′ )(l ′ ϕ) ⟨B j ⟩ (l B j ϕ)(R l l ′ ) (l ′ ϕ) B j (l w ′ p ′ ϕ )(l w ′ p ′ ψ ) ⊥ Excl where ϕ ̸ = ψ Specific rules for M ′′ : (l w l w ′ ⟨B j ⟩ϕ) (R l w l u )(R ′ l w ′ l u ′ )(l u l u ′ ϕ) ⟨B j ⟩ ⊗ (l w l w ′ B j ϕ)(R l w l u )(R ′ l w ′ l u ′ ) (l u l u ′ ϕ)|(l u l u ′ 0) B j ⊗ (l w l w ′ p) (l w p) ← 1 (l w l w ′ ¬p) (l w ¬p) ← 2 (l w l w ′ 0)(l w ′ p ′ ψ ) (l w ¬ψ) Pre 1 (l w l w ′ ϕ)(l w ′ p ′ ψ ) (l w ψ) Pre 2 (l w l w ′ ϕ)(l w l w ′ 0) ⊥ ⊥ ′′
where ϕ ̸ = 0 where ϕ ̸ = 0 Remark 3.1 Another sound and complete tableau method can be obtained by replacing the rules Pre 1 and ⊥ ′′ above by the following rule:

(l w l w ′ 0) (l w ′ p ′ ψ 1 ) (l w ¬ψ 1 ) | . . . | (l w ′ p ′ ψn ) (l w ¬ψ n ) Pre ′ 1
where p ′ ψ 1 , . . . , p ′ ψn is the set of propositional letters appearing in ϕ ′ at the root of the tableau. This second tableau method is more modular, in the sense that if we remove Rule (Excl), then the resulting tableau method is still sound and complete with respect to the semantics where we do not impose the (Exclusivity) condition on L ′ -models. Note also that the L-model and L ′model obtained from an open branch with this tableau method do not need to be adapted to fulfill the satisfiability problem, as in the proof of Proposition 3.3 with the first tableau method.

Tableau method soundness and completeness

Proposition 3.2 (Tableau method soundness) For all ϕ, ϕ ′′ ∈ L, for all

ϕ ′ ∈ L ′ , ϕ, ϕ ′ ϕ ′′ implies ϕ, ϕ ′ ϕ ′′ Proof. Instead of proving that ϕ, ϕ ′ ⊢ ϕ ′′ implies ϕ, ϕ ′ |= ϕ ′′ , we equivalently prove that ϕ, ϕ ′ ϕ ′′ implies ϕ, ϕ ′ ϕ ′′ . Suppose there exist a pointed L-model (M, w), a L ′ -model (M ′ , w ′ ) such that M, w |= ϕ, M ′ , w ′ |= ϕ ′ , M, w |= Pre(w ′ ) and M ⊗ M ′ , (w, w ′ ) ϕ ′′ .
We must prove that every tableau for (ϕ, ϕ ′ , ¬ϕ ′′ ) has an open branch (the proof of termination is postponed to Section 4).

We say that a set Σ of tableau formulae is interpretable if there exist a Lmodel M, a L ′ -model M ′ , f : LABEL → W and f ′ : LABEL' → W ′ (where LABEL and LABEL' are the sets of labels for worlds appearing in Σ) such that (M, M ′ , f, f ′ ) makes all the tableau formulae in Σ true for the following semantics |= T :

(M, M ′ , f, f ′ ) |= T (l w ϕ) iff M, f (l w ) |= ϕ (M, M ′ , f, f ′ ) |= T (l w ′ ϕ ′ ) iff M ′ , f ′ (l w ′ ) |= ϕ ′ (M, M ′ , f, f ′ ) |= T (R l w l u ) iff f (l w )Rf (l u ) (M, M ′ , f, f ′ ) |= T (R ′ l w ′ l u ′ ) iff f ′ (l w ′ )R ′ f ′ (l u ′ ) (M, M ′ , f, f ′ ) |= T (l w l w ′ 0) iff M, f (l w ) Pre(f ′ (l w ′ )) (M, M ′ , f, f ′ ) |= T (l w l w ′ ϕ ′′ ) iff M, f (l w ) |= Pre(f ′ (l w ′ )) and M ⊗ M ′ , (f (l w ), f ′ (l w ′ )) |= ϕ ′′ (M, M ′ , f, f ′ ) |= T ⊥ iff false
Notice that since ϕ, ϕ ′ ϕ ′′ , the set Γ 0 = {(l w ϕ)(l w ′ ϕ ′ )(l w l w ′ ¬ϕ ′′ )} is interpretable. Furthermore, if a set of formulas is interpretable, it does not contain ⊥. So if we prove that when the numerator of a rule is interpretable, one of the denominators also is, then we have that every tableau for (ϕ, ϕ ′ , ¬ϕ ′′ ) has an open branch. We only prove it for the specific rules of M ′′ , the proof for the other rules being standard. In the following, when f is a function, we let f (x → a) be the function that maps x to a and y to f (y) if y ̸ = x.

Rule ⟨B j ⟩ ⊗ : If M, M ′ , f, f ′ |= T (l w l w ′ ⟨B j ⟩ϕ) then M ⊗ M ′ , (f (l w ), f ′ (l w ′ )) |= ⟨B j ⟩ϕ. So there exists (u, u ′ ) ∈ W ′′ such that (f (l w ), f ′ (l w ′ ))R ′′ (u, u ′ ) and M ⊗ M ′ , (u, u ′ ) |= ϕ. Since (f (l w ), f ′ (l w ′ ))R ′′ (u, u ′ ) we have that f (l w )Ru, f ′ (l w ′ )R ′ u ′ and M, u |= Pre(u ′ ). So by letting g := f (l u → u) and g ′ := f ′ (l u ′ → u ′ ) we have that M, M ′ , g, g ′ |= T {(R l w l u )(R ′ l w ′ l u ′ )(l u l u ′ ϕ)}. Rule B j ⊗ : If M, M ′ , f, f ′ |= T {(l w l w ′ B j ϕ)(R l w l u )(R ′ l w ′ l u ′ )} then M, f (l w ) |= Pre(f (l w ′ )), M ⊗ M ′ , (f (l w ), f ′ (l w ′ )) |= B j ϕ, f (l w )Rf (l u ) and f ′ (l w ′ )R ′ f ′ (l u ′ ). So, either M, f (l u )
Pre(l u ′ ) or M, f (l u ) |= Pre(l u ′ ). In the first case, M, M ′ , f, f ′ |= T (l u l u ′ 0). In the second case, (f (l u ), f ′ (l u ′ )) is a world of M ′′ , and (f (l w ),

f ′ (l w ′ ))R ′′ (f (l u ), f ′ (l u ′ )). Therefore we have M ⊗ M ′ , (f (l u ), f ′ (l u ′ )) |= ϕ, hence M, M ′ , f, f ′ |= T (l u l u ′ ϕ) Rules ← 1 and ← 2 : If M, M ′ , f, f ′ |= T {l w l w ′ p} then M, f (l w ) |= Pre(f (l w ′ ) and M ⊗ M ′ , (f (l w ), f ′ (l w ′ )) |= p. Since V ′′ (f (l w ), f ′ (l w ′ )) = V (f (l w )), we have that M, f (l w ) |= p, hence M, M ′ , f, f ′ |= T {(l w p)}. Rule ← 2 is proved similarly. Rules Pre 1 and Pre 2 : If M, M ′ , f, f ′ |= T {(l w l w ′ ϕ)(l w ′ p ′ ψ )} for some ϕ ̸ = 0, then M, f (l w ) |= Pre(f ′ (l w ′ )), and f ′ (l w ′ ) ∈ V ′ (p ′ ψ ). So M, f (l w ) |= Pre(p ′ ψ ), and M, M ′ , f, f ′ |= T (l w ψ). As for Rule Pre 1 , if M, M ′ , f, f ′ |= T {(l w l w ′ 0)(l w ′ p ′ ψ )}, then, by definition of |= T , M, f (l w ) |= ¬Pre(f (l w ′ ) and M ′ , f (l w ′ ) |= p ′ ψ .
Therefore, by the (Exclusivity) condition, Pre(f (l w ′ )) = ψ, and so M, f (l w ) |= ¬ψ, i.e. (l w ¬ψ).

Rule ⊥ ′′ : if ϕ ̸ = 0, then the set {(l w l w ′ ϕ)(l w l w ′ 0)} is not interpretable by definition. So the result trivially holds in this case. 2 Proposition 3.3 (Tableau method completeness) For all ϕ, ϕ ′′ ∈ L, for all ϕ ′ ∈ L ′ , ϕ, ϕ ′ ϕ ′′ implies ϕ, ϕ ′ ϕ ′′ .

Proof. In the proof of the proposition we make use of an unbounded number of atomic facts. So we start by showing that the case where Φ is finite reduces to the case where it is infinite. We define the L Φ -models as the L-models, where the valuation function has domain Φ. The epistemic language L Φ is defined like L, where the atomic facts range over Φ, and we write |= Φ ϕ if M |= ϕ for all L Φ -model M. We similarly define L ′ Φ ′ , and we write

L ′ Φ for L ′ {p ′ ψ | ψ∈L Φ } . We finally define ϕ, ϕ ′ |= Φ ϕ ′′ like ϕ, ϕ ′ |= ϕ ′′ ,
where models are L Φ -models and L ′ Φ -models. We just need to prove that for all Φ, for all ϕ, ϕ ′′ ∈ L Φ and ϕ

′ ∈ L ′ Φ , ϕ, ϕ ′ |= Φ ϕ ′′ implies that for all Φ * such that Φ ⊆ Φ * , it holds that ϕ, ϕ ′ |= Φ * ϕ ′′ .
Indeed, if this holds, then if ϕ, ϕ ′ |= Φ ϕ ′′ with Φ finite, we take some infinite Φ ⊆ Φ * , we have that ϕ, ϕ ′ |= Φ * ϕ ′′ ; hence if Proposition 3.3 holds for Φ infinite, it also holds for Φ finite.

To prove it we need the following result, in which, for ϕ ∈ L Φ and ϕ ′ ∈ L ′ Φ , ϕ ⊗ ϕ ′ ∈ L Φ is the progression of ϕ by ϕ ′ (see [Aucher, 2011] for definition).

Theorem 3.4 ([Aucher, 2011]) For any Φ, for any

ϕ, ϕ ′′ ∈ L Φ and ϕ ′ ∈ L ′ Φ , ϕ, ϕ ′ |= Φ ϕ ′′ iff |= Φ ϕ ⊗ ϕ ′ → ϕ ′′ (note that ϕ ⊗ ϕ ′ → ϕ ′′ is an L Φ -formula).
Let Φ be a set of propositional letters and let ϕ,

ϕ ′′ ∈ L Φ and ϕ ′ ∈ L ′ Φ . Asssume that ϕ, ϕ ′ |= Φ ϕ ′′ . Now let Φ * such that Φ ⊆ Φ * . By Theorem 3.4, |= Φ ϕ ⊗ ϕ ′ → ϕ ′′ . Besides, |= Φ * ϕ ⊗ ϕ ′ → ϕ ′′ also holds because Φ ⊆ Φ * and ϕ ⊗ ϕ ′ → ϕ ′′ ∈ L Φ . Then, by Theorem 3.4 again, ϕ, ϕ ′ |= Φ * ϕ ′′ .
We now prove Proposition 3.3 in the case where Φ is infinite. We prove that ϕ, ϕ ′ ϕ ′′ implies ϕ, ϕ ′ ϕ ′′ . Suppose there is a tableau for (ϕ, ϕ ′ , ¬ϕ ′′ ) that has an open branch, we prove that there exist a pointed L-model (M, w) and a pointed

L ′ -model (M ′ , w ′ ) such that M, w |= Pre(w ′ ), M, w |= ϕ, M ′ , w ′ |= ϕ ′ and M ⊗ M ′ , (w, w ′ ) |= ¬ϕ ′′ .
Let Γ f be the set of tableau formulas carried by the end node of the open branch. We define M and M ′ as follows. Each of them is built in two steps.

• Let M = (W, R, V ) with W = {w | (l w ψ) ∈ Γ f } and R = {(w, u) | (R l w l u ) ∈ Γ f }. V is defined in two steps : for all atoms p that appear in ϕ or ϕ ′′ , V (p) = {w | (l w p) ∈ Γ f }.
Then, for each world w in W , we assign a fresh atomic variable p w , and define V (p w ) = {w}. This is possible because Φ is infinite.

• Let M ′ = (W ′ , R ′ , V ′ ) with W ′ = {w ′ (l w ′ ψ) ∈ Γ f }, V (p ′ ψ ) = {w ′ | (l w ′ p ′ ψ ) ∈ Γ f }, and R ′ = {(w ′ , u ′ ) | (R ′ l w ′ l u ′ ) ∈ Γ f }. Moreover, for all w ′ ∈ M ′ such that there is no (l w ′ p ′ ψ ) ∈ Γ f , we set w ′ ∈ V ′ (p ′ ψ w ′ ),
where ψ w ′ is defined as follows : let

S w ′ = {w | ∃ϕ ̸ = 0, (l w l w ′ ϕ) ∈ Γ f }; then ψ w ′ = ∨ w∈S w ′ p w .
Note that by soundness of Rule (Excl), M ′ satisfies the exclusivity condition.

Finally, we define M ′′ as M ⊗ M ′ (we will prove later that M, w |= Pre(w ′ )). Lemmas 3.5 and 3.6 below establish the completeness of our tableau method.2

Lemma 3.5 If (l w ϕ) ∈ Γ f then M, w |= ϕ, and if (l w ′ ϕ ′ ) ∈ Γ f then M ′ , w ′ |= ϕ ′ .
Proof. We only prove it for M, it is similar for M ′ . The proof is done by induction on ϕ. p, ¬p: by definition of V . As for the case ϕ ∧ ψ, by saturation of rule ∧, Γ f also contains (l w ϕ) and (l w ψ). By induction hypothesis we have that M, w |= ϕ and M, w |= ψ, so M, w |= ϕ ∧ ψ. The cases ¬(ϕ ∧ ψ) and ¬¬ϕ are proved similarly.

⟨B j ⟩ϕ: By saturation of rule ⟨B j ⟩ there exists l u such that (R l w l u ) ∈ Γ f and (l u ϕ) ∈ Γ f . By induction hypothesis M, u |= ϕ, and wRu holds by construction of M, so M, w |= ⟨B j ⟩ϕ.

B j ϕ: Take some u in W such that wRu holds, we prove that M, u |= ϕ and conclude that M, w |= B j ϕ. Since wRu holds we know by construction of M that (R l w l u ) is in Γ f . So by saturation of rule B j , (l u ϕ) also belongs to Γ f , and by induction hypothesis

M, u |= ϕ. 2 Lemma 3.6 If there is ϕ ′′ ̸ = 0 such that (l w l w ′ ϕ ′′ ) ∈ Γ f , then M, w |= Pre(w ′ ) and M ⊗ M ′ , (w, w ′ ) |= ϕ ′′ .
Proof. We first prove the following Fact:

Fact 3.7 If (l w l w ′ ϕ) ∈ Γ f with ϕ ̸ = 0, then M, w |= Pre(w ′ ).
Assume towards a contradiction that M, w Pre(w ′ ). There are then two cases: either there is (l

w ′ p ′ ψ ) ∈ Γ f or there is no (l w ′ p ′ ψ ) ∈ Γ f .
In the first case, M, w ψ because ψ = Pre(w ′ ) by the (Exclusivity) condition. However, by the rule Pre 2 , (l w ψ) ∈ Γ f . Then, by Lemma 3.5, M, w |= ψ. This is impossible. In the second case, M ′ , w ′ |= p ′ ψ w ′ by definition of V ′ , and therefore Pre(w ′ ) = ψ w ′ . Besides, M, w |= p w by definition of V , and since (l w l w ′ ϕ) ∈ Γ f for some ϕ ̸ = 0, |= p w → ψ w ′ . So M, w |= ψ w ′ , and finally M, w |= Pre(w ′ ), which is impossible.

We can now prove Lemma 3.6. We prove it by induction on ϕ. (ii) If ⊥ ∈ Γ ′ i , we stop the current execution; (iii) Γ i+1 := the set of tableau formulas obtained by applying ⟨B j ⟩, B j , ⟨B j ⟩ ⊗ , B j ⊗ on Γ ′ i .

Step 1 is non-deterministic and corresponds to a Boolean saturation of labels of depth i. It non-deterministically runs in linear size of Γ i . Step 2 consists in checking if rule ⊥ has been executed. In this case, the current execution halts. Step 3 produces tableau formulas where labels are of depth i + 1.

Note that the maximal depth of formulas ψ ′′ in tableau formulas of the form (l u l u ′ ψ ′′ ) in Γ i is strictly decreasing with i (see rule ⟨B j ⟩ ⊗ and B j ⊗ ). So when i > δ(ϕ ′′ ), there is no more tableau formula of the form (l u l u ′ ψ ′′ ) in Γ i with ψ ′′ ̸ = 0. So when i > δ(ϕ ′′ ), the rules Pre 2 , ⟨B j ⟩ ⊗ and B j ⊗ will no more be applied.

Likewise, the maximal depth of formulas ψ (resp. ψ ′ ) in tableau formulas of the form (l u ψ) (resp. (l u ′ ψ ′ )) in Γ i is strictly decreasing with i. Moreover the depth of the formulas ψ appearing in a tableau formula of the form (l u ψ) is less than max{δ(ϕ), max k∈{1,...,n} δ(ψ k )}, and the depth of the formulas ψ ′ appearing in a tableau formula of the form (l u ′ ψ ′ ) is less than δ(ϕ ′ ).

At the end, Γ N +1 = ∅ and the algorithm has applied rules until saturation, that is, the set of tableau formulas ∪ N i=0 Γ i is saturated. Now let us have a look at the time required to execute the algorithm. Let x be the size of the input, that is the sum of the sizes of ϕ, ϕ ′ , ϕ ′′ and Pre(p ′ ψ k ).

Step 1 saturates the worlds u, u ′ and (u, u ′ ) appearing in the tableau formulas in Γ i . For each of those worlds, the saturation is linear in x.

Step 3 creates new tableau formulas for each ⟨B j ⟩-formula appearing in Γ ′ i . So for each world in Γ i it produces at most 2x new worlds. If we note y i the maximal number of worlds in Γ i , we have that y i+1 = 2xy i . So y i = (2x) i . The number of created worlds is bounded by (2x) x+1 and this construction takes an exponential amount of time.

2

To prove NEXPTIME-hardness of the satisfiability problem, we will reduce a NEXPTIME-complete tiling problem to it [Boas, 1997]. Let k be a natural number.

A tile type t is a 4-tuple of colors t = (lef t(t), right(t), up(t), down(t)). The tiling problem we consider is defined as follows.

• Output: yes iff we can tile a k × k grid with the tile types of T and t 0 being placed onto (0, 0).

In other worlds, the problem is to decide whether there exists a function τ from {1, . . . k} 2 to T satisfying the following constraints:

(i) τ (0, 0) = t 0 ;

(ii) up(τ (x, y)) = down(τ (x, y + 1)) for all x ∈ {1, . . . , k}, y ∈ {1, . . . , k -1};

(iii) right(τ (x, y)) = lef t(τ (x+1, y)) for all x ∈ {1, . . . , k -1}, y ∈ {1, . . . , k}.

Proposition 4.2

The satisfiability problem is NEXPTIME-hard.

Proof. Without loss of generality we may assume that k = 2 n . Let us consider an instance (T, t 0 , k) of the tiling problem. We now define three formulas ϕ, ϕ ′ , ϕ ′′ that are computable in polynomial time in |T | and n such that it is possible to tile a k × k grid with the tile types of T and t 0 being placed onto (0, 0) iff (ϕ, ϕ ′ , ϕ ′′ ) is satisfiable.

There is a modal formula χ of length O(n 2 ) which is satisfied in a frame iff the model contains as a submodel a binary tree of depth 2n, for instance:

χ = ∧ l<2n B j l ( (⟨B j ⟩p l ∧ ⟨B j ⟩¬p l ) ∧ ∧ i<l ((p i → B j p i ) ∧ (¬p i → B j ¬p i ))
) .

The 2 2n leaves of the tree are labeled by 2n-tuples containing either p i or ¬p i for i < 2n. The 2 2n leaves correspond to the 2 2n tile locations (x, y) in the following sense: the values of the propositions p i , where i < n, correspond to the binary representation of the abscissa x and the values of the propositions p i , where n ≤ i < 2n, correspond to the binary representation of the ordinate y. For instance, for n = 4 the location where x = 4 and y = 3 is represented by the following valuation: ¬p 0 , p 1 , ¬p 2 , ¬p 3 4 ¬p 4 , ¬p 5 , p 6 , p 7 3

The idea of encoding the existence of a k × k tiling is as follows:

• ϕ encodes a tiling τ 1 with such a binary tree such that τ 1 (0, 0) = t 0 ;

• ϕ ′ also encodes a tiling τ 2 wich such a binary tree;

• ϕ ′′ encodes that τ 1 = τ 2 = τ , and constraints (ii) and (iii) of the tiling τ .

Defining ϕ

We define the following formula:

path = ⟨B j ⟩ 2n+|T | ⊤ ∧ ∧ i<2n+|T | B j i ⟨B j ⟩⊤.
The formula path says that there is a path whose length is greater that 2n+|T | but no shorter path in the model.

In order to define ϕ, each tiling type t is used as a proposition in the language, and means : 'for the current location (x, y), we have τ 1 (x, y) = t'.

We define ϕ by:

ϕ = χ ∧ B j 2n ( path ∧ ∨ t∈T t ∧ ∧ t∈T (t → ∧ u∈T,u̸ =t ¬u) ∧ (( ∧ i<2n ¬p i ) → t 0 )
) Defining ϕ ′ For all i, we define l

′ i = ⟨B j ⟩ i+1 B j ⊥. Let χ ′ = ∧ i<2n B j i ( ⟨B j ⟩B j 2n-i-1 l ′ i ∧ ⟨B j ⟩B j 2n-i-1 ¬l ′ i ) .
The formula χ ′ has the same aim as χ and enables to enforce the existence of a binary tree where leaves correspond to the locations (x, y) of the tiling τ 2 . Formulas l ′ i for i < 2n represent the binary representation of (x, y).

Let t 1 , . . . , t |T | be an enumeration of elements of T . In order to define ϕ ′ , for each tiling type t i we use the formula t ′ i = l ′ i+2n in the language whose intuitive meaning is 'for the current location (x, y), we have τ 2 (x, y) = t i .

We define ϕ ′ by where goodP roduct = ∧ i≤2n+2n+|T |+1 B j i p ′ ⊤ ensures that all worlds (w, w ′ ) appear in the product model.

ϕ ′ = χ ′ ∧

Defining ϕ ′′

The formula ϕ ′′ will consider all the leaves (w, w ′ ) of the product model where w is a leaf of the model M and w ′ is a leaf of the model M ′ in order to encode the fact that τ 1 = τ 2 and the constraints (ii) and (iii).

We define ϕ ′′ by: ))] where:

ϕ ′′ = B j
• α = ∧ i<n (p i ↔ l ′ i ) means 'the abscissa x of the tile location of w is equal to the absissa x ′ of the tile location of w ′ ';

• β = ∧ n≤i<2n (p i ↔ l ′ i ) means 'the ordinate y of the tile location of w is equal to the ordinate y ′ of the tile location of w ′ ';

• α 1 = ∨ i<n ( ∧ j<i (p j ↔ l ′ j ) ∧ ¬p i ∧ l ′ i ∧ ∧ i<j<n (p j ∧ ¬l ′ j )
) means ''the abscissa x of the tile location of w and the absissa x ′ of the tile location of w ′ ' are such that x ′ = x + 1;

• β 1 = ∨ n≤i<2n ( ∧ n≤j<i (p j ↔ l ′ j ) ∧ ¬p i ∧ l ′ i ∧ ∧ i<j<2n (p j ∧ ¬l ′ j )
) means ''the ordinate y of the tile location of w and the ordinate y ′ of the tile location of w ′ ' are such that y ′ = y + 1.

  p, ¬p: By Rule ← 1 , (l w p) ∈ Γ f , and so M, w |= p by Lemma 3.5. Moreover, by Fact 3.7, M, w |= Pre(w ′ ). Therefore, M⊗M ′ , (w, w ′ ) |= p by definition of the product update. The proof for ¬p is similar to the case of p. The proof of the other boolean cases ϕ ∧ ψ, ¬(ϕ ∧ ψ) and ¬¬ϕ is obtained by max k∈{1,...,n} δ(ψ k )}. The algorithm runs as follows. For i = 0 to N , we execute: (i) Γ ′ i := the saturation of Γ i by rules ∧, ¬∧, ¬, ⊥, Excl, ← 1 , ← 2 , Pre 1 , Pre 2 , ⊥ ′′ ;

δ(ϕ) is defined inductively as follows: δ(p) = 0, δ(¬ϕ) = δ(ϕ), δ(ϕ∧ψ) = max{δ(ϕ), δ(ψ)} and δ(B j ϕ) = 1 + δ(ϕ).

• Input: a finite set T of tile types, a t 0 ∈ T and a natural number k written in its binary form.

applying straightforwardly the Induction Hypothesis.

⟨B j ⟩ϕ: If (l w l w ′ ⟨B j ⟩ϕ) ∈ Γ f , then by saturation of Rule ⟨B j ⟩ ⊗ , (R l w l u ), (R ′ l w ′ l u ′ ) and (l u l u ′ ϕ) belong to Γ f . By application of Fact 3.7, M, w |= Pre(w ′ ). Now, by definition of M and M ′ , u ∈ R(w) and u ′ ∈ R ′ (w ′ ). Moreover, (l u l u ′ ϕ) ∈ Γ f and ϕ ̸ = 0, so by Fact 3.7, M, u |= Pre(u ′ ), hence (u, u ′ ) ∈ R(w, w ′ ). By application of the induction hypothesis,

) by definition of the product update. Then, by definition of M and M ′ , (R

In the first case, assume that there is (l u ′ p ′ ψ ) ∈ Γ f . Then, by saturation of Rule Pre 1 , (l u ¬ψ) ∈ Γ f . Therefore, M, u |= ¬ψ by Lemma 3.5. This is impossible because M ′ , u ′ |= p ′ ψ , and so M, u |= ψ should also hold because (u, u ′ ) ∈ M ⊗ M ′ . Therefore, there is no (l

There is a contradiction, so this case is impossible. Proof. The tableau rules presented in Section 3.2 give rise to a nondeterministic algorithm running in exponential time. We say that a label l u is of depth k if there is a sequence w = u 1 , . . . , u k = u such that (R l w i l w i+1 ) for all i < k. Let p ′ ψ 1 , . . . , p ′ ψn be the set of atomic propositions appearing in ϕ ′ . Let δ(.) be the function that gives the modal depth of a given formula. 7 The algorithm starts with the following set of tableau for-

We leave the reader prove that we can tile a k × k grid with the tile types of T and t 0 being placed onto (0, 0) iff (ϕ, ϕ ′ , ϕ ′′ ) is satisfiable. 2

Implementation

The tableau method described in Remark 3.1 of Section 3.2 is implemented in LoTRECScheme (a variant of LoTREC [START_REF] Gasquet | LoTREC: Logical Tableaux Research Engineering Companion[END_REF] written in Scheme). Contrary to LoTREC, the system of LoTRECScheme allows the name of a node to be a couple (w, w ′ ) and this functionnality is suitable for our tableau rules. You can find the implementation at the following web page:

http://www.irisa.fr/prive/fschwarz/publications/m4m2011/.

Concluding remarks and related work

This paper contributes to the proof theory and the study of the computational complexity of DEL, which has been rather neglected so far. Indeed, most work in this field has often been inspired or applied to logico-philosophical puzzles such as for example the muddy children riddle, Fitch paradox, or Moorean sentences. Up to our knowledge, the only known results of computational complexity are the PSPACE-completeness of the satisfiability problem for public announcement logic [Lutz, 2006] and the polynomial time upper bound of the model-checking problem for public announcement logic. As for proof theory, a sound and complete sequent calculus for DEL has been developped in [Baltag et al., 2004], yet in an algebraic setting. Because of this different setting, the comparison cannot be systematic, but, unlike our DEL-sequents, their sequents m 1 , . . . , q 1 , . . . , A 1 , . . . , m k , . . . , q l , . . . , A n ⊢ δ are arbitrarily long and consist of different types of formulas which can contain propositions m 1 , . . . , m k , events q 1 , . . . , q l and agents A 1 , . . . , A n , and which resolve into a single proposition or event δ. Some tableau methods have been proposed for DEL, but only for public announcement logic [START_REF] Balbiani | Tableaux for public announcement logic[END_REF],de Boer, 2007] and hybrid public anouncement logic [Hansen, 2010]. A terminating tableau method has also been proposed for the full BMS framework in [Hansen, 2010] by encoding the reduction axioms as tableau rules. However, none of these tableau methods can somehow address the three questions raised in the introduction, because the BMS language of [START_REF] Baltag | Logic for epistemic programs[END_REF] does not allow for partial and incomplete descriptions of events: an event model or a formula announced publicly specifies completely how all the agents perceive the occurrence of the corresponding event.


Zainab Assaghir
email: assaghiz@loria.fr

Amedeo Napoli
email: napoli@loria.fr

Mehdi Kaytoue
email: kaytoue@dcc.ufmg.br

Didier Dubois
email: dubois@irit.fr

Numerical information fusion: Lattice of answers with supporting arguments

Keywords: numerical information fusion, reliability, formal concept analysis, pattern structure, lattice of arguments

The problem addressed in this paper is the merging of numerical information provided by several sources. Merging conflicting pieces of information into an interpretable and useful format is a tricky task even when an information fusion method is chosen. The use of formal concept analysis and pattern structures enables us to associate subsets of sources to combination results obtainable from consistent subsets of pieces of information. This provides a lattice of arguments where the reliability of sources can be taken into account. Instead of providing a unique fusion result, the method yields a structured view of partial results labelled by subsets of sources and allows us to argue about the most appropriate evaluation. The approach is illustrated with an experiment on a real-world application to decision aid in agricultural practices.

I. INTRODUCTION

In several application domains, information is available from several sources rather than a single one. Extracting consistent and useful pieces of information from such distributed sources is the major task of information fusion [START_REF] Bloch | Fusion: General concepts and characteristics[END_REF]. Moreover information delivered by sources may be uncertain or imprecise, and then these aspects have to be taken into account in information fusion. There are several information fusion operators for combining pieces of information that may be often conflicting [START_REF] Dubois | Possibility theory and data fusion in poorly informed environments[END_REF]. These fusion operators are applied on the set of all sources and provide a result.

In this work, we use Formal Concept Analysis (FCA) to draw a map of all subsets of sources and the information they provide [START_REF] Ganter | Formal cConcept Analysis[END_REF]. The main capability of FCA is to produce pairs of subsets of totally related entities called formal concepts. Hence, concepts encode maximal sets of sources associated with the result of the fusion process. Concepts are ordered and form a structure called concept lattice. This lattice is meaningful for organizing information fusion results from different subsets of sources and allows more flexibility for the user. Moreover, the lattice keeps track of the origin of the information such as presented in [START_REF] Dubois | Dealing with multi-source information in possibilistic logic[END_REF] for the fusion of symbolic information. Besides, the paper investigates a method for coping with inconsistency, by defining a suitable notion of lattice of arguments, when merging inconsistent information.

This work can be used in many applications where it is necessary to find a suitable value summarizing several estimates coming from multiple sources and to support a decision. Here, we use an experiment in agronomy for decision-support in agricultural practices.

The paper is organized as follows. Section II introduces the preliminaries on FCA and its extension for handling numerical data. Then, Section III shows how FCA is well suited for organizing different information fusion results. Section IV introduces the notion of lattice of arguments. Then, Section V presents how the reliability of sources can be taken into account. Section VI describes a real-world experiment: a concept lattice embedding fusion results is interpreted for making decisions about agricultural practices.

II. FORMAL CONCEPT ANALYSIS

m 1 m 2 g 1 × g 2 × g 3 × × g 4 × Table I A FORMAL CONTEXT

A. Basics

Formal Concept Analysis (FCA) is a method mainly used for the analysis of data. Implicit relationships between objects can be derived and described through a set of attributes. The FCA formalism is based on lattice structures [START_REF] Ganter | Formal cConcept Analysis[END_REF]. FCA computes a concept lattice which provides a classification of objects in a domain. FCA starts from a binary table called formal context (G, M, R) that represents a relation R between a set of objects G and a set of attributes M . The statement (g, m) ∈ R is interpreted as "object g has attribute m". An example of formal context is given on Table I where a table entry contains a cross (×) iff the object in the corresponding row possesses the attribute in the corresponding column, e.g. g 1 has attribute m 1 , i.e.

(g 1 ,m 1 ) ∈ R. The two operators (•) ′ define a Galois connection between the powersets (2 G , ⊆) and (2 M , ⊆), with A ⊆ G and B ⊆ M :

A ′ = {m ∈ M |∀g ∈ A : gRm} for A ⊆ G, B ′ = {g ∈ G |∀m ∈ B : gRm} for B ⊆ M A pair (A, B), such that A ′ = B and B ′ = A, where A ⊆ G, B ⊆ M , is called a (formal) concept, e.g.
({g 1 ,g 2 ,g 3 }, {m 1 }). A concept includes both notions of maximality and generalization/specialization: a concept corresponds to a maximal set of objects (extent) sharing a common maximal set of attributes (intent). The set A of objects is called the extent and the set B of properties is the intent of the concept (A, B).

Concepts are then partially ordered to form a lattice. The generalization/specialization is given by the partial ordering of concepts. Concepts are partially ordered by

(A 1 ,B 1 ) ≤ (A 2 ,B 2 ) ⇔ A 1 ⊆ A 2 (⇔ B 2 ⊆ B 1 ), e.g. the concept ({g 3 }, {m 1 ,m 2 }) is a sub-concept of ({g 1 ,g 2 ,g 3 }, {m 1 }).
With respect to this partial order, the set of all formal concepts forms a complete lattice called the concept lattice of the formal context (G, M, R). Figure 1 shows the concept lattice 1 associated with the context in Table I. On the diagram, each node denotes a concept while a line denotes an order relation between two concepts. Due to reduced labeling, the extent of a concept is composed of all objects lying in the extents of its sub-concepts. Dually, the intent of a concept is composed of all attributes in the intents of its super-concepts. The top concept (⊤) of the lattice contains all objects and the bottom concept (⊥) in the lattice contains all properties. Thus, FCA allows us to associate a maximal subset of objects with a maximal subset of attributes.

Real-world data in biology, agronomy, etc., usually consist in complex data involving numbers, intervals, graphs, etc. (e.g. Table II). FCA cannot be directly applied to such data. They can be processed with FCA after a transformation, called conceptual scaling, e.g. discretization. Transformations generally imply an important loss of information (e.g. links between objects) and arbitrary choices. However, there are means to handle numerical values and intervals in an elegant and efficient way in FCA. For that purpose, Ganter and Kuznetsov [START_REF] Ganter | Pattern Structures and Their Projections[END_REF] define pattern structures that directly handle complex data such as given in Table II.

m 1 m 2 g 1 [1, 5] [1, 9] g 2 [2, 3] [1, 3] g 3 [4, 7] [6, 7] g 4 [6, 10] [8, 9]

B. Pattern structures for complex data

Pattern structures are introduced in [START_REF] Ganter | Pattern Structures and Their Projections[END_REF] as an extension of FCA to handle complex data. When working with classical FCA, the object descriptions are sets of attributes, and are partially ordered by set inclusion. But inclusion is the canonical ordering on sets, induced by set-intersection: let P, Q ⊆ M be two attribute sets, then P ⊆ Q ⇔ P ∩Q = P . So the partially ordered set of attributes (M, ⊆) can as well be written (M, ∩). Based on this remark, a meet operator denoted by ⊓, idempotent, commutative and associative, can be applied on the set of object descriptions and the potential descriptions are ordered in a meet-semi-lattice w.r.t. the induced ordering ⊓. Therefore, a pattern structure entails a Galois connection between the powerset of objects (2 G , ⊆) and a meet-semi-lattice of descriptions denoted by (D, ⊓).

Formally, let G be a set of objects, let (D, ⊓) be a meetsemi-lattice of potential object descriptions and let δ : G -→ D be a mapping.

(A 2 ,d 2 ) ⇔ A 1 ⊆ A 2 (⇔ d 2 ⊑ d 1 )
, the set of all concepts forms a complete lattice called a (pattern) concept lattice.

Pattern structures allow us to consider complex data in full compliance with FCA formalism. It requires the definition of a meet operator on object descriptions, inducing their partial order. Actually, as for scaling in classical FCA, the choice of an operator depends on expert knowledge, and the context in which the resulting concept lattice will be used.

III. INFORMATION FUSION USING FCA

In information fusion, the question is to synthesize several pieces of information, providing by different sources, into an interpretable and useful information. Pieces of numerical information supplied by sources are often imprecise. The simplest representation of this imprecision consists of intervals. For example, Table II represents an example of information fusion problem : how to synthesize a useful value for m 1 (resp. for m 2 ), based on values provided by information sources g i , i =1,...,4, to be used in an evaluation process. According to [START_REF] Bloch | Fusion: General concepts and characteristics[END_REF], [START_REF] Dubois | Possibility theory and data fusion in poorly informed environments[END_REF], there are three kinds of behaviors for a fusion operator denoted f : conjunctive, disjunctive and mild operators.

• The basic conjunctive operator is a set intersection. It is used when all the sources are reliable, and usually results in a more precise information item. If there is some conflict in the information, then the result of the conjunction can be empty. For example, considering Table II, the conjunctive fusion result is an emptyset for the variable m 1 . • The basic disjunctive operator is a set union. It is used when at least one of the sources is reliable without knowing which sources are so. The result of a disjunctive operator can be considered as reliable, but is also often imprecise. For example, the disjunctive fusion result for the variable m 1 , in Table II, is [START_REF] Bloch | Fusion: General concepts and characteristics[END_REF][START_REF] Assaghir | Fuzzy logic approach to represent and propagate imprecision in agrienvironmental indicator assessment[END_REF]. • A mild operator lies between conjunction and disjunction, and is typically used when sources are partly conflicting. It tries to achieve a good balance between informativeness and reliability. The fusion based on Maximal Consistent Subset (MCS) is an example of mild operator, which consists in finding maximal consistent conjunctions of sources, then returning the disjunction of these maximal sets [START_REF] Dubois | Multiple source information fusion: a practical inconsistency tolerant approach[END_REF], [START_REF] Destercke | Possibilistic information fusion using maximal coherent subsets[END_REF]. Going back to Table II, maximal consistent subsets of values for m 1 are [2, 3], [START_REF] Dubois | Dealing with multi-source information in possibilistic logic[END_REF][START_REF] Ganter | Pattern Structures and Their Projections[END_REF] and [START_REF] Dubois | Multiple source information fusion: a practical inconsistency tolerant approach[END_REF][START_REF] Destercke | Possibilistic information fusion using maximal coherent subsets[END_REF] provided respectively by subsets {g 1 ,g 2 }, {g 1 ,g 3 } and {g 3 ,g 4 }. Then, the MCS fusion result is given by

[2, 3] ∪ [4, 5] ∪ [6, 7].
Conjunctive and disjunctive fusion operators are commutative, associative and idempotent. The mild operators are commutative and idempotent but they not associative. Nevertheless, fusion operators are generally applied to all sources and the obtained result (called also global result) is considered by users for the evaluation process. Sometimes, it happens that this result is not useful, e.g. the intersection of all sources in Table II is an emptyset. Then, we are interested to consider subsets of pieces of information provided by sources. Thus, it may be useful to keep sources distinct and exploit the partial fusion results (i.e. results obtained from subsets of sources). Nevertheless, there exist 2 n subsets of sources for a set of n sources. On the other hand, FCA (in particular pattern structure) starts from a similar kind of information as in information fusion problem table. Moreover, it produces concepts corresponding to maximal sets of objects associated with a maximal set of values [START_REF] Assaghir | Managing information fusion with formal concept analysis[END_REF].

Then, FCA (i.e. pattern structures for numerical data) can be used to combine numerical information coming from several sources. Indeed, information sources (resp. variables) in information fusion problems play the role of objects (resp. attributes) in the pattern structure formalism. Moreover a fusion operator is considered as a meet operator in pattern structures and FCA formalism. Let us consider a set of sources G = {g 1 ,g 2 ,...,g n }. Each source g i provides an information item in the form of an interval [a i ,b i ] for a parameter m. f m a fusion operator and f m (g i ,g j ) is the fusion result of information items coming from g i and g j .

Definition 1: An information fusion space D m is composed of the information available for a parameter m and all possible fusion results they provide, w.r.t a fusion operator

f m . Formally, D m = {f m (g i ∈ H), ∀H ⊆ G}.
Going back to Table II, with variable m 1 and f 1 being the conjunctive fusion operator (i.e. interval intersection), [START_REF] Dubois | Dealing with multi-source information in possibilistic logic[END_REF][START_REF] Destercke | Possibilistic information fusion using maximal coherent subsets[END_REF], [START_REF] Dubois | Multiple source information fusion: a practical inconsistency tolerant approach[END_REF][START_REF] Assaghir | Fuzzy logic approach to represent and propagate imprecision in agrienvironmental indicator assessment[END_REF], [START_REF] Dubois | Possibility theory and data fusion in poorly informed environments[END_REF][START_REF] Ganter | Formal cConcept Analysis[END_REF], [START_REF] Dubois | Dealing with multi-source information in possibilistic logic[END_REF][START_REF] Ganter | Pattern Structures and Their Projections[END_REF], [START_REF] Dubois | Multiple source information fusion: a practical inconsistency tolerant approach[END_REF][START_REF] Destercke | Possibilistic information fusion using maximal coherent subsets[END_REF], ∅}.

D m1 = {[1, 5],

A. Lattice of conjunctive results

The conjunctive fusion operator f m = ∩, for a parameter m, is commutative, associative and idempotent. Then, it can be considered as a meet operator and (D m , ∩) is an information meet-semi-lattice. Consequently, (G, (D m , ∩),δ) is a pattern structure and we can build the lattice given in Figure 2.

On Figure 2, from the FCA point of view, each node denotes a concept while a line denotes an order relation between two concepts (i.e., interval inclusion). In information fusion problems, each node contains a subset of sources (extent in FCA) and an interval (intent in FCA) corresponding to the intersection (i.e. the meet in FCA) of all intervals given by sources. The top node (⊤) in the lattice corresponds to all sources and the bottom node (⊥)t on o source at all.

The lattice gives a meaningful map of the available information and the fusion results. Each node contains a maximal subset of sources and the information fusion result it supplies. Moreover, the lattice provides a structured view of global and partial conjunctive fusion results. Actually, a pair (A, d) of (G, (D m1 , ∩),δ), is interesting from many points of view, as illustrated with the node labelled ({g 1 ,g 2 }, [START_REF] Dubois | Possibility theory and data fusion in poorly informed environments[END_REF][START_REF] Ganter | Formal cConcept Analysis[END_REF]). Moreover, when the global fusion result is conflicting hence not useful (for example, in the conjunctive fusion lattice, the global fusion result is the empty set), the lattice allows users to choose several subsets of sources with their fusion results that are the more useful and the corresponding non-empty intervals. Then, it is interesting to observe subsets of sources given in the lattice and their partial fusion results.

Note that the disjunctive fusion operator allows to build another lattice since it is commutative, associative and idempotent.

Besides, information sources give information about several variables. Then, we must compute one information fusion lattice for each variable. In the pattern structure formalism [START_REF] Kaytoue | Mining gene expression data with pattern structures in formal concept analysis[END_REF], when the description of objects is representing by a vector of object descriptions for each variable, we consider a meet operator for each attribute. Then, we consider that information fusion sources describe variables using a multi-dimentional vector. Each dimension corresponds to a variable. Consequently, we use a fusion operator for each dimension in the source description. This method allows us to obtain the fusion result for several variables simultaneously.

B. Lattice of MCS results

The MCS fusion operator cannot be used as a meet operator since it is not associative. For instance, going back to Table II and f 1 represents the MCS fusion operator, f 1 ((g 1 ,g 2 ),g 3 )=[ 2 , 3] ∪ [START_REF] Dubois | Dealing with multi-source information in possibilistic logic[END_REF][START_REF] Destercke | Possibilistic information fusion using maximal coherent subsets[END_REF] and f 1 ((g 1 ,g 3 ),g 2 )= [2, 3] ∪ [START_REF] Dubois | Dealing with multi-source information in possibilistic logic[END_REF][START_REF] Ganter | Pattern Structures and Their Projections[END_REF]. Then, we cannot directly build the MCS fusion results lattice. However, the MCS fusion operator returns the disjunction of maximal consistent conjunctions. Consequently, we can use the disjunctive operator, on the conjunctions obtained from initial information, as a meet operator to build the lattice of MCS information fusion results. Then, we use a pre-processing method, detailed in [START_REF] Assaghir | Managing information fusion with formal concept analysis[END_REF], that consists in computing maximal consistent subsets of sources (i.e. MCS) with the associated conjunction of intervals; then we apply a disjunctive operator (viewed as a meet operator) on these MCSs and derive another meetsemi-lattice (D m , ∪).

Then, consider the set K of subsets of sources providing the MCS values and let D m represent the information fusion space of the parameter m. Consequently, (K, (D, ∪),δ) is a pattern structure and we can build another lattice.

Going back to Table II the fusion result must be convex, and the convex hull of MCS fusion results is imprecise. Therefore, using a subset of sources, i.e. a partial fusion result is more useful and the fusion result is more precise. Hence, the lattice of MCS results organizes the groups of sources with their merged results. Each node corresponds to a subset of sources with their MCS result. On Figure 3, let us consider the node labelled ({(g 1 ,g 3 ), (g 3 ,g 4 )}, (m 1 , [4, 5] ∪ [START_REF] Dubois | Multiple source information fusion: a practical inconsistency tolerant approach[END_REF][START_REF] Destercke | Possibilistic information fusion using maximal coherent subsets[END_REF])). The value [START_REF] Dubois | Dealing with multi-source information in possibilistic logic[END_REF][START_REF] Ganter | Pattern Structures and Their Projections[END_REF]∪ [START_REF] Dubois | Multiple source information fusion: a practical inconsistency tolerant approach[END_REF][START_REF] Destercke | Possibilistic information fusion using maximal coherent subsets[END_REF], of the variable m 1 , is coming from K 1 and K 2 . Moreover, these values represent the MCS fusion result of the subset {g 1 ,g 3 ,g 4 }. The top node ⊤ corresponds to the union of all MCS of sources that is the MCS fusion result of all sources.

, K = {K 1 ,K 2 ,K 3 } where K 1 = {g 1 ,g 3 }, K 2 = {g 3 ,g 4 } and K 3 = {g 1 ,g 2 } for m 1 .
Besides, if the information sources provide globally consistent information, then the conjunction of all items is not empty. In that case, the lattice of MCS results reduces to a unique node (this corresponds to the intersection of all source items since they are consistent). However, if the information sources are pairwise conflicting, then each concept of the conjunctive fusion lattice contains a single source and the pieces of information it provides, the ⊤ and the ⊥ nodes. More generally, if sources are conflicting, the global conjunctive fusion result is empty. Then, nodes located just below the ⊤ (called co-atom concepts) in the conjunctive fusion results lattice, form nodes of the MCS fusion results lattice (called atom concepts). Instead of the pre-processing method for the MCS results lattice, we can build the lattice of conjunctive results. Then, it consists in deleting the ⊤ and performing unions to obtain MCS results. Note the obtained structure is based on both intersection and union semi-lattices, but it is not a lattice structure.

IV. CONCEPT LATTICE AS LATTICE OF ARGUMENTS

The concept lattice gives a classification of sources and information provided by sources. Maximal fusion results are organized in the lattice. When the global fusion result corresponding to the fusion of all sources is empty or imprecise, the lattice allows us to consider partial fusion results that correspond to subsets of sources. Then, the lattice forms a hierarchy of arguments or answers for an evaluation process. Instead of the global fusion each subset of sources with their fusion results in the lattice can be used in the evaluation process. Each node in the lattice provides a decision for the user. Then, the lattice is the basis for answering queries or displaying arguments for several decisions. Each pair containing a subset of sources with their fusion result leads to a possible decision. Hence, the lattice can be called lattice of answers or lattice of arguments.

Formally, let us consider S = {g 1 ,...,g k },k ≤ n a subset of sources in G and f m (S) is the fusion result of information provided by sources in S w.r.t. a fusion operator f m for the parameter m. Then, the pair (S, f m (S)) is called an argument or an answer. Hence, the concept lattice is said to be a lattice of arguments or a lattice of answers if and only if the subset S is maximal with respect to f m (S), i.e. for any S 0 such that f m (S 0 )=f m (S),w eh a v eS 0 ⊆ S. Thus, the information f m (S) is associated with a maximal subset of sources that support it.

Instead of providing a unique fusion result, the lattice of arguments gives a structured view of optimal partial fusion results labelled by subsets of sources. This allows us to choose among these subsets of sources and argue about the most appropriate evaluation using the reliability of sources. In the next section, we will detail how the reliability of sources can be taken into account to provide a synthetic conclusion in the evaluation process.

V. TAKING INTO ACCOUNT THE SOURCE RELIABILITY

The reliability of a source represents its capability to provide a correct piece of information for a given problem. There are two approaches to modeling such reliability:

• One may define a reliability complete pre-ordering describing whether one source is more reliable than another or not. • One is capable to determine a numerical reliability factor or certainty degree for each source, denoted by α ∈ [0, 1]. We can let α =1to denote that the source is fully reliable and α =0when the source is totally unreliable (in the sense of useless: the information provided by the corresponding source is not taken into account in the evaluation process). Reliability can be context-dependent. For example, even if some source is more reliable than others regarding a parameter, these other sources maybe more worthy of trust than the former for another parameter. The question is how to use reliability information in the lattice of arguments and more generally, how to combine information from n sources taking into account the reliability of the sources in order to provide a synthetic conclusion for the user. For a set of n sources, let α j > 0 be the reliability degree of source g j for a parameter m. When all sources are reliable, the conjunctive fusion operator is used to combine pieces of information and the global evaluation is considered.

In a quantitative uncertainty setting, Shafer's evidence theory [START_REF] Shafer | A Mathematical Theory of Evidence[END_REF] provides a way for discounting the information supplied by unreliable sources. The degree of reliability α is interpreted as the probability that the information d provided by a source is relevant and correct. In other words, the degree 1-α is the probability that the information is useless. A pair (d, α) formed by an interval d and a reliability degree α is then interpreted as a consonant belief function defined by a mass function mass(d)=α and mass(DOM)=1-α where DOM is the attribute domain. It is equivalent to replace d by a possibility distribution on DOM, such that π(x)=1if x ∈ d and 1α otherwise.

As the application of FCA requires idempotent operations we shall use minimum and maximum to combine such possibility distributions. The combination using the minimum is in agreement with a logical point of view on the information fusion problem. One can generalize the MCS method to the handling of reliability weights attached to sources for each argument in the lattice of arguments. Suppose one source is characterized by (d 1 ,α 1 ) and another one by (d 2 ,α 2 ). Combining the two possibility distributions by the minimum, and assuming d 1 ∩ d 2 is a non-empty interval, one easily deduces that necessity degrees of d 1 ∩ d 2 and d 1 ∪ d 2 are respectively min(α 1 ,α 2 ) and max(α 1 ,α 2 ). However, if there are conflicts between sources, the conjunction of possibility distributions is not sufficient.

One idea is then to use qualitative counterparts [START_REF] Prade | Possibilistic evidence[END_REF] of combination rules existing in evidence theory setting. Define a qualitative mass function µ on 2 DOM associated with the pair (d, α) as µ(d)=α and µ(DOM)=1. The corresponding necessity measure is defined by N (d 1 )=max e⊑d1 µ(e). The conjunctive rule assigns the mass min(α 1 ,α 2 ) to d 1 ∩ d 2 = ∅ (and 0 otherwise), α 1 to d 1 , α 2 to d 2 , and 1 to DOM. When there is no conflict, the result is still a possibility distribution, due to the use of min operation, since assuming α 1 ≤ α 2 , min(α 1 ,α 2 )=α 1 , and (d 1 ∩ d 2 ,α 1 ) subsumes (d 1 ,α 1 ), thus preserving the nestedness of focal elements. In case of conflict, the result is no longer expressed by a possibility distribution (since the focal elements d 1 and d 2 are then disjoint). The disjunctive rule works similarly: it assigns the mass min(α 1 ,α 2 ) to d 1 ∪ d 2 ,a n d1t oDOM. These rules easily generalize to any number of sources. Then, if K 1 ,K 2 , ..., K k are the maximal consistent subsets of sources supporting a result d (a disjunction of intervals), then the reliability of the result can be computed by applying these rules.

This calculation can help the user select a proper subset of sources bringing information that is as useful and reliable as possible.

VI. A REAL-WORLD APPLICATION IN AGRONOMY

Agronomists compute indicators for evaluating the impact of agricultural practices on the environment. Questions such as the following are of importance: what are the consequences of the application of a pesticide given its properties, the period of application, and the characteristic features of the field? The risk level for a pesticide to reach surface water is measured by the indicator I sur in [START_REF] Van Der Werf | An indicator of pesticide environmental impact based on a fuzzy expert system[END_REF]. Agronomists try to make a diagnosis based on the value of I sur . Pesticide features depend on the chemical properties of the product while pesticide period application and field properties depend on domain knowledge [START_REF] Bockstaller | Use of agro-ecological indicators for the evaluation of farming systems[END_REF]. This knowledge lies in information sources among which books, databases, and expert knowledge in agronomy. Then values for some features vary w.r.t. sources.

Here, we are interested in the use of pesticide metsulfuronmethyle and its influence on the surface water. Two characteristic features of Metsulfuron-methyle are needed to compute the indicator I sur , namely DT 50 and aquatox (aqu) (more details on these parameters can be found in [START_REF] Van Der Werf | An indicator of pesticide environmental impact based on a fuzzy expert system[END_REF]; they are not crucial for the understanding of this paper).

Table IV FEATURES OF Metsulfuron Methyle

their certainty degrees for each characteristic. The symbol "?" represents the case when the information source does not give data for the parameter. For this case, the certainty degree is unknown and it will not be taken into account in the computation of the reliability. Agronomists look to find a suitable value for each parameter to be considered for computing the I sur indicator, hence facing an information fusion problem.

Lattice construction. The parameters DT 50 and aqu are independent. No information is available about sources. Then, the appropriate fusion is the method based on the MCS fusion operator. Therefore, 2 We use the convex hull of the fusion results for computing Isur are smaller than 7 and other ones are greater than 7. Then, using the set of all sources cannot help agronomists to evaluate the agricultural practices. This due to the diversity of sources and the conflict between sources. Then, it is useful to observe partial fusion results given by the lattice.

For example, considering C 1 (see Figure 4), DT 50 = [27, 34] and aqu =0 .01, then I sur =[ 6 .9, 7]. This indicates that the farmer must change its practices, since values of I sur are smaller than 7. Then, considering the subset {PM10,PM11,ARSl,ARSf,Com98,RIVM,BUK, AGXf, AGXl} for DT 50 and Com96 for aqu, using of metsulfuron methyle is risky for the environment. However, considering DT 50 = [27, 34] and aqu =0 .045,t h e resulting interval of I sur is [7, 7.4] indicating that the practices of the farmer are environment-friendly since the I sur values are greater than 7.

Taking into account the reliability. Consider now that the user knows that some sources are more reliable than others regarding both of parameters DT 50 and aqu. Each information source is given with a degree of certainty for each parameter (see Table IV). Using the conjunctive combination rule described in section V, we can attach reliability weights to each MCS K i as shown on figure 4.

Then it is possible to compute reliability weights for other arguments in the lattice. For instance C 1 merges information about DT 50 and aqu and has reliability min(0.4, 0.6). Likewise the argument merging K 1 and K 4 has reliability min(0.2, 0.6). This computation can help users to identify sources and subset of sources bringing information that is as reliable and useful as possible. Instead of computing a weight for each obtained value of the indicator, handling reliability in the combination of sources using a lattice of arguments allows to rank fusion results for each parameter w.r.t. their usefulness in the agricultural context.

VII. RELATED WORKS AND CONCLUDING REMARKS

The method presented here for handling the reliability of sources is similar to the method proposed by Dubois et al. [START_REF] Dubois | Dealing with multi-source information in possibilistic logic[END_REF] in a logical framework. In this work, authors propose to associate each piece of information not only with its certainty level (as in standard possibilistic logic), but also with the sources which provide it, thus capturing the idea of source-based argument like in our methodology. In this work, each conclusion that can be deduced from such a knowledge base is associated with the subset of sources that supports this conclusion, where each source is itself associated with a certainty level. This approach handles conflicts, by allowing mutually exclusive conclusions supported by distinct subsets of sources. However, conclusions are not merged, as done here with numerical interval values, taking advantage of formal concept analysis for structuring the merging results. Similarly, the work presented here may be also somewhat related with another extension of possibilistic logic called "logic of supporters" [START_REF] Lafage | A logic of supporters[END_REF], where logical formulas are associated with a set of supporters organized in a lattice structure, but this proposal does not deal with information fusion.

In this paper, we propose a method to combine information using formal concept analysis, more particularly its extension for numerical data (pattern structures). This method provides a lattice of arguments. We also detail how to handle the reliability (when available) in the combination process. Instead of giving a unique fusion result, the lattice of arguments gives a structured view of partial fusion results labelled by subsets of sources. Moreover, when the reliability of sources is available, arguments are rank-ordered in order to identify the most appropriate evaluation.

Lastly, it is interesting to notice that the approach presented here in the case of imprecise numerical information represented by means of intervals, could be adapted to any types of uncertainty representations. In particular, these subsets may be the sets of models of propositional knowledge bases. Then, our approach to information fusion would fit in the setting first proposed in [START_REF] Ferré | Searching for objects and properties with logical concept analysis[END_REF], and known to be a special case of pattern structure.

Figure 1 .

 1 Figure 1. Concept lattice induced by TableI

  Then (G, (D, ⊓),δ) is called a pattern structure. Elements of D are called patterns and are ordered by a subsumption relation ⊑ such that given c, d ∈ D one has c ⊑ d ⇐⇒ c ⊓ d = c. A pattern structure (G, (D, ⊓),δ) gives rise to the following derivation operators (•) ,g i v e n A ⊆ G and d ∈ (D, ⊓): A = g∈A δ(g) d = {g ∈ G|d ⊑ δ(g)} These operators form a Galois connection between (2 G , ⊆) and (D, ⊑). (Pattern) concepts of (G, (D, ⊓),δ) are pairs of the form (A, d), A ⊆ G, d ∈ (D, ⊓), such that A = d and A = d . For a pattern concept (A, d), d is called a pattern intent and is the common description of all objects in A, called pattern extent. When partially ordered by (A 1 ,d 1 ) ≤

Figure 2 .

 2 Figure 2. Conjunctive results lattice

  Figure 3 represents the lattice of MCS results for variable m 1 . In [10],

Figure 3 .

 3 Figure 3. Lattice of MCS fusion results

  Lattice interpretation. The resulting lattice is given in Figure4with 21 values allowing to compute the indicator I sur . The lower arguments represent MCS values of each parameter. For the other arguments in the lattice, the subset of sources (resp. values) is composed of all sources (resp. values) lying in the subsets of sources (resp. values) of its sub-arguments. For

Figure 4 .

 4 Figure 4. Lattice of MCS fusion results raised from TableIV

  example, on Figure 4, the argument value of C 1 is {(DT 50, [27, 34]), (aqu, 0.01)}. But, if two sub-arguments give different values for the same attribute, then the union of values is considered. For example, the argument value of C 2 is {(DT 50, [27, 34]), (aqu, {0.045}∪{ 0.01})} and its sub-arguments values are {(DT 50, [27, 34]), (aqu, 0.01)} and {(aqu, 0.045)}. Moreover, each argument value in the lattice represents the disjunctive fusion result of the subset of sources in the argument. Consequently, these values correspond to the MCS fusion results of subsets in G. Indeed, the highest argument in the lattice corresponds to the MCS global fusion result of all sources for all parameters. Here, this result is [27, 34] ∪ [120, 120] for DT 50 and {0.045}∪{0.01}∪{100} for the variable aqu.First results. Once feature values are summarized from the delivered pieces of information, agronomists try to make a diagnosis w.r.t. the value of I sur . A value below 7 indicates that the farmer has to change its practices (pesticide, soil, date, etc.). By contrast, a value above 7 indicates that the practices of the farmer are environment-friendly[START_REF] Van Der Werf | An indicator of pesticide environmental impact based on a fuzzy expert system[END_REF].Considering the global result, i.e. DT 50 = [27, 120] and aqu =[ 0 .01, 100] then the indicator I sur =[ 3 .5, 9.7] 2 . This interval is not useful since some values in[3.5, 9.7]

  For instance ⊑ fm is the interval inclusion if fm is a conjunctive operator.

	FCA	Pattern structures	Information fusion
	objects	objects	sources
	attributes	descriptions	variables
	binary data	complex data	intervals
	meet operator	meet operator ⊓	fusion operator fm
		D description space	Dm fusion space
	(2 M , ∩)	(D, ⊓)	(Dm,fm)
	(2 M , ⊆)	(D, ⊑)	(Dm, ⊑ fm ) a
	formal concept	pattern concept	argument
	concept lattice	pattern concept lattice lattice of arguments
		Table III
	RELATED NOTIONS IN THE FIELDS OF FCA, PATTERN STRUCTURES AND
		INFORMATION FUSION

Table

III

represents some related basic notions in FCA, pattern structures and information fusion that we will detail later in this paper to show how FCA and pattern structures are well suited for merging information.

a ⊑ and ⊑ fm are respectively defined with respect to ⊓ and fm.

Table IV (

 IV simplified data) gives the values of the parameters DT 50 and aqu according to 11 different information sources, and α i and β i denote the certainty degrees of the source i regarding the parameter DT 50 and aqu respectively.

		DT 50	aqu	α a i	β a i
	BUS	120	?	0.2
	PM10	[7,35]	?	0.7
	PM11	[7,35]	100	0.7	0.9
	Com96	[14,180]	0.01	0.5	0.6
	Com98	[4,71]	?	0.5
	ARSl	[14,38]	?	0.2
	ARSf	[8,105]	?	0.2
	RIVM	[27,34]	100	0.4	0.3
	BUK	[7,190]	?	0.4
	AGXf	[4,100]	0.045	0.8	0.8
	AGXl	[20,51]	0.045	0.7	0.8

a

  Table VI presents the preprocessing table obtained from initial information provided by sources in Table IV. Table V gives subsets of sources producing the MCS of values for each parameter.

	K1 {BUS, Com96,BUK}
	K2 {PM10,PM11,ARSl,ARSf,Com98,RIVM,BUK,AGXf,AGXl}
	K3 {PM11,RIVM}
	K4 {Com96}
	K5 {AGXf, AGXl}
		Table V
	LABEL OF ALL MCS
		DT 50	aqu
	K1	120	∅
	K2	[27, 34]	∅
	K3	∅	0.045
	K4	∅	0.01
	K5	∅	100
		Table VI
	TABLE IV PRE-PROCESSED

1082-3409/11 $26.00 © 2011 IEEE DOI 10.1109/ICTAI.2011.98