CAISL: Simplification Logic for Conditional Attribute Implications

CAISL: Simplification Logic for Conditional Attribute Implications Estrella Rodr´ıguez-Lorenzo1, Pablo Cordero1, Manuel Enciso1, Rokia Missaoui2, ´ Angel Mora1 1Universidad de M´alaga, Andaluc´ıa Tech, Spain, e-mail: {estrellarodlor,amora}@ctima.uma.es, {pcordero,enciso}@uma.es 2Universit´e du Qu´ebec en Outaouais, Canada, e-mail: {rokia.missaoui}@uqo.ca Abstract. In this work, we present a sound and complete axiomatic system for conditional attribute implications (CAI s) in Triadic Concept Analysis (TCA). Our approach is strongly based on the Simplification paradigm, allowing a more suitable approach to automated reasoning than those based on Armstrong’s Axioms. We also present an automated method to prove the derivability of a CAI from a set of CAI s. 1 Introduction Implications in FCA represent associations between two attribute sets, denoted by X→Y, and capture an important knowledge hidden in the input data. They also allow an alternate representation of the concept lattice and open the door to their automated management through logic. Such a management is used, for instance, to characterize representations of the whole knowledge by means of the notion of implicational systems. There exist different axiomatic systems in FCA, the first one is called Armstrong’s Axioms [1], but later, other equivalent logics emerged [4, 5, 9]. The first study on triadic implications has been investigated by Biedermann [2] and then an extended work has been poposed by Ganter and Obiedkov [6]. In addition to a formal definition of implications and their language, we believe that the introduction of a sound and complete inference system is needed to reason about such implications and determine whether a given implication can be derived from an implication basis. Soundness ensures that implications derived by using the axiomatic system are valid in the formal context and completeness guarantees that all valid implications can be derived from the implicational system. As far as we know, there does not exist an axiomatic system in Triadic Concept Analysis. The main goal of this paper is then to define a new axiomatic system based on Simplification Logic [4] as an alternate view of the inference system recently developed by the authors [12]. This new way also allows an efficient automated reasoning, commonly called the implication problem, to determine if a conditional attribute implication (CAI ) can be derived from a set of CAI s. Given a set of dependencies Σand a further dependency σ, the implication problem means that one would like to check whether σholds in all datasets satisfying Σ. This problem occurs in research areas such as database theory and knowledge reasoning, and its solution allows the search for associations in an interactive and exploratory way rather than an exhaustive manner. Using Armstrong’s axioms, many polynomial time algorithms for implication problem decision have been defined and the closure of an attribute set has been exploited to solve it. The remainder of this paper is organized as follows. In Section 2 we provide a background on TCA. Section 3 briefly presents a logic for conditional attribute implications called CAIL [12] while Section 4 describes a new axiomatic system called CAISL that is more suitable for solving the implication problem in the triadic framework. In Section 5 we establish equivalences derived from CAISL between sets of CAI sand show how we can syntactically transform and simplify a set of CAI s while preserving their semantics in the CAISL context. To check whether a CAI holds for a given set of CAI s, we propose and illustrate a new procedure in Section 6. Finally, Section 7 summarizes our contribution and presents further work. 2 Triadic concept analysis As a natural extension to Formal Concept Analysis (FCA), theoretical foundations of Triadic Concept Analysis have been investigated by Lehmann and Wille [8] who were inspired by the philosophical framework of Charles S. Peirce [11] of three universal categories. The input is a formal triadic context describing objects in terms of attributes that hold under given conditions and the output is a concept trilattice that allows the generation of triadic association rules, including implications [2, 6, 7, 10]. Definition 1. A triadic context K=hG, M, B, Iiconsists of three sets: a set of objects (G), a set of attributes (M) and a set of conditions (B) together with a ternary relation I⊆G×M×B. A triple (g, m, b)in Imeans that object gpossesses attribute munder condition b. Figure 1 shows a triadic context K:= hG, M, B, Ii, where G={1,2,3,4,5} is a set of customers, M={P,N,R,K,S}a set of suppliers and B={a,b,d,e} represents a set of products. The ternary relation gives information about the customers and the suppliers from whom they buy products. For instance, Customer 1 buys from Supplier P products a,b and e. KP N R K S 1 abe abe ad ab a 2 ae bde abe ae e 3 abe e ab ab a 4 abe be ab ab e 5 ae ae abe abd a Fig. 1. A triadic context The derivation operators in triadic concept analysis were introduced in [8]. If X1,X2and X3are subsets of G,Mand Brespectively, then one can get: X0 1={(aj, ak)∈M×B|(ai, aj, ak)∈Ifor all ai∈X1}. (X2, X3)0={ai∈G|(ai, aj, ak)∈Ifor all (aj, ak)∈X2×X3}. In a similar way, X0 2, (X1, X3)0,X0 3and (X1, X2)0can be defined. As shown in [13], the above family of operators, by setting a subset of objects, attributes or conditions (respectively) yields Galois connections. In this paper, we use the family of Galois connections associated with condition subsets. That is, given C ⊆ Bwe consider the Galois connection between the lattices (2M,⊆) and (2G,⊆) as the pair of mappings: (−,C)0: 2G−→ 2M(−,C)0: 2M−→ 2G X17−→ (X1,C)0X27−→ (X2,C)0 Thus, for each X1⊆Gand X2⊆M, one has X2⊆(X1,C)0if and only if X1⊆(X2,C)0. In a similar way as in dyadic FCA, the composition of both derivation operators leads to the notion of triadic concept. Definition 2. A triadic concept of a triadic context is a triple (A1, A2, A3)with A1⊆G,A2⊆M,A3⊆Band A1×A2×A3⊆Isuch that for X1⊆G, X2⊆M, and X3⊆Bwith X1×X2×X3⊆I, the containments A1⊆X1, A2⊆X2,and A3⊆X3always lead to (A1, A2, A3)=(X1, X2, X3). The subsets A1,A2and A3 are called the extent, the intent and the modus of the triadic concept (A1, A2, A3) respectively. There are a few kinds of triadic implications with different semantics. Biedermann [3] defines a triadic implication to be an expression of the form: (A→B)C where Aand Bare attribute sets and Cis a set of conditions. This implication is interpreted as: If an object has all attributes from Aunder all conditions from C, then it also has all attributes from Bunder all conditions from C. Its formal definition is the following: Definition 3. Let K=hG, M, B, Iibe a triadic context, A, B ⊆Mand C ⊆ B. The implication (X→Y)Cholds in the context Kiff (X, C)0⊆(Y, C)0. Ganter and Obiedkov [6] consider three kinds of triadic implications. We will describe and make use of the following one which is stronger than Biedermann’s expression and has another notation: XC −→ Y, where X, Y ⊆Mand C ⊆ B. Such implication is called conditional attribute implication (CAI ) and is read as “X implies Yunder all conditions in Cor any subset of it”. Definition 4 (Conditional attribute implication). Let K=hG, M, B, Iibe a triadic context, X, Y ⊆Mand C ⊆ B. The implication XC −→ Yholds in the context Kwhen (X, {c})0⊆(Y, {c})0for all c∈ C. Notice that CAI s preserve the dyadic implications that hold for each elementary condition in C. The following proposition relates both notions of implications and also shows that Biedermann’s definition is weaker than the CAI definition. Proposition 1 ([6]). Let K=hG, M, B, Iibe a triadic context, X, Y ⊆Mand C ⊆ B. Then XC −→ Yholds in Kiff (X→Y)Nalso holds in Kfor all N ⊆ C. The following example illustrates the above proposition. Example 1. Let Kbe the triadic formal context given in Figure 1. i) The CAI Nae −→ Pholds in Ksince the following implications are satisfied: (N→P)a,(N→P)e,(N→P)ae. ii) The Biedermann’s implication (N→P)abe is satisfied but the CAI Nabe −−→ P does not hold because, for instance, (N→P)bis not satisfied. Our objective in this paper is to provide inference mechanisms for a set of CAI s. To that end, a sound and complete axiomatic system is needed. As mentioned earlier, we have introduced in [12] a novel logic for computing CAI s and reasoning about them. This logic is briefly presented in the following section. 3 CAIL: Conditional Attribute Implication Logic In this section, we describe CAIL, a logic for reasoning about CAI s in the framework of TCA [12]. This logic is presented in a classical style by considering three pillars: the language, the semantics and the inference system. Language: As it has been outlined, we use the following language: given an attribute set Ωand a set of conditions Γ, the set of well-formed formulas (hereinafter, formulas or implications) is LΩ,Γ ={AC −→ B|A, B ⊆Ω, C ⊆ Γ}. In the sequel we use X, Y, Z, W to mean subsets of attributes (X, Y, Z, W ⊆Ω) and C,C1,C2for subsets of conditions (C,C1,C2⊆Γ). For the sake of readability of formulas, we omit the brackets and commas (e.g. abc denotes the set {a, b, c}) and, as usual, the union is denoted by set juxtaposition (e.g. XY denotes X∪Y). Semantics: Based on Definition 4, the semantics is introduced by means of the notions of interpretation and model. From a language LΩ,Γ , an interpretation is a triadic context K=hG, M, B, Iisuch that M=Ωand B=Γ. A model for a formula XC −→ Y∈ LΩ,Γ is an interpretation that satisfies XC −→ Yin K. In this case, we write K|=XC −→ Y. As usual, for Σ⊆ LΩ,Γ , an interpretation Kis a model for Σ(briefly, K|=Σ) if K|=XC −→ Yfor each XC −→ Y∈Σ. Similarly, Σ|=XC −→ Ystates that XC −→ Y is a semantic consequence of Σ, i.e. every model for Σis also a model for XC −→ Y. Syntactic inference: The syntactic derivation in CAIL is denoted by the symbol `Cand covers two axiom schemes and four inference rules. Definition 5. The CAIL axiomatic system consists of the following rules: [Non-constraint] `C∅∅ −→ Ω. [Inclusion] `CXY Γ −→ X. [Augmentation] XC −→ Y`CXZ C −→ Y Z. [Transitivity] {XC1 −→ Y, Y C2 −→ Z} `CXC1∩C2 −−−−→ Z. [Conditional Decomposition] XC1C2 −−−→ Y`CXC1 −→ Y. [Conditional Composition] {XC1 −→ Y, Z C2 −→ W} `CXZ C1C2 −−−→ Y∩W. The derivation notion is introduced as usual: For a given set Σ⊆ LΩ,Γ and ϕ∈ LΩ,Γ , we state that ϕis derived (or inferred) from Σby using the CAIL axiomatic system, denoted by Σ`Cϕ, if there exists a chain of formulas ϕ1, . . . , ϕn∈ LΩ,Γ such that ϕn=ϕand, for all 1 ≤i≤n,ϕiis either an axiom, an implication in Σ or is obtained by applying the CAIL inference rules to formulas in {ϕj|1≤j < i}. Soundness and completeness: In [12], we prove that every model of Σis a model of XC −→ Yiff such implication can be derived syntactically from Σusing the CAIL axiomatic system, i.e. Σ|=XC −→ Yif and only if Σ`CXC −→ Y 4 CAISL: Simplification Logic for CAI s Once the preliminary results have been introduced, we now present a new axiomatic system which is more suitable for automated reasoning. We will use the same language and semantics provided in the previous section but give a novel equivalent axiomatic system based on simplification paradigm [4]. For this axiomatic system, the symbol `Sdenotes the syntactic derivation. Definition 6. The CAISL axiomatic system has two axiom schemes: [Non-constraint] `S∅∅ −→ Ω. [Reflexivity] `SXΓ −→ X. and four inference rules: [Decomposition] {XC1C2 −−−→ Y Z} `SXC1 −→ Y. [Composition] {XC1 −→ Y, Z C2 −→ W} `SXZ C1∩C2 −−−−→ Y W. [Conditional Composition] {XC1 −→ Y, Z C2 −→ W} `SXZ C1C2 −−−→ Y∩W. [Simplification] If X∩Y=∅, {XC1 −→ Y, XZ C2 −→ W} `SXZrYC1∩C2 −−−−→ WrY. The two axiom schemes in CAISL have the following interpretations respectively: (1) all attributes hold for all objects under a void condition, and (2) X always implies itself under all conditions. The key statement is that both axiomatic systems are equivalent as the following theorem proves. However, as we will show below, CAISL is more appropriate for developing automated methods to reason about implications. Theorem 1 (Equivalence between CAIL and CAISL). For any Σ⊆ LΩ,Γ and XC −→ Y∈ LΩ,Γ , one has Σ`SXC −→ Yif and only if Σ`CXC −→ Y Proof. To prove the equivalence between both logics, we will show that the inference rules of CAISL can be derived from those in CAIL and vice versa. i) Inference rules derived from CAIL [Reflexivity]: 1. XΓ −→ X. . . . . . . . . . . . . Inclusion. [Decomposition]: 1. XC1C2 −−−→ Y Z . . . . . . .Hypothesis. 2. Y Z Γ −→ Y. . . . . . . . . . . Inclusion. 3. XC1C2 −−−→ Y..........1,2 Trans. 4. XC1 −→ Y. . . . .3 Cond. Decomp. [Composition]: 1. XC1 −→ Y. . . . . . . . . . Hypothesis. 2. ZC2 −→ W. . . . . . . . . . Hypothesis. 3. XZ C1 −→ Y Z . . . . . . . . . . .1 Augm. 4. Y Z C2 −→ Y W . . . . . . . . . . 2 Augm. 5. XZ C1∩C2 −−−−→ Y W . . . . . 3,4 Trans. [Simplification]: 1. XC1 −→ Y. . . . . . . . . . Hypothesis. 2. XZ C2 −→ W. . . . . . . . Hypothesis. 3. XZrYΓ −→ X. . . . . . . Inclusion. 4. WΓ −→ WrY. . . . . . . . Inclusion. 5. XZ C2 −→ WrY. . . . . 2,4 Trans. 6. XZrYC1 −→ Y......3,1 Trans. 7. XZrYC1 −→ XY Z . . . . 6 Augm. 8. XY Z C2 −→ W Y . . . . . . . 5 Augm. 9. XZrYC1∩C2 −−−−→ W Y 7,8 Trans. 10. XZ rYC1∩C2 −−−−→ WrY. 9 Decomp. ii) Inference rules derived from CAISL [Inclusion]: 1. XY Γ −→ XY . . . . . . . Reflexivity. 2. XY Γ −→ Y. . . . . . . . . . 1 Decomp. [Augmentation]: 1. XC −→ Y. . . . . . . . . . . Hypothesis. 2. ZΓ −→ Z. . . . . . . . . . . . .Reflexivity. 3. XZ C −→ Y Z .........1,2 Comp. [Transitivity]: 1. XC1 −→ Y. . . . . . . . . . . Hypothesis. 2. YC2 −→ Z. . . . . . . . . . . Hypothesis. 3. XC1 −→ YrX. . . . . . . 1 Decomp. 4. YC2 −→ ZrY. . . . . . . . .2 Decomp. 5. XΓ −→ X. . . . . . . . . . . . Reflexivity. 6. XΓ −→ ∅ . . . . . . . . . . . . . 5 Decomp. 7. XY C2 −→ ZrY......4,6 Comp. 8. YrXΓ −→ YrX. . . .Reflexivity. 9. XC1∩C2 −−−−→ ZrY. . . . . 3,7 Simp. 10. XC1∩C2 −−−−→ Y Z ......1,9 Comp. 11. XC1∩C2 −−−−→ Z. . . . . . . 10 Decomp. ut Since the two axiomatic systems are equivalent, in the sequel we will omit the subscript in the syntactic derivation symbol using simply `. 5 CAISL Equivalences In this section, we introduce several results which constitute the basis of the automated reasoning method that will be introduced in the next section. These results illustrate how we can use CAISL as a framework to syntactically transform and simplify a set of CAI s while entirely preserving their semantics. This is the common feature of the family of Simplification Logics. The notion of equivalence is introduced as usual: two sets of CAI s, Σ1and Σ2, are equivalent, denoted by Σ1≡Σ2, when their models are the same. Equivalently, Σ1≡Σ2iff Σ1`ϕfor all ϕ∈Σ2, and Σ2`ϕfor all ϕ∈Σ1. Lemma 1. The following equivalences hold: {XC1 −→ Y, X C2 −→ W}≡{XC1∩C2 −−−−→ Y W, X C1 rC2 −−−→ Y, X C2 rC1 −−−→ W}(1) {XC1 −→ Y, XV C2 −→ W}≡{XC1 −→ Y, XV C2 rC1 −−−→ W, X(VrY)C1∩C2 −−−−→ WrY}(2) Proof. For Equivalence (1), first, we prove that XC1∩C2 −−−−→ Y W,XC1 rC2 −−−→ Y, and XC2 rC1 −−−→ Wcan be inferred from {XC1 −→ Y, X C2 −→ W}: –By applying Composition to XC1 −→ Yand XC2 −→ W, we get XC1∩C2 −−−−→ Y W. –XC1 rC2 −−−→ Yand XC2 rC1 −−−→ Ware obtained by Decomposition. On the other hand, we prove that XC1 −→ Yand XC2 −→ Wcan be inferred from {XC1∩C2 −−−−→ Y W, X C1 rC2 −−−→ Y, X C2 rC1 −−−→ W}by applying Conditional Composition. For Equivalence (2), from {XC1 −→ Y, XV C2 −→ W}, we infer XV C2 rC1 −−−→ Wby applying Decomposition to VC2 −→ W. In addition, we infer XV rYC1∩C2 −−−−→ WrY by applying Simplification to XC1 −→ Yand XV C2 −→ W. Finally, {XC1 −→ Y, XV C2 rC1 −−−→ W, XV rYC1∩C2 −−−−→ WrY} ` XV C2 −→ Wis proved. By applying Reflexivity and Decomposition, we get XV C1∩C2 −−−−→ XV rY and, by Transitivity with XV rYC1∩C2 −−−−→ WrY, one has XV C1∩C2 −−−−→ WrY. Now, by applying Composition to XC1 −→ Yand XV C1∩C2 −−−−→ WrY, we infer XV C1∩C2 −−−−→ WY and, by Decomposition, XV C1∩C2 −−−−→ W. At last, by applying Conditional Composition to XV C1∩C2 −−−−→ Wand XV C2 rC1 −−−→ W, we obtain XV C2 −→ W.ut The following theorem highlights a common characteristic of Simplification Logics, which shows that inference rules can be read as equivalences that allow redundancy removal. Theorem 2. The following equivalences hold: Axiom Eq.: {X∅ −→ Y}≡{XC −→ ∅} ≡ ∅ Decomposition Eq.: {XC −→ Y}≡{XC −→ YrX} Composition Eq.: {XC −→ Y, X C −→ W}≡{XC −→ Y W} Conditional Composition Eq.: {XC1 −→ Y, X C2 −→ Y} ≡ {XC1C2 −−−→ Y} Simplification Eq.: If X∩Y=∅, then {XC1C2 −−−→ Y, XV C2 −→ W}≡{XC1C2 −−−→ Y, XV rYC2 −→ WrY} Proof. The first equivalence is straightforward because both implications are axioms. For the rest of equivalences, the left to right inference is directly obtained by applying the homonymous inference rule. Thus, we prove the right to left inference: i) XC −→ XY is inferred by Composition of XC −→ YrXand XC −→ Xobtained by reflexivity. Then, by applying Decomposition, one has XC −→ Y. ii) XC −→ Yand XC −→ Ware inferred by applying Decomposition to XC −→ Y W. iii) XC1 −→ Yand XC2 −→ Yare inferred from XC1C2 −−−→ Yby applying Decomposition. iv) It is a consequence of Axiom Equivalence and Equivalence (2) in Lemma 1. ut This section has been devoted to equivalences in CAISL of a CAI s set in order to remove redundancy or, dually, to extend the set. The effect depends on the direction we apply the equivalence. In next section, we are going to use other equivalences where the empty set plays a main role. The Deduction Theorem presented below gives to the empty set such a role. This theorem establishes the necessary and sufficient condition to ensure the derivability of a CAI from a set of CAI s. 6 Automated reasoning This section shows the merits of CAISL for the development of automated methods. Specifically, we present a method that checks whether a CAI is derived from a set of CAI s. The next theorem is the core of our approach in the design of the automated prover. Theorem 3 (Deduction). For any Σ⊆ LΩ,Γ and XC −→ Y∈ LΩ,Γ , one has Σ`XC −→ Yif and only if Σ∪ {∅ C −→ X}`∅ C −→ Y Proof. Straightforwardly, we have Σ`XC −→ Yimplies Σ∪ {∅ C −→ X} ` ∅ C −→ Y. Conversely, assuming Σ∪ {∅ C −→ X}`∅ C −→ Y, we have to prove that K|=Σ implies K|=XC −→ Yfor each model K. Consider K=hG, M, B, Iias a model of Σ. In order to prove (X, {c})0⊆ (Y, {c})0for all c∈Cin K, we build the context K1=hG1, M, B, I1iwhere G1= (X, {c})0and I1=I∩(G1×M×B). Since K|=Σ, we have K1|=Σ∪ {∅ {c} −−→ X}and therefore, by hypothesis, K1|={∅ {c} −−→ Y}. That is, (Y, {c})0⊇(∅,{c})0=G1= (X, {c})0. If we go back to the original triadic context K, (X, {c})0remains unchanged whereas (Y, {c})0could grow up. Therefore, in K, one has (X, {c})0⊆(Y, {c})0for all c∈C.ut Function CAISL-Prover(Σ,XC −→ Y) input : A set of implications Σ, and a CAI XC −→ Y output: A boolean answer begin ∆X:= X× C ∆Y:= (Y× C)r(X× C) repeat flag:=false foreach UC1 −→ V∈Σwith C1∩ C 6=∅do ∆C:= {c∈ C1∩ C | U× {c} ⊆ ∆X} if ∆C6=∅then . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Equivalence (4) ∆X:= ∆X∪(V×∆C) ∆Y:= ∆Yr(V×∆C) Σ:= Σr{UC1 −→ V} C1:= C1r∆C if C16=∅then Σ:= Σ∪ {UC1 −→ V} flag:=true ∆C:= {c∈ C1∩ C | V× {c} ⊆ ∆X} if ∆C6=∅then . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Equivalence (5) if ∆C=C1then Σ:= Σr{UC1 −→ V} else Σ:=(Σr{UC1 −→ V})∪ {UC1 r∆C −−−−→ V} until (∆Y=∅)or (flag=false) return the boolean value (∆Y=∅) Theorem 3 guides the design of the automated prover. To check that the formula XC −→ Yis inferred from the set Σwe apply the family of simplification equivalences iteratively - while it is possible - to the set Σ∪ {∅ C −→ X}looking for ∅C −→ Y. The following proposition revisits Theorem 2 by instantiating the particular case of having the empty premise. Proposition 2. The following equivalences hold: {∅ C1 −→ X, U C2 −→ V}≡{∅ C1 −→ X, U rXC1∩C2 −−−−→ VrX, U C2 rC1 −−−→ V}(3) {∅ C1 −→ X, U C2 −→ V}≡{∅ C1∩C2 −−−−→ XV, ∅C1 rC2 −−−→ X, U C2 rC1 −−−→ V}, when U⊆X(4) {∅ C1 −→ X, U C2 −→ V}≡{∅ C1 −→ X, U C2 rC1 −−−→ V}, when V⊆X(5) Proof. Equivalence (3) is a particular case of Equivalence (2). In particular, when U⊆X, Equivalence (4) is obtained from (3) by applying Conditional Composition