Towards Simplification Logic for Graded Attribute Implications with General Semantics

Abstract

We present variant of simplification logic for reasoning with if-then dependencies that arise in formal concept analysis of data with graded attributes. The dependencies and the proposed logic are parameterized by systems of isotone Galois connections which allows us to handle a large family of possible interpretations of data dependencies. We describe semantics of the rules, axiomatic system of the logic, and prove its soundness and completeness.

Keywords

• Closure operator
• lattice theory
• fuzzy logic
• implication

-

In this paper, we contribute to the area of inference systems that emerge in formal concept analysis [ 10 ] of data with graded attributes. By a graded attribute, sometimes called a fuzzy attribute, we mean an attribute that may apply to an object to degrees. Needless to say, there are basically two options to treat such attributes: Either by binary scaling and exploiting the existing methods in FCA or by providing a suitable formalization of structures of degrees and developing FCA considering such structures in order to include “graded attributes” as fundamental notions. In this paper, we use the “approach by generalization” and explore general inference systems related to graded attribute implications, i.e., if-then formulas describing dependencies between graded attributes. 1.1

Early Approaches

The first approach to FCA that contained results on graded attribute implications was introduced by Silke Polandt in her somewhat unappreciated book [ 19 ]. The approach is based on residuated lattices [ 28 ] considered as basic structures of truth degrees [ 11,13 ] and introduces attribute implications as if-then formulas A ⇒ B, where A and B are graded collections of attributes (fuzzy sets of attributes), i.e., technically both A and B are maps A : Y → L and B : Y → L, where Y is a set of attributes and L is a set of utilized degrees. The interpretation of A ⇒ B in a given formal context with graded attributes is defined in terms of a graded subsethood. c paper author(s), 2018. Proceedings volume published and copyrighted by its editors.

