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 Simpli cation paradigm which o ers 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.
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 di erent axiomatic systems in FCA,
the rst one is called Armstrong's Axioms [
The rst study on triadic implications has been investigated by Biedermann [
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 de ne a new axiomatic system
based on Simpli cation Logic [
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 de ned 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 brie y presents a logic for conditional attribute
implications called CAIL [
As a natural extension to Formal Concept Analysis (FCA), theoretical foundations
of Triadic Concept Analysis have been investigated by Lehmann and Wille [
De nition 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.
In a similar way, X20, (X1; X3)0, X30 and (X1; X2)0 can be de ned. As shown
in [
There are a few kinds of triadic implications with di erent semantics.
Biedermann [
M and C (Y; C)0.
B.
Ganter and Obiedkov [
De nition 4 (Conditional attribute implication). Let K = hG; M; B; Ii be a triadic context, X; Y context K when (X; fcg)0
M and C B. The implication X !C Y holds in the
(Y; fcg)0 for all c 2 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 de nition is weaker than the CAI de nition.
Proposition 1 ([
B. Then X !C Y holds in K i (X ! Y )N also holds in K for all N
M and
In this section, we describe CAIL, a logic for reasoning about CAI s in the
framework of TCA [
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 ; = fA !C B j A; B ; C g.
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 fa; b; cg) and, as usual, the union is denoted by set juxtaposition (e.g. XY denotes X [ Y ). Semantics: Based on De nition 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 formula X !C Y 2 L ; is an interpretation that satis es X !C Y in K. In this case, we write K j= X !C Y .
As usual, for L ; , an interpretation K is a model for (brie y, K j= ) if K j= X !C Y for each X !C Y 2 . Similarly, j= X !C Y states that X !C Y is a semantic consequence of , i.e. every model for is also a model for X !C Y .
Syntactic inference: The syntactic derivation in CAIL is denoted by the symbol `C and covers two axiom schemes and four inference rules.
De nition 5. The CAIL axiomatic system consists of the following rules: [Non-constraint] `C ; !; . [Inclusion] `C XY ! X. [Augmentation] X !C Y `C XZ !C Y Z. [Transitivity] fX C!1 Y; Y C!2 Zg `C X C1\C!2 Z. [Conditional Decomposition] X C1C!2 Y `C X C!1 Y . [Conditional Composition] fX C!1 Y; Z C!2 W g `C XZ C1C!2 Y \W .
The derivation notion is introduced as usual: For a given set L ; and ' 2
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 2 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 f'j j 1 j < ig.
Soundness and completeness: In [
. and four inference rules: [Decomposition] fX C1C!2 Y Zg `S X C!1 Y . [Composition] fX C!1 Y; Z C!2 W g `S XZ C1\C!2 Y W . [Conditional Composition] fX C!1 Y; Z C!2 W g `S XZ C1C!2 Y \W . [Simplification] If X \ Y = ;,
fX C!1 Y; XZ C!2 W g `S XZ rY C1\C!2 W rY:
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 and X !C Y 2 L ; , one has L ; `S X !C 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 ii) Inference rules derived from CAISL [Composition]: 1. X C!1 Y . . . . . . . . . . Hypothesis. 2. Z C!2 W . . . . . . . . . . Hypothesis. 3. XZ C!1 Y Z . . . . . . . . . . . 1 Augm. 4. Y Z C!2 Y W . . . . . . . . . . 2 Augm. 5. XZ C1\C!2 Y W . . . . . 3; 4 Trans. [Inclusion]: 1. XY ! XY . . . . . . . Re exivity. 2. XY ! Y . . . . . . . . . . 1 Decomp. [Augmentation]: 1. X !C Y . . . . . . . . . . . Hypothesis. 2. Z ! Z . . . . . . . . . . . . . Re exivity. 3. XZ !C Y Z . . . . . . . . . 1; 2 Comp. [Transitivity]: 1. X C!1 Y . . . . . . . . . . . Hypothesis. 2. Y C!2 Z . . . . . . . . . . . Hypothesis. 3. X C!1 Y rX . . . . . . . 1 Decomp.
[Simplification]: 1. X C!1 Y . . . . . . . . . . Hypothesis. 2. XZ C!2 W . . . . . . . . Hypothesis. 3. XZ rY ! X . . . . . . . Inclusion. 4. W ! W rY . . . . . . . . Inclusion. 5. XZ C!2 W rY . . . . . 2; 4 Trans. 6. XZ rY C!1 Y . . . . . . 3; 1 Trans. 7. XZ rY C!1 XY Z . . . . 6 Augm. 8. XY Z C!2 W Y . . . . . . . 5 Augm. 9. XZ rY C1\C!2 W Y 7; 8 Trans. 10. XZ r Y C1\C!2 W r Y . 9 De
comp. 4. Y C!2 Z rY . . . . . . . . .2 Decomp. 5. X ! X . . . . . . . . . . . . Re exivity. 6. X ! ; . . . . . . . . . . . . . 5 Decomp. 7. XY C!2 Z rY . . . . . . 4; 6 Comp. 8. Y rX ! Y rX . . . .Re exivity. 9. X C1\C!2 Z rY . . . . . 3; 7 Simp. 10. X C1\C!2 Y Z . . . . . . 1; 9 Comp. 11. X C1\C!2 Z . . . . . . . 10 Decomp. [Conditional Decomposition]: 1. X C1C!2 Y . . . . . . . . . Hypothesis. 2. X C!1 Y . . . . . . . . . . . . 1 Decomp.
tu
Since the two axiomatic systems are equivalent, in the sequel we will omit the subscript in the syntactic derivation symbol using simply `.
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 Simpli cation 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. Equivalently, 1 2 i 1 ` ' for all ' 2 2, and 2 ` ' for all ' 2 1. Lemma 1. The following equivalences hold:
fX C!1 Y; X C!2 W g fX C!1 Y; XV C!2 W g fX C1\C!2 Y W; X C1rC!2 Y; X C2rC!1 W g fX C!1 Y; XV C2rC!1 W; X(V rY ) C1\C!2 W rY g (2) (1) Proof. For Equivalence (1), rst, we prove that X C1\C!2 Y W , X C1rC!2 Y , and X C2rC!1 W can be inferred from fX C!1 Y; X C!2 W g: { By applying Composition to X C!1 Y and X C!2 W , we get X C1\C!2 Y W . { X C1rC!2 Y and X C2rC!1 W are obtained by Decomposition.
On the other hand, we prove that X C!1 Y and X C!2 W can be inferred from fX C1\C!2 Y W; X C1rC!2 Y; X C2rC!1 W g by applying Conditional Composition.
For Equivalence (2), from fX C!1 Y; XV C!2 W g, we infer XV C2rC!1 W by applying Decomposition to XV C!2 W . In addition, we infer XV rY C1\C!2 WrY by applying Simpli cation to X C!1 Y and XV C!2 W .
Finally, fX C!1 Y; XV C2rC!1 W; XV r Y C1\C!2 W r Y g ` XV C!2 W is proved. By applying Re exivity and Decomposition, we get XV C1\C!2 XV rY and, by Transitivity with XV rY C1\C!2 W rY , one has XV C1\C!2 W rY . Now, by applying Composition to X C!1 Y and XV C1\C!2 W rY , we infer XV C1\C2 ! W Y and, by Decomposition, XV C1\C!2 W . At last, by applying Conditional Composition to XV C1\C!2 W and XV C2rC!1 W , we obtain XV C!2 W . tu
The following theorem highlights a common characteristic of Simpli cation Logics, which shows that inference rules can be read as equivalences that allow redundancy removal.
Theorem 2. The following equivalences hold: Axiom Eq.: fX !; Y g fX !C ;g Decomposition Eq.: fX !C Y g
; fX !C Y rXg Composition Eq.: fX !C Y; X !C W g fX !C Y W g Conditional Composition Eq.: fX C!1 Y; X C!2 Y g by re exivity. Then, by applying Decomposition, one has X !C Y . ii) X !C Y and X !C W are inferred by applying Decomposition to X !C Y W . tu
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 e ect 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 su cient condition to ensure the derivability of a CAI from a set of CAI s. 6
This section shows the merits of CAISL for the development of automated methods. Speci cally, 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.
L ; and X !C Y 2 L ; , one has ` X !C Y if and only if [ f; !C Xg ` ; !C Y Proof. Straightforwardly, we have ` X !C Y implies [ f; !C Xg ` ; !C Y . Conversely, assuming [ f; !C Xg ` ; !C Y , we have to prove that K j= implies K j= X !C Y for each model K.
Consider K = hG; M; B; Ii as a model of . In order to prove (X; fcg)0 (Y; fcg)0 for all c 2 C in K, we build the context K1 = hG1; M; B; I1i where G1 = (X; fcg)0 and I1 = I \ (G1 M B).
Since K j= , we have K1 j= fc!g Xg and therefore, by hypothesis, [ f; K1 j= f; fc!g Y g. That is, (Y; fcg)0 (;; fcg)0 = G1 = (X; fcg)0.
If we go back to the original triadic context K, (X; fcg)0 remains unchanged whereas (Y; fcg)0 could grow up. Therefore, in K, one has (X; fcg)0 (Y; fcg)0 for all c 2 C. tu Function CAISL-Prover( ,X !C Y ) input : A set of implications , and a CAI X !C Y output: A boolean answer begin
X := X
Y := (Y repeat ag:=false
C C)r(X
C) 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: f;
C!1 X; U C!2 V g
f; C!1 X; ; C1\C!2 V rX; U C2rC!1 V g Analogously, when V one has Equivalence (5): f;
C1rC!2 X; ; C1\C!2 X; ; C1\C!2 V rX; U C2rC!1 V g f; C1rC!2 X; ; C1\C!2 X V; U C2rC!1 V g
X , by applying Equivalence (3) and Axiom equivalence, f;
C!1 X; U C!2 V g f; C!1 X; U rX
C1\C!2 ;; U C2rC!1 V g f;
C!1 X; U C2rC!1 V g tu
The equivalences introduced in Proposition 2 constitute the core of the function 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 ful lled.
Finally, we conclude this section with an illustrative example.
Steep 0 1 2 3 4 5 Example 2. Let = fQ d!e M; M !a T; Q b!d L; ML bd!e Q; T a!b RL; R a!e Qg be a set of CAI s. The CAISL-Prover function proves that ML ab!d Q is inferred from (see Table 1) and T a!b Q is not inferred from (see Table 2).
Step
State 0 1 2 3 4 5 6 7 8 9
X = f(T; a); (T; b)g Y = f(Q; a); (Q; b)g = fQ d!e M, M a! T; Q bd! L; ML bd!e Q; T ab! RL; R a!e Qg X = f(T; a); (T; b)g Y = f(Q; a); (Q; b)g = fQ de! M; M a! T; Q bd! L; ML bd!e Q; T ab! RL; R a!e Qg X = f(T; a); (T; b)g Y = f(Q; a); (Q; b)g = fQ d!e M; M a! T; Q bd! L; ML bd!e Q; T ab! RL; R a!e Qg X = f(T; a); (T; b)g Y = f(Q; a); (Q; b)g = fQ d!e M; Q bd! L; ML bd!e Q; T ab! RL; R a!e Qg X = f(T; a); (T; b)g Y = f(Q; a); (Q; b)g = fQ d!e M; Q bd! L; ML bde! Q; T ab! RL; R a!e Qg X = f(T; a); (T; b); (R; a); (R; b); (L; a); (L; b)g Y = f(Q; a); (Q; b)g = fQ d!e M; Q bd! L; ML bd!e Q; T ab! RL; R a!e Qg X = f(T; a); (T; b); (R; a); (R; b); (L; a); (L; b); (Q; a)g Y = f(Q; b))g = fQ d!e M; Q bd! L; ML bd!e Q; R 6ae! Qg
Loop 2 X = f(T; a); (T; b); (R; a); (R; b); (L; a); (L; b); (Q; a)g Y = f(Q; b))g = fQ de! M; Q bd! L; ML bd!e Q; R !e Qg X = f(T; a); (T; b); (R; a); (R; b); (L; a); (L; b); (Q; a)g Y = f(Q; b))g = fQ d!e M; Q 6bd! L; ML bd!e Q; R !e Qg X = f(T; a); (T; b); (R; a); (R; b); (L; a); (L; b); (Q; a)g Y = f(Q; b))g = fQ d!e M; Q d! L; ML bde! Q; R !e Qg
X = f(T; a); (T; b); (R; a); (R; b); (L; a); (L; b); (Q; a)g 10 Y = f(Q; b))g
= fQ d!e M; Q d! L; ML bd!e Q; R e! Qg Output Return FALSE
We have proposed a logic named CAISL to deal with conditional attribute
implications 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 [
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.
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).