CAISL: Simplification Logic for Conditional Attribute Implications Estrella Rodrı́guez-Lorenzo1 , Pablo Cordero1 , Manuel Enciso1 , Rokia Missaoui2 , Ángel Mora1 1 Universidad de Málaga, Andalucı́a Tech, Spain, e-mail: {estrellarodlor,amora}@ctima.uma.es, {pcordero,enciso}@uma.es 2 Université du Québec 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 which offers a more suitable way for automated reasoning than the one 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 inte- ractive 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 pro- cedure 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 con- cept trilattice that allows the generation of triadic association rules, including implications [2, 6, 7, 10]. Definition 1. A triadic context K = hG, M, B, Ii consists 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 I means that object g possesses attribute m under 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 cus- tomers and the suppliers from whom they buy products. For instance, Customer 1 buys from Supplier P products a, b and e. K P 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 , X2 and X3 are subsets of G, M and B respectively, then one can get: X10 = {(aj , ak ) ∈ M ×B | (ai , aj , ak ) ∈ I for all ai ∈ X1 }. (X2 , X3 )0 = {ai ∈ G | (ai , aj , ak ) ∈ I for all (aj , ak ) ∈ X2 ×X3 }. In a similar way, X20 , (X1 , X3 )0 , X30 and (X1 , X2 )0 can 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 ⊆ B we consider the Galois connection between the lattices (2M , ⊆) and (2G , ⊆) as the pair of mappings: (−, C)0 : 2G −→ 2M (−, C)0 : 2M −→ 2G X1 7−→ (X1 , C)0 X2 7−→ (X2 , C)0 Thus, for each X1 ⊆ G and X2 ⊆ M , one has X2 ⊆ (X1 , C)0 if and only if X1 ⊆ (X2 , C)0 . In a similar way as in dyadic FCA, the composition of both derivation opera- tors 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 ⊆ B and A1 ×A2 ×A3 ⊆ I such that for X1 ⊆ G, X2 ⊆ M, and X3 ⊆ B with X1 ×X2 ×X3 ⊆ I, the containments A1 ⊆ X1 , A2 ⊆ X2 , and A3 ⊆ X3 always lead to (A1 , A2 , A3 ) = (X1 , X2 , X3 ). The subsets A1 , A2 and 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. Bieder- mann [3] defines a triadic implication to be an expression of the form: (A → B)C where A and B are attribute sets and C is a set of conditions. This implication is interpreted as: If an object has all attributes from A under all conditions from C, then it also has all attributes from B under all conditions from C. Its formal definition is the following: Definition 3. Let K = hG, M, B, Ii be a triadic context, X, Y ⊆ M and C ⊆ B. The implication (X → Y )C holds in the context K iff (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 C expression and has another notation: X − → Y, where X, Y ⊆ M and C ⊆ B. Such implication is called conditional attribute implication (CAI ) and is read as “X implies Y under all conditions in C or any subset of it”. Definition 4 (Conditional attribute implication). Let K = hG, M, B, Ii be C a triadic context, X, Y ⊆ M and C ⊆ B. The implication X − → Y holds in the 0 0 context K when (X, {c}) ⊆ (Y, {c}) for all c ∈ C. Notice that CAI s preserve the dyadic implications that hold for each elemen- tary 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, Ii be a triadic context, X, Y ⊆ M and C C ⊆ B. Then X − → Y holds in K iff (X → Y )N also holds in K for all N ⊆ C. The following example illustrates the above proposition. Example 1. Let K be the triadic formal context given in Figure 1. ae i) The CAI N −→ P holds in K since the following implications are satisfied: (N → P )a , (N → P )e , (N → P )ae . abe ii) The Biedermann’s implication (N → P )abe is satisfied but the CAI N −−→ P does not hold because, for instance, (N → P )b is 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 frame- work 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 at- tribute set Ω and a set of conditions Γ , the set of well-formed formulas (here- C inafter, formulas or implications) is LΩ,Γ = {A − → 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 , C2 for 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, Ii such that M = Ω and B = Γ . A model for a C C formula X − → Y ∈ LΩ,Γ is an interpretation that satisfies X − → Y in K. In this C case, we write K |= X − →Y. As usual, for Σ ⊆ LΩ,Γ , an interpretation K is a model for Σ (briefly, K |= Σ) C C C C if K |= X − → Y for each X − → Y ∈ Σ. Similarly, Σ |= X − → Y states that X −→Y C is a semantic consequence of Σ, i.e. every model for Σ is also a model for X − →Y. Syntactic inference: The syntactic derivation in CAIL is denoted by the symbol `C and covers two axiom schemes and four inference rules. Definition 5. The CAIL axiomatic system consists of the following rules: ∅ [Non-constraint] `C ∅ −→ Ω. Γ [Inclusion] `C XY − → X. C C [Augmentation] X − → Y `C XZ − → Y Z. C1 C2 C ∩C2 [Transitivity] {X −→ Y, Y −→ Z} `C X −−1−−→ Z. C C C [Conditional Decomposition] X −−1−→ 2 1 Y `C X −→ Y. C1 C2 C C2 [Conditional Composition] {X −→ Y, Z −→ W } `C XZ −−1−→ 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, ϕi is 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 C of X − → Y iff such implication can be derived syntactically from Σ using the CAIL axiomatic system, i.e. C C Σ |= X − →Y if and only if Σ `C X − →Y 4 CAISL: Simplification Logic for CAI s Once the preliminary results have been introduced, we now present a new ax- iomatic 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 ax- iomatic system, the symbol `S denotes the syntactic derivation. Definition 6. The CAISL axiomatic system has two axiom schemes: ∅ [Non-constraint] `S ∅ − → Ω. Γ [Reflexivity] `S X −→ X. and four inference rules: C C C [Decomposition] {X −−1−→ 2 1 Y Z} `S X −→ Y. 1 C 2 C C ∩C [Composition] {X −→ Y, Z −→ W } `S XZ −−1−−→ 2 Y W. 1 2 C C C C [Conditional Composition] {X −→ Y, Z −→ W } `S XZ −−1−→ 2 Y ∩W . [Simplification] If X ∩ Y = ∅, 1 C 2 C C ∩C {X −→ Y, XZ −→ W } `S XZ rY −−1−−→ 2 W rY. The two axiom schemes in CAISL have the following interpretations respec- tively: (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 follow- ing 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Ω,Γ C and X − → Y ∈ LΩ,Γ , one has C C Σ `S X − →Y if and only if Σ `C X − →Y Proof. To prove the equivalence between both logics, we will show that the infer- ence rules of CAISL can be derived from those in CAIL and vice versa. i) Inference rules derived from CAIL [Reflexivity]: Γ 1. X − → X . . . . . . . . . . . . . Inclusion. [Simplification]: [Decomposition]: 1C C1 C2 1. X −→ Y . . . . . . . . . . Hypothesis. 1. X −− −→ Y Z . . . . . . .Hypothesis. 2. XZ −→ C2 W . . . . . . . . Hypothesis. Γ 2. Y Z −→ Y . . . . . . . . . . . Inclusion. 3. XZ rY − Γ → X . . . . . . . Inclusion. C1 C2 3. X −− −→ Y . . . . . . . . . .1, 2 Trans. 4. W − Γ → W rY . . . . . . . . Inclusion. C1 C2 4. X −→ Y . . . . .3 Cond. Decomp. 5. XZ −→ W rY . . . . . 2, 4 Trans. C1 [Composition]: 6. XZ rY −→ Y . . . . . . 3, 1 Trans. C1 C1 1. X −→ Y . . . . . . . . . . Hypothesis. 7. XZ rY −→ XY Z . . . . 6 Augm. C2 C2 2. Z −→ W . . . . . . . . . . Hypothesis. 8. XY Z −→ W Y . . . . . . . 5 Augm. C1 C ∩C2 3. XZ −→ Y Z . . . . . . . . . . . 1 Augm. 9. XZ rY −−1−−→ W Y 7, 8 Trans. C2 C ∩C2 4. Y Z −→ Y W . . . . . . . . . . 2 Augm. 10. XZ r Y −−1−−→ W r Y . 9 De- C ∩C2 5. XZ −−1−−→ Y W . . . . . 3, 4 Trans. comp. ii) Inference rules derived from CAISL 2C [Inclusion]: 4. Y −→ Z rY . . . . . . . . .2 Decomp. Γ Γ 1. XY −→ XY . . . . . . . Reflexivity. 5. X −→ X . . . . . . . . . . . . Reflexivity. Γ Γ 2. XY −→ Y . . . . . . . . . . 1 Decomp. 6. X −→ ∅ . . . . . . . . . . . . . 5 Decomp. C2 [Augmentation]: 7. XY −→ Z rY . . . . . . 4, 6 Comp. C Γ 1. X − → Y . . . . . . . . . . . Hypothesis. 8. Y rX − → Y rX . . . .Reflexivity. Γ C ∩C2 2. Z − → Z . . . . . . . . . . . . .Reflexivity. 9. X −−1−−→ Z rY . . . . . 3, 7 Simp. C C ∩C2 3. XZ − → Y Z . . . . . . . . . 1, 2 Comp. 10. X −−1−−→ Y Z . . . . . . 1, 9 Comp. C ∩C2 [Transitivity]: 11. X −−1−−→ Z . . . . . . . 10 Decomp. C 1 1. X −→ Y . . . . . . . . . . . Hypothesis. [Conditional Decomposition]: C2 C C 1 2 2. Y −→ Z . . . . . . . . . . . Hypothesis. 1. X −− −→ Y . . . . . . . . . Hypothesis. C1 C1 3. X −→ Y rX . . . . . . . 1 Decomp. 2. X −→ Y . . . . . . . . . . . . 1 Decomp. t u 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, Σ1 and Σ2 , are equivalent, denoted by Σ1 ≡ Σ2 , when their models are the same. Equiv- alently, Σ1 ≡ Σ2 iff Σ1 ` ϕ for all ϕ ∈ Σ2 , and Σ2 ` ϕ for all ϕ ∈ Σ1 . Lemma 1. The following equivalences hold: 1 C C 2 C ∩C C rC C rC {X −→ Y, X −→ W } ≡ {X −−1−−→ 2 1 Y W, X −− 2 −→ 2 Y, X −− 1 −→ W} (1) C1 C2 C1 C2rC1 C1 ∩C2 {X −→ Y, XV −→ W } ≡ {X −→ Y, XV −−−→ W, X(V rY ) −−−−→ W rY } (2) C ∩C C rC Proof. For Equivalence (1), first, we prove that X −−1−−→ 2 1 Y W , X −− 2 −→ Y , and 2 C rC 1 1 2 C C X −− −→ W can be inferred from {X −→ Y, X −→ W }: 1 C2 C C ∩C – By applying Composition to X −→ Y and X −→ W , we get X −−1−−→ 2 Y W. C1rC2 C2rC1 – X −−−→ Y and X −−−→ W are obtained by Decomposition. 1 C 2 C On the other hand, we prove that X −→ Y and X −→ W can be inferred from C1 ∩C2 C1rC2 C2rC1 {X −−−−→ Y W, X −−−→ Y, X −−−→ W } by applying Conditional Composition. 1 C 2 C 2 1 C rC For Equivalence (2), from {X −→ Y, XV −→ W }, we infer XV −− −→ W by C 2 C ∩C applying Decomposition to XV −→ W . In addition, we infer XV rY −−1−−→2 WrY C1 C2 by applying Simplification to X −→ Y and XV −→ W. C1 C2rC1 C ∩C2 C2 Finally, {X −→ Y, XV −− −→ W, XV r Y −−1−−→ W r Y } ` XV −→ W is C ∩C proved. By applying Reflexivity and Decomposition, we get XV −−1−−→ 2 XV rY C ∩C2 C ∩C2 and, by Transitivity with XV rY −−1−−→ W rY , one has XV −−1−−→ W rY . Now, C1 C ∩C2 C ∩C2 by applying Composition to X −→ Y and XV −−1−−→ W rY , we infer XV −−1−−→ C ∩C2 W Y and, by Decomposition, XV −−1−−→ W . At last, by applying Conditional C1 ∩C2 C2rC1 C2 Composition to XV −−−−→ W and XV −−−→ W , we obtain XV −→ W. t u 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: ∅ C Axiom Eq.: {X − → Y } ≡ {X − → ∅} ≡ ∅ C C Decomposition Eq.: {X −→ Y } ≡ {X − → Y rX} C C C Composition Eq.: {X − → Y, X −→ W } ≡ {X − → Y W} 1 2 C C C C Conditional Composition Eq.: {X −→ Y, X −→ Y } ≡ {X −−1−→ 2 Y} Simplification Eq.: If X ∩ Y = ∅, then C C C C C C {X −−1−→ 2 2 Y, XV −→ W } ≡ {X −−1−→ 2 2 Y, XV rY −→ W rY } Proof. The first equivalence is straightforward because both implications are ax- ioms. 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: C C C i) X −→ XY is inferred by Composition of X − → Y rX and X − → X obtained C by reflexivity. Then, by applying Decomposition, one has X − →Y. C C C ii) X −→ Y and X − → W are inferred by applying Decomposition to X − → Y W. C 1 2 C C C iii) X −→ Y and X −→ Y are inferred from X −−1−→ 2 Y by applying Decomposi- tion. iv) It is a consequence of Axiom Equivalence and Equivalence (2) in Lemma 1. t u 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 meth- ods. 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. C Theorem 3 (Deduction). For any Σ ⊆ LΩ,Γ and X − → Y ∈ LΩ,Γ , one has C C C Σ`X− → Y if and only if Σ ∪ {∅ − → X} ` ∅ − →Y C C C Proof. Straightforwardly, we have Σ ` X −→ Y implies Σ ∪ {∅ −→ X} ` ∅ − → Y. C C Conversely, assuming Σ ∪ {∅ − → X} ` ∅ − → Y , we have to prove that K |= Σ C implies K |= X − → Y for each model K. Consider K = hG, M, B, Ii as a model of Σ. In order to prove (X, {c})0 ⊆ (Y, {c})0 for all c ∈ C in K, we build the context K1 = hG1 , M, B, I1 i where G1 = (X, {c})0 and I1 = I ∩ (G1 × M × B). {c} Since K |= Σ, we have K1 |= Σ ∪ {∅ −−→ X} and therefore, by hypothesis, {c} K1 |= {∅ −−→ Y }. That is, (Y, {c})0 ⊇ (∅, {c})0 = G1 = (X, {c})0 . If we go back to the original triadic context K, (X, {c})0 remains unchanged whereas (Y, {c})0 could grow up. Therefore, in K, one has (X, {c})0 ⊆ (Y, {c})0 for all c ∈ C. t u C Function CAISL-Prover(Σ,X − →Y) C input : A set of implications Σ, and a CAI X − →Y output: A boolean answer begin ∆X := X × C ∆Y := (Y × C)r(X × C) repeat flag:=false 1 C foreach U −→ V ∈ Σ with C1 ∩ C =6 ∅ do ∆C := {c ∈ C1 ∩ C | U × {c} ⊆ ∆X } if ∆C 6= ∅ then . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Equivalence (4) ∆X := ∆X ∪ (V × ∆C ) ∆Y := ∆Y r(V × ∆C ) 1 C Σ := Σ r{U −→ V} C1 := C1 r∆C 1 C if C1 6= ∅ then Σ := Σ ∪ {U −→ V} flag:=true ∆C := {c ∈ C1 ∩ C | V × {c} ⊆ ∆X } if ∆C 6= ∅ then . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Equivalence (5) 1 C if ∆C = C1 then Σ := Σ r{U −→ V} 1 C C1r∆ else Σ :=(Σ r{U −→ V }) ∪ {U −−−−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 C formula X − → Y is inferred from the set Σ we apply the family of simplification C equivalences iteratively - while it is possible - to the set Σ ∪ {∅ − → 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: C 1 2 C 1 C C ∩C C rC {∅ −→ X, U −→ V } ≡ {∅ −→ X, U rX −−1−−→ 2 2 V rX, U −− 1 −→ V} (3) C 1 2 C C ∩C C rC C rC {∅ −→ X, U −→ V } ≡ {∅ −−1−−→ 2 1 XV, ∅ −− 2 −→ 2 X, U −− 1 −→ V }, when U ⊆ X (4) C 1 2 C 1 2 C 1 C rC {∅ −→ X, U −→ V } ≡ {∅ −→ X, U −− −→ 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 and Composition equivalences: C1 2 C 1 C C ∩C C rC {∅ −→ X, U −→ V } ≡ {∅ −→ X, ∅ −−1−−→ 2 2 V rX, U −− 1 −→ V} 1 C rC 2 C ∩C C ∩C C rC ≡ {∅ −− −→ X, ∅ −−1−−→ 2 X, ∅ −−1−−→ 2 2 V rX, U −− 1 −→ V} 1 C rC 2 C ∩C C rC ≡ {∅ −− −→ X, ∅ −−1−−→ 2 2 XV, U −− 1 −→ V} Analogously, when V ⊆ X, by applying Equivalence (3) and Axiom equivalence, one has Equivalence (5): 1 C 2 C 1 C C ∩C C rC {∅ −→ X, U −→ V } ≡ {∅ −→ X, U rX −−1−−→ 2 2 ∅, U −− 1 −→ V} 1C 2 1 C rC ≡ {∅ −→ X, U −− −→ V} t u The equivalences introduced in Proposition 2 constitute the core of the func- tion called CAISL-Prover, which acts as an automated prover for CAISL. The prover works by splitting the original formula into its left and right hand sides (see Theorem 2) and, by applying the equivalences, we check whether its right side can be reduced to the empty set. The derivability is proved if and only if such reduction is fulfilled. Finally, we conclude this section with an illustrative example. Steep State ∆X = {(M, a), (M, b), (M, d), (L, a), (L, b), (L, d)} 0 ∆Y = {(Q, a), (Q, b), (Q, d)} de a bd bde ab ae Σ = {Q −−→ M, M − → T, Q −−→ L, ML −−−→ Q, T −−→ RL, R −−→ Q} ∆X = {(M, a), (M, b), (M, d), (L, a), (L, b), (L, d)} 1 ∆Y = {(Q, a), (Q, b), (Q, d)} 6de a bd bde ab ae Σ = {Q −−→ M, M − → T, Q −−→ L, ML −−−→ Q, T −−→ RL, R −−→ Q} ∆X = {(M, a), (M, b), (M, d), (L, a), (L, b), (L, d), (T , a)} 2 ∆Y = {(Q, a), (Q, b), (Q, d)} e a bd bde ab ae Σ = {Q − → M, M −  → T, Q −−→ L, ML −−−→ Q, T −−→ RL, R − −→ Q} ∆X = {(M, a), (M, b), (M, d), (L, a), (L, b), (L, d), (T , a)} 3 ∆Y = {(Q, a), (Q, b), (Q, d)} e bd bde ab ae Σ = {Q − → M, Q −  −− → L, ML −−−→ Q, T −−→ RL, R − −→ Q} ∆X = {(M, a), (M, b), (M, d), (L, a), (L, b), (L, d), (T , a), (Q, b), (Q, d)} 4 ∆Y = {(Q, a)} e 6b6de ab ae Σ = {Q − → M, ML −−−→ Q, T −−→ RL, R − − → Q} ∆X = {(M, a), (M, b), (M, d), (L, a), (L, b), (L, d), (T , a), (Q, b), (Q, d), (R, a)} 5 ∆Y = {(Q, a)} e e 6ab ae Σ = {Q − → M, ML − → Q, T −−→ RL, R − −→ Q} ∆X = {(M, a), (M, b), (M, d), (L, a), (L, b), (L, d), (T , a), (Q, b), (Q, d), (R, a), (Q, a)} 6 ∆Y = ∅ e e b 6ae Σ = {Q − → M, ML − → Q, T − → R, R −−→ Q} Output Return TRUE abd Table 1. Illustration of the derivability of ML −−→ Q de a bd bde ab ae Example 2. Let Σ = {Q −→ M, M − → T, Q −→ L, ML −−→ Q, T −→ RL, R −→ Q} abd be a set of CAI s. The CAISL-Prover function proves that ML −−→ Q is inferred ab from Σ (see Table 1) and T −→ Q is not inferred from Σ (see Table 2). Step State ∆X = {(T , a), (T , b)} 0 ∆Y = {(Q, a), (Q, b)} de a bd bde ab ae Σ = {Q −−→ M, M − → T, Q −−→ L, ML −−−→ Q, T −−→ RL, R − −→ Q} ∆X = {(T , a), (T , b)} 1 ∆Y = {(Q, a), (Q, b)} de a bd bde ab ae Σ = {Q −−→ M, M − → T, Q −−→ L, ML −−−→ Q, T −−→ RL, R − −→ Q} ∆X = {(T , a), (T , b)} 2 ∆Y = {(Q, a), (Q, b)} de a bd bde ab ae Σ = {Q −−→ M, M − → T, Q −−→ L, ML −−−→ Q, T −−→ RL, R − −→ Q} ∆X = {(T , a), (T , b)} 3 ∆Y = {(Q, a), (Q, b)} de bd bde ab ae Σ = {Q −−→ M, Q − −−→ L, ML −−−→ Q, T −−→ RL, R − −→ Q} ∆X = {(T , a), (T , b)} 4 ∆Y = {(Q, a), (Q, b)} de bd bde ab ae Σ = {Q −−→ M, Q −−→ L, ML −−−→ Q, T −−→ RL, R − −→ Q} ∆X = {(T , a), (T , b), (R, a), (R, b), (L, a), (L, b)} 5 ∆Y = {(Q, a), (Q, b)} de bd bde ab  ae Σ = {Q −−  → M, Q −−→ L, ML −−−→ Q, T −−→ RL, R − −→ Q} ∆X = {(T , a), (T , b), (R, a), (R, b), (L, a), (L, b), (Q, a)} 6 ∆Y = {(Q, b))} de bd bde 6ae Σ = {Q −−→ M, Q −−→ L, ML −−−→ Q, R −−→ Q} Loop 2 ∆X = {(T , a), (T , b), (R, a), (R, b), (L, a), (L, b), (Q, a)} 7 ∆Y = {(Q, b))} de bd bde e Σ = {Q −−→ M, Q −−→ L, ML −−−→ Q, R − → Q} ∆X = {(T , a), (T , b), (R, a), (R, b), (L, a), (L, b), (Q, a)} 8 ∆Y = {(Q, b))} de 6b d bde e Σ = {Q −−→ M, Q − −− → L, ML −−−→ Q, R − → Q} ∆X = {(T , a), (T , b), (R, a), (R, b), (L, a), (L, b), (Q, a)} 9 ∆Y = {(Q, b))} de d bde e Σ = {Q −−→ M, Q − → L, ML −−−→ Q, R − → Q} ∆X = {(T , a), (T , b), (R, a), (R, b), (L, a), (L, b), (Q, a)} 10 ∆Y = {(Q, b))} de d bde e Σ = {Q −−→ M, Q − → L, ML −−−→ Q, R − → Q} Output Return FALSE ab Table 2. Illustration of the non derivability of T −→ Q 7 Conclusion and Future Work We have proposed a logic named CAISL to deal with conditional attribute impli- cations in Triadic Concept Analysis. Its soundness and completeness have been proved by establishing the equivalence between the axioms and rules of CAISL and those of CAIL - a recently developed solution [12]. This novel approach is strongly based on the Simplification paradigm which is a useful formalism to de- velop automated methods. In this direction, CAISL has been used to build an automated prover to check the derivability of a CAI from a set of CAI s, which is an important issue in data and knowledge management. The use of a logic-based approach is a challenging but very interesting issue that has not been explored in the TCA framework yet. Our short-term research activity is to adapt our proposal to other kinds of triadic implications and analyze the interplay between them. Acknowledgment This work is supported by regional project TIN2014-59471-P of the Science and Innovation Ministry of Spain, co-funded by the European Regional Development Fund (ERDF) as well as by a discovery grant from the Natural Sciences and Engineering Research Council of Canada (NSERC). References 1. Armstrong, W.: Dependency structures of data base relationships. Proc. IFIP Congress. North Holland, Amsterdam pp. 580–583 (1974) 2. Biedermann, K.: How triadic diagrams represent conceptual structures. In: ICCS. pp. 304–317 (1997) 3. Biedermann, K.: Powerset trilattices. In: ICCS. pp. 209–224 (1998) 4. Cordero, P., Enciso, M., Mora, A., P. de Guzmn, I.: Slfd logic: Elimination of data redundancy in knowledge representation. In: IBERAMIA. Lecture Notes in Com- puter Science, vol. 2527, pp. 141–150. Springer Berlin Heidelberg (2002) 5. Fagin, R.: Functional dependencies in a relational database and propositional logic. IBM. Journal of research and development 21 (6), 534–544 (1977) 6. Ganter, B., Obiedkov, S.A.: Implications in triadic formal contexts. In: ICCS. pp. 186–195 (2004) 7. Jäschke, R., Hotho, A., Schmitz, C., Ganter, B., Stumme, G.: Trias - an algorithm for mining iceberg tri-lattices. In: ICDM. pp. 907–911 (2006) 8. Lehmann, F., Wille, R.: A triadic approach to formal concept analysis. In: ICCS. pp. 32–43 (1995) 9. Maier, D.: The theory of Relational Databases. Computer Science Press (1983) 10. Missaoui, R., Kwuida, L.: Mining triadic association rules from ternary relations. In: Formal Concept Analysis - 9th International Conference, ICFCA 2011, Nicosia, Cyprus, May 2-6, 2011. Proceedings. pp. 204–218 (2011) 11. Peirce, C.S.: Collected Papers. Harvard University Press, Cambridge (1931-1935) 12. Rodrı́guez-Lorenzo, E., Cordero, P., Enciso, M., Missaoui, R., Mora, A.: An ax- iomatic system for conditional attribute implications in triadic concept analysis. Submitted to International Journal of Intelligent Systems (2016) 13. Wille, R.: The basic theorem of triadic concept analysis. Order 12(2), 149–158 (1995)