Paper published in Dmitry I. Ignatov, Lhouari Nourine (Eds.): CLA 2018, pp. 129{140, Department of Computer Science, Palacky University Olomouc, 2018. Copying permitted only for private and academic purposes.

The role of the graded subsethood in [ 19 ] as well as in the later approaches is crucial, so let us clarify what we mean by that. The classic subsethood (or inclusion) can be seen as a binary relation on the set of all subsets of a given universe, e.g., the set of all attributes. When one thinks of a subsethood in presence of graded attributes, it appears almost immediately that there seem to be multiple reasonable choices for that. For instance, for maps A and B as above, we might say that “B is fully included in A” whenever B(y) ≤ A(y) for each attribute y ∈ Y , where ≤ is a partial order on the set of all degrees in L. As such, the full inclusion is a classic binary relation on the set of all graded sets in the universe Y , i.e., for each A, B, either B is fully included in A or not.

However straightforward, the full inclusion may be regarded as not natural by some because it does not reflect closeness of degrees. For instance, when B(y) ≤ A(y) for all y except for some z ∈ Y for which we have B(z) = 0.63 and A(y) = 0.62 (when a real unit interval is used as the scale of truth degrees), then B is not fully included in A, however, most observers would regard B to be almost fully a subset of A. This issue can be resolved by introducing a graded subsethood. While there are many approaches to define a graded subsethood, [ 19 ] and later works use the one introduced by Goguen [ 11 ] which is based on residuated implication. Using the notation of [ 2 ], a degree S(A, M ) to which A is a subset of M (see [2, p. 82]) is defined by

S(A, M ) = Vy∈Y A(y) → M (y) , where A : Y → L, M : Y → L, → is residuum (a truth function of graded/fuzzy implication), i.e., S(A, M ) is the infimum of degrees A(y) → M (y) for all y ∈ Y . Since S(A, M ) is a general degree from L, a high degree S(A, M ) can naturally be interpreted so that “A is almost included in M .” Interestingly, the two notions of subsethood are related in the following sense: “A is fully included in M ” if and only iff S(A, M ) = 1 (with 1 being the highest degree in L).

Using the graded subsethood (and the notation of [ 2,13 ]), the initial approach to attribute implications [ 19 ] defined a degree to which A ⇒ B holds for an object x ∈ X by

||A ⇒ B||Ix = S(A, Ix) → S(B, Ix), where Ix : Y → L represents graded attributes of the object x ∈ X (i.e., Ix(y) is a “degree to which object x has the attribute y.”) One can immediately see that (2) is indeed a proper generalization of the classic notion of A ⇒ B (where A, B ⊆ Y ) being true in Ix ⊆ Y . By a straightforward extension of the notion, we can introduce a degree ||A ⇒ B||hX,Y,Ii to which a graded attribute implication A ⇒ B is true in a context hX, Y, Ii with graded attributes:

||A ⇒ B||hX,Y,Ii = Vx∈X ||A ⇒ B||Ix .

In this setting, Polandt [ 19 ] investigated several important areas including characterization of completeness in data and similarity issues. (1) (2)

Approaches Using Hedges

The approach by Pollandt is sound but it turned out it lacks a certain level of generality that can be found in the approach using hedges which initally started by [ 3 ], cf. also [ 6,7 ] for comprehensive description. The approach uses a linguistic hedge [ 29 ] as an additional parameter that influences the interpretation of graded attribute implications and related notions from FCA [ 5 ]. Technically, instead of considering (2), one considers ||A ⇒ B||I∗x defined by

||A ⇒ B||I∗x = S(A, Ix)∗ → S(B, Ix), where ∗ is an idempotent truth-stressing linguistic hedge [ 14 ]. By letting ∗ being the identity map on L, (3) collapses into the Pollandt-style definition (2). The interesting point about this particular general approach is that for other choices of hedges, we obtain other interesting interpretations of graded dependencies. For instance, when ∗ is the so-called globalization [ 22 ], then (3) becomes ||A ⇒ B||I∗x = 1, if S(A, Ix) < 1, S(B, Ix), otherwise. (3) (4) In particular, ||A ⇒ B||I∗x = 1 iff S(A, Ix) = 1 (i.e., A is fully contained in Ix) implies S(B, Ix) = 1 (i.e., B is fully contained in Ix). In general, (2) and (4) are different and coincide only if the scale of degrees is a two-valued Boolean algebra. Therefore, the approach by hedges can be seen as a generalization that encompasses interpretation of graded if-then rules based on both the graded and full inclusions and these two borderline cases result by different choices of hedges. This is an important aspect from users’ point of view.

From the theoretical point of view, the generalization by hedges brought new insights into the properties of several important notions depending on the choice of a hedge. For instance, minimal bases and pseudo-intents in the general setting [ 3,7 ] have almost the exact same characterization as in the classic case [ 12 ] when the hedge is globalization which it is not the case for general hedges where several incomparable systems of pseudo-intents may exist for a single dataset, see [ 24,25 ] for details. 1.3

Parameterizations by Isotone Galois Connections

The present paper is closely related to general methods of parameterizing the semantics of graded attribute implications proposed in [ 26 ]. Such parameterizations subsume the paramaterizations by hedges as well as other non-trivial alternative semantics of attribute implications. It may be motivated by two fundamental observations on properties of graded attribute implications paramaterized by hedges [ 6,7 ]. First, we have [6, Theorem 3] ||A ⇒ B||I∗x = W c ∈ L; ||A ⇒ c⊗B||I∗x = 1 , (5) where c⊗B denotes a map from Y to L such that (c⊗B)(y) = c ⊗ B(y), where ⊗ is the multiplication adjoint to → appearing in (1). Put in words, (5) shows that the degrees to which graded attribute implications are true can be expressed just by focusing on implications that are fully true, i.e., true to degree 1. (6) (7)

Second, we have ||A ⇒ B||I∗x = 1 (i.e., A ⇒ B is fully true in Ix) iff for any truth degree c ∈ L, it holds that [6, Lemma 2]

S(c∗⊗A, Ix) = 1 implies S(c∗⊗B, Ix) = 1.

By a slight abuse of notation and denoting the full inclusion by ⊆, the previous condition can be restated as follows:

c∗⊗A ⊆ Ix implies c∗⊗B ⊆ Ix.

Therefore, one may introduce a general interpretation of graded attribute implications A ⇒ B by defining A ⇒ B true in Ix whenever the following condition holds: For any f ∈ S, it holds that f (A) ⊆ Ix implies f (B) ⊆ Ix. In order to obtain a formalization which is sufficiently strong, [ 26 ] shows that it is sufficient to consider S as a set of (lower) adjoints of isotone Galois connections that is closed under composition. Using this formalism, [ 26 ] shows a standard agenda of attribute implications, including a complete Armstrong-style [ 1 ] axiomatization and characterization of completeness in data.

The parameterizations by systems of isotone Galois connections can be used not only in case of graded attribute implications but for other formalisms for reasoning with if-then rules. For instance, attribute implications developed in context of linear temporal logic [ 23 ] fall in this category as well. The properties of this family of parameterizations and related closure structures are studied in [ 27 ]. 1.4

Our Contribution

As an alternative to the well-known Armstrong inference system [ 1 ] which is not very suitable for automated reasoning, [ 9 ] proposed a simplification logic and novel algorithms for if-then rules based on simplification equivalence. Further results derived from this work include automated methods based directly on the simplification logic [ 17,18,8,16,15 ]. The simplification logic was later introduced for graded attribute implications parameterized by hedges in [ 4 ].

In this paper, we outline a general simplification logic for graded if-then rules whose semantics is parameterized by systems of isotone Galois connections. In Section 2, we present the underlying algebraic structures that are involved in the simplification logic as well as the parameterizations. We emphasize that, we utilize the co-residuated lattices in order to have a reasonable truth-function of logical difference upon which the simplification logic is based. The role of the classic multiplications and residua in the ordinary residuated lattices is substituted by the general parameterizations. In Section 3, we outline the logic including the semantics of its formulas, we present an inference system and show its soundness. Furthermore, in Section 4 and Section 5, we present a further properties of the inference system and outline the completeness result. 2

Preliminaries

Throughout this paper we consider, as the structure of degrees, a complete coresiduated lattice, that is, an algebra L = hL, ≤, ⊕, , 0, 1i satisfying the following conditions: – hL, ≤, 0, 1i is a complete lattice where 0 is the least element and 1 is the greatest element. As usual, we use the symbols ∨ and ∧ to denote suprema (least upper bounds) and infima (greatest lower bounds), respectively. – hL, ⊕, 0i is a commutative monoid. – The pair h⊕, i satisfies the following adjointness property:

For all a, b, c ∈ L, a ≤ b ⊕ c if and only if a b ≤ c.

(8) Notice that (8) is equivalent to the following condition:

(a ⊕ b) a ≤ b ≤ a ⊕ (b a), for all a, b ∈ L. (9) Any complete Brouwerian algebra [ 21,20 ] (also known as complete co-Heyting algebra) is a complete co-residuated lattice. Thus, as an example of complete coresiduated lattice, one has the unit interval with the operations ⊕ and such that a ⊕ b = max{a, b}, a b = a when b < a, and a b = 0 otherwise. We also take advantage of the following properties: a ≤ b if and only if a a 0 = a, a b ≤ a ≤ a ⊕ b, b ≤ c implies a ⊕ b ≤ a ⊕ c, b a ∨ b ≤ a ⊕ (b a ⊕ ((a ⊕ b)

a) ≤ a ⊕ b, c) = a ⊕ (b a ⊕ (b ∧ c) = (a ⊕ b) ∧ (a ⊕ c).

c), b = 0, a ≤ c a and a c ≤ a b, (10) (11) (12) (13) (14) (15) (16)

For illustration, we use a running example based on a particular structure of degrees. The structure is shown in the next example.

Example 1. Consider L = hL, ≤, ⊕, , 0, 1i where L = { 1i0 | i ∈ N, 0 ≤ i ≤ 10}, the relation ≤ is the usual order, and ⊕ and are defined as follows: a ⊕ b = am+axb{,12 , a, b}, iofthae+rwbis≤e, 21 , a b =  10m,−axb{,a, b}, iioffth0ae≤≤rwbbi,s<e. a ≤ 21 , It is easy to see that L is a complete co-residuated lattice.

Using L, we use the notion of L-fuzzy sets, i.e., maps from non-empty universe sets to L. The collection of all L-fuzzy sets in universe Y is denoted by LY . Also, in the examples we use the usual notation {. . . , y/A(y) . . .} for writing L-fuzzy sets in finite universes.

Operations in L can be extended pointwise to L-fuzzy sets in the usual way: For A, B ∈ LY the L-fuzzy sets A ⊕ B and A B are defined by (A ⊕ B)(y) = A(y) ⊕ B(y) and (A B)(y) = A(y) B(y) for all y ∈ Y .

The parameterizations [ 26 ] we use in out paper are defined in terms of isotone Galois connections in hLY , ⊆i. Specifically, we consider pairs of self-maps hf , gi, i.e., f : LY → LY and g : LY → LY , such that, for all A, B ∈ LY , f (A) ⊆ B iff A ⊆ g(B). (17) In this pair, each mapping is uniquely determined by the other, because f (A) = T{B ∈ LY | A ⊆ g(B)} and g(B) = S{A ∈ LY | f (A) ⊆ B}. It is well-known that (17) is equivalent to postulating that both of the following conditions hold: 1. f and g are isotone, i.e., A ⊆ B implies f (A) ⊆ f (B) and g(A) ⊆ g(B) for all A, B ∈ LY . 2. g ◦ f is inflationary (extensive) and f ◦ g is deflationary (intensive), i.e.,

A ⊆ g(f (A)) and f (g(A)) ⊆ A for all A ∈ LY .

In fact, g ◦f is a closure operator and f ◦g is a kernel operator (interior operator ).

For any isomorphism f in hLY , ⊆i, the pair hf , f −1i is an isotone Galois connection. Thus, the identity mapping IY : LY → LY , with IY (A) = A for all A ∈ LY , provides an isotone Galois connection. Another important example is h0Y , 1Y i where 0Y (A)(y) = 0 and 1Y (A)(y) = 1, for any A ∈ LY and y ∈ Y .

In addition, given two isotone Galois connections hf 1, g1i and hf 2, g2i, their composition hf 1 ◦ f 2, g2 ◦ g1i is also an isotone Galois connection. Definition 1. A family of isotone Galois connections S in hLY , ⊆i is said to be an L-parameterization [ 26 ] if it is closed for composition and contains the identity.

In other words, S is an L-parameterization iff S = S, ◦, hIY , IY i is a monoid. Example 2. Consider the algebra L introduced in Example 1, an arbitrary nonempty set Y and, for each ` ∈ L, an isotone Galois connection hf `, g`i in hLY , ⊆i defined as follows: for all A ∈ LY and y ∈ Y , f `(A)(y) = max{0, A(y) − `} and g`(A)(y) = min{1, A(y) + `}.

In particular, f 1 = 0Y , g1 = 1Y , and f 0 = g0 = IY .

The family S = {hf 5i , g 5i i | i ∈ N, 0 ≤ i ≤ 5} is an L-parameterization. 3

Parameterized Simplification Logic

Given a non-empty alphabet Y , whose elements are named attributes, the set of well-formed formulas of the language is:

Y .

LY = {A ⇒ B | A, B ∈ L } These well-formed formulas will be named implications and, in each implication, the first and the second component will be named premise and conclusion respectively. Finally, the sets of implications Σ ⊆ L will be named theories.

We have just introduced the syntax of our logic. In the rest of the section we complete its formal presentation. Thus, first we introduce the semantics of the logic, second we present an axiomatic system and, finally, we show that both the semantic and the syntactic points of views coincide proving the soundness and completeness of the axiomatic system. 3.1

Semantics

Before we define the interpretation of formulas, we introduce S-additive L-fuzzy sets that will play the role of models. Definition 2. Let Y be a non-empty set and S be an L-parameterization. An L-fuzzy set A ∈ LY is said to be S-additive if f (B) ⊆ A and f (C) ⊆ A imply f (B ⊕ C) ⊆ A, for all B, C ∈ LY and hf , gi ∈ S.

The following proposition follows directly from Definition 2 and (17). Proposition 1. Let Y be a non-empty set and S be an L-parameterization. An L-fuzzy set A ∈ LY is S-additive if and only if g(A) ⊕ g(A) = g(A). Example 3. Let L be the algebra introduced in Example 1, S be the L-parameterization introduced in Example 2, and Y be an arbitrary non-empty set. A set A ∈ LY is S-additive if and only if, for all y ∈ Y , A(y) = 0 or A(y) ≥ 12 .

Fixed S being an L-parameterization, the models of the logic are defined in terms of S-additive L-sets as follows: Definition 3. Let A ⇒ B ∈ LY . An S-additive set M ∈ LY is said to be a model for A ⇒ B if f (A) ⊆ M implies f (B) ⊆ M , for all hf , gi ∈ S. The set of models for A ⇒ B is denoted by Mod(A ⇒ B). As usual, we say that an S-additive set M is model for a theory Σ ⊆ LY if it is model for all the implications A ⇒ B ∈ Σ, that is, Mod(Σ) = TA⇒B∈Σ Mod(A ⇒ B).

As it is usual for graded attribute implications, we can interpret our formulas in L-contexts. An L-context I = hX, Y, Ii consists of a non-empty sets X (and Y ) of objects (and attributes—as before) and a map I : X × Y → L. For x ∈ X, we consider Ix ∈ LY such that Ix(y) = I(x, y) for all y ∈ Y . An L-context I = hX, Y, Ii is called a model of A ⇒ B whenever {Ix | x ∈ X} ⊆ Mod(A ⇒ B). Example 4. Consider the algebra L introduced in Example 1 and the L-parameterization S introduced in Example 2. For the following L-contexts

– The implication A ⇒ B is said to be semantically derived from the theory Σ1 if Mod(Σ1) ⊆ Mod(A ⇒ B). It is denoted by Σ1 |= A ⇒ B. – Both theories Σ1 and Σ2 are said to be semantically equivalent if Mod(Σ1) =

Mod(Σ2). It is denoted by Σ1 ≡ Σ2.

3.2 Inference System

We look for a syntactic inference system capable of characterizing the semantic entailment |= as defined before. In this subsection, we introduce the inference system and prove its soundness.

Definition 5. For all A, B, C, D ∈ LY and hf , gi ∈ S, the inference system consists of following axiom scheme:

Reflexivity : Infer A ⇒ A,

together the following inference rules:

Composition : From A ⇒ B and A ⇒ C infer A ⇒ B ⊕ C,

Simplification : From A ⇒ B and C ⇒ D infer A ⊕ (C

B) ⇒ D,

Extension : From A ⇒ B infer f (A) ⇒ f (B).

(Ref) (Comp) (Simp) (Ext) The notion of syntactic derivation, or inference, is introduced in the standard way. Definition 6 (Syntactic derivation). An implication A ⇒ B ∈ LY is said to be syntactically derived or inferred from a theory Σ ⊆ LY , denoted by Σ ` A ⇒ B, if there exists a sequence σ1, . . . , σn ∈ LY such that σn is the implication A ⇒ B and, for all 1 ≤ i ≤ n, one of the following conditions holds: – σi ∈ Σ; – σi is an axiom obtained from (Ref); – σi is obtained by applying any of the inference rules (Comp), (Simp), or (Ext) to formulas in {σj | 1 ≤ j < i}.

Theorem 1 (Soundness). For any implication A ⇒ B ∈ LY and any theory Σ ⊆ LY , it follows that Σ ` A ⇒ B implies Σ |= A ⇒ B.

Proof. Assume that Σ ` A ⇒ B, i.e. there exists a sequence σ1, . . . , σn ∈ LY such that the conditions in Definition 6 hold. We prove that any model M ∈ Mod(Σ) is model for σi for all 1 ≤ i ≤ n and, therefore, M ∈ Mod(A ⇒ B).

It is straightforward that, if σi is an axiom or belongs to Σ, the set M is a model for σi. Assume now that M ∈ Mod{σj | 1 ≤ j < i} and prove that M is model for any formula that is obtained by applying (Comp), (Simp) or (Ext).

We only show the proof for (Simp) because the cases of (Comp) and (Ext) are straightforward from the facts that the models are S-additive and S is closed under compositions, respectively.

Consider U1 ⇒ V1, U2 ⇒ V2 ∈ {σj | 1 ≤ j < i}. Since M is model for these implications, we have that f (Uk) ⊆ M implies f (Vk) ⊆ M , for all hf , gi ∈ S and k ∈ {1, 2}. We must prove that M is model for U1 ⊕ (U2 V1) ⇒ V2.

Consider hf , gi ∈ S such that f (U1 ⊕ (U2 V1)) ⊆ M . Since f is isotone and U1 ⊆ U1 ⊕ (U2 V1), we have that f (U1) ⊆ M and, therefore, f (V1) ⊆ M . Now, from the S-additivity of M , f (V1 ⊕ U1 ⊕ (U2 V1)) ⊆ M . From (9), we have U2 ⊆ V1 ⊕ (U2 V1) ⊆ V1 ⊕ U1 ⊕ (U2 V1) and, therefore, f (U2) ⊆ M . Finally, since M is model for U2 ⇒ V2, we have that f (V2) ⊆ M . tu

Basic Properties

In this section we show equivalences that are derived from the primitive inference rules and allow us to remove redundant information, i.e., simplify theories. In the following proposition we introduce some derived inference rules.

Proposition 2. The following rules are derived from the axiomatic system:

Generalized Reflexivity : ` A ⇒ B when B ⊆ A

Transitivity : A ⇒ B, B ⇒ C ` A ⇒ C

Generalization : A ⇒ B ` C ⇒ D when A ⊆ C and D ⊆ B

Generalized Composition : A ⇒ B, C ⇒ D ` A ∪ C ⇒ B ⊕ D Augmentation : A ⇒ B ` A ∪ C ⇒ B ⊕ C

Generalized Transitivity : A ⇒ B, B ∪ C ⇒ D ` A ∪ C ⇒ D

Proof. All (GRef)–(GTran) can be verified using properties of ⊕ and in L.

tu

One outstanding characteristic of Simplification logic is that their inference rules induces a set of equivalences, providing a way to design automated prover methods strongly based in the axiomatic system presented in Definition 5. In the following proposition we present these equivalences. (GRef) (Tran)

(Gen) (GComp)

(Augm) (GTran) (DeEq) (CoEq) (CoEq) Proposition 3. The following equivalences hold:

Decomposition : {A ⇒ B} ≡ {A ⇒ B A} Composition : {A ⇒ B, A ⇒ C} ≡ {A ⇒ B⊕C} Simplification : if A ⊆ C, {A ⇒ B, C ⇒ D} ≡ {A ⇒ B, C

B ⇒ D

B} Proof. These equivalences, read from left to right, follow directly from (GRef), (Comp), and (Simp). For limitations of space we will prove the opposite direction only for (DeEq): In order to see that {A ⇒ B A} ` A ⇒ B holds, observe that In the last step, we have utilized the fact that B ⊆ A ⊕ B ⊆ A ⊕ (B In this section, we prove the completeness of the axiomatic system in the case of both L and Y are finite. First, we consider, in this framework, the generalization of the notion of syntactic closure of an L-set.

Theorem 2. Let Σ ⊆ LY be a theory. If LY is finite, the mapping cΣ : LY defined as follows: for each A ∈ LY , → LY cΣ (A) = S{B ∈ LY | Σ ` A ⇒ B} is a closure operator in hLY , ⊆i. In addition,

Σ ` A ⇒ B if and only if B ⊆ cΣ (A) for all A, B ∈ LY .

Proof (Sketch). From (Ref) and (Tran), we easily obtain that cΣ is extensive and isotone. Now, since LY is finite, applying (Comp) and (Gen) a finite number of times we get Σ ` A ⇒ cΣ (A). The rest is obvious. tu Definition 7 (Syntactic closure). Given Σ ⊆ LY and A ∈ LY , the set cΣ (A) is called syntactic closure of A with respect to Σ.

Theorem 3. If LY is finite, for any theory Σ ⊆ LY , we have that Y .

Mod(Σ) = {cΣ (A) | A ∈ L } Proof. First, for all A ∈ LY , we prove that cΣ (A) is S-additive: given hf , gi ∈ S, if f (B) ⊆ cΣ (A) and f (C) ⊆ cΣ (A), from Theorem 2, Σ ` A ⇒ f (B) and Σ ` A ⇒ f (C). The following sequence prove that Σ ` A ⇒ f (B ⊕ C) and, therefore, f (B ⊕ C) ⊆ cΣ (A).

Second, we prove that cΣ (A) is model for Σ: for all hf , gi ∈ S, if U ⇒ V ∈ Σ and f (U ) ⊆ cΣ (A), then Σ ` A ⇒ f (U ) and, by (Ext), Σ ` f (U ) ⇒ f (V ). Therefore, by (Tran), Σ ` A ⇒ f (V ) and f (V ) ⊆ cΣ (A).

Finally, it is straightforward that cΣ (M ) = M for any M ∈ Mod(Σ). tu We already have the necessary results to ensure that everything that can be semantically derived can also be syntactically inferred.

Theorem 4 (Completeness). If LY is finite, Σ |= A ⇒ B implies Σ ` A ⇒ B, for any Σ ⊆ LY and A ⇒ B ∈ LY .

Proof. If Σ 6` A ⇒ B, then, from Theorem 3, cΣ (A) ∈ Mod(Σ) but, from Theorem 2, cΣ (A) 6∈ Mod(A ⇒ B). Therefore, Σ 6|= A ⇒ B. tu

Returning to the graded attribute implications parameterized by hedges, it can be easily seen that our inference system and the complete logic presented in our paper generalizes the simplification logic for (FASL) from [ 4 ]. Indeed, one may put ⊕ = ∨ and let be the adjoint operation satisfying (8). Furthermore, given a hedge ∗, one can consider an L-parameterization S which consists of all hfc∗⊗, gc∗→i where (fc∗⊗(A))(y) = c∗ ⊗ A(y) and (gc∗→(A))(y) = c∗ → A(y) for any A ∈ LY , c ∈ L, and y ∈ Y . In this setting, our inference system coincides with the inference system of FASL. In particular, the rule of multiplication (from A ⇒ B infer c∗⊗A ⇒ c∗⊗B), cf. also [ 6,26 ], coincides with (Ext). 6

Conclusions

In this work, we have proposed a parameterized simplification logic for reasoning with graded implications in formal concept analysis. To achieve this goal, we have used systems of isotone Galois connections to handle a large family of possible interpretations in data dependencies. As it is usual, the logic was described in terms of a formal language, the semantics, and the axiomatic system. We proved its soundness and completeness. We showed how FASL proposed in [ 4 ] is a particular case of the parameterized simplification logic proposed in the present paper. In addition, different logics can be seen as particular cases of the general setting established here. Future research will focus on efficient algorithms based on the proposed logic.

Acknowledgment

Supported by Grants TIN2014-59471-P and TIN2017-89023-P of the Science and Innovation Ministry of Spain, co-funded by the European Regional Development Fund (ERDF). V. Vychodil was also supported the ECOP (Education for Competitiveness Operational Programme) project no. CZ.1.07/2.3.00/20.0059, which was co-financed by the European Social Fund and the state budget of the Czech Republic during 2011–2014.

References

1. Armstrong , W.W.: Dependency structures of data base relationships . In: Rosenfeld, J.L. , Freeman , H. (eds.) Information Processing 74: Proceedings of IFIP Congress . pp. 580 - 583 . North Holland, Amsterdam ( 1974 )

2. Belohlavek , R.: Fuzzy Relational Systems: Foundations and Principles . Kluwer Academic Publishers, Norwell, MA, USA ( 2002 )

3. Belohlavek , R. , Chlupova , M. , Vychodil , V. : Implications from data with fuzzy attributes . In: Proc. 2004 IEEE International Conference on Advances in I ntelligent Systems-Theory and Applications . University of Canberra, Centre de Recherche Public Henri Tudor ( 2004 ), 5 pages

4. Belohlavek , R. , Cordero , P. , Enciso , M. , Mora , A. , Vychodil , V.: Automated prover for attribute dependencies in data with grades . International Journal of Approximate Reasoning 70 , 51 - 67 ( 2016 )

5. Belohlavek , R. , Vychodil , V. : Formal concept analysis and linguistic hedges . International Journal of General Systems 41 ( 5 ), 503 - 532 ( 2012 )

6. Belohlavek , R. , Vychodil , V. : Attribute dependencies for data with grades I . International Journal of General Systems 45 ( 7-8 ), 864 - 888 ( 2016 )

7. Belohlavek , R. , Vychodil , V. : Attribute dependencies for data with grades II . International Journal of General Systems 46 ( 1 ), 66 - 92 ( 2017 )

8. Cordero , P. , Enciso , M. , Mora , A. , Ojeda-Aciego , M. : Computing minimal generators from implications: a logic-guided approach . In: Proc. of Concept Lattices and Applications , CLA 2012 . pp. 187 - 198 ( 2012 )

9. Cordero , P. , Enciso , M.M. , Mora , A. , de Guzma´n, I.P.I. , Mora , A ´., P´erez de Guzman, I.: SLFD Logic: Elimination of Data Redundancy in Knowledge Representation 2527 , 141 - 150 ( 2002 )

10. Ganter , B. , Wille , R.: Formal Concept Analysis: Mathematical Foundations . Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1st edn. ( 1997 )

11. Goguen , J.A.: The logic of inexact concepts . Synthese 19 , 325 - 373 ( 1969 )

12. Guigues , J.L. , Duquenne , V. : Familles minimales d'implications informatives resultant d'un tableau de donn´ees binaires . Math. Sci. Humaines 95 , 5 - 18 ( 1986 )

13. Ha´jek, P.: Metamathematics of Fuzzy Logic. Kluwer Academic Publishers, Dordrecht, The Netherlands ( 1998 )

14. Ha´jek, P.: On very true . Fuzzy Sets and Systems 124 ( 3 ), 329 - 333 ( 2001 )

15. Lorenzo , E.R. , Adaricheva , K.V. , Cordero , P. , Enciso , M. , Mora , A. : From an Implicational System to its Corresponding D-basis . In: Proceedings of the Twelfth International Conference on Concept Lattices and Their Applications , ClermontFerrand, France, October 13-16 , 2015 . pp. 217 - 228 ( 2015 )

16. Lorenzo , E.R. , Bertet , K. , Cordero , P. , Enciso , M. , Mora , A. : The direct-optimal basis via reductions . In: Proceedings of the Eleventh International Conference on Concept Lattices and Their Applications , Koˇsice, Slovakia, October 7- 10 , 2014 . pp. 145 - 156 ( 2014 )

17. Mora , A. , Cordero , P. , Enciso , M. , Fortes , I. , Aguilera , G.: Closure via functional dependence simplification . International Journal of Computer Mathematics 89 ( 4 ), 510 - 526 ( 2012 )

18. Mora , A ´., Enciso , M. , Cordero , P., de Guzma´n, I.P.P.: An Efficient Preprocessing Transformation for Functional Dependencies Sets Based on the Substitution Paradigm . Lecture Notes in Computer Science , vol. 3040 , pp. 136 - 146 ( 2003 )

19. Pollandt , S. : Fuzzy-Begriffe: Formale Begriffsanalyse unscharfer Daten . Springer ( 1997 )

20. Rauszer , C. : Semi-boolean algebras and their applications to intuitionistic logic with dual operations . Fundamenta Mathematicae 83 ( 3 ), 219 - 249 ( 1974 )

21. Stone , M.H. : Topological representations of distributive lattices and brouwerian logics . Cˇasopis pro pˇestova´n´ı matematiky a fysiky 67(1) , 1 - 25 ( 1938 )

22. Takeuti , G. , Titani , S. : Globalization of intuitionistic set theory . Annals of Pure and Applied Logic 33 , 195 - 211 ( 1987 )

23. Triska , J. , Vychodil , V. : Logic of temporal attribute implications . Annals of Mathematics and Artificial Intelligence 79 ( 4 ), 307 - 335 ( 2017 )

24. Vychodil , V.: On minimal sets of graded attribute implications . Information Sciences 294 , 478 - 488 ( 2015 )

25. Vychodil , V.: Computing sets of graded attribute implications with witnessed nonredundancy . Information Sciences 351 , 90 - 100 ( 2016 )

26. Vychodil , V.: Parameterizing the semantics of fuzzy attribute implications by systems of isotone Galois connections . IEEE Trans. on Fuzzy Systems 24 , 645 - 660 ( 2016 )

27. Vychodil , V.: Closure structures parameterized by systems of isotone Galois connections . International Journal of Approximate Reasoning 91 , 1 - 21 ( 2017 )

28. Ward , M. , Dilworth , R.P. : Residuated lattices . Trans. Amer. Math. Soc . 45 , 335 - 354 ( 1939 )

29. Zadeh , L.A. : A fuzzy-set-theoretic interpretation of linguistic hedges . Journal of Cybernetics 2 ( 3 ), 4 - 34 ( 1972 )