Introduction

Attribute exploration (cf. [3]) is a family of interactive procedures for Knowledge Acquisition (KA) in Formal Concept Analysis (FCA), whose goal is to build a knowledge base of the attributes we are working with. The procedures used in FCA have nice computer implementations, existing even generalizations for the management of the background information. Sometimes attribute exploration is hard or tedious to apply. Thus, it may advisable to use automated tools. Many Computer Algebra Systems (CAS) provide tools for working with discrete data, for example, Gröbner basis. Since it is possible to translate entailment problems into ideal problems in finite fields, Gröbner basis is a powerful tool for reasoning in propositional logic [8,9,2].

Our aim is to extend the framework of attribute exploration through the introduction of Boolean derivatives and the assistance of a CAS. The CAS that we will use CoCoA (http://cocoa.dima.unige.it/), very well suited for our pourposes because of its easy management of Gröbner basis and related tools. The paper is organized as follows. The next section reviews the relationship between propositional logic and the ring F 2 [x], as well as the basics of FCA. In the third section the Boolean derivatives are introduced, as well as a complete polynomial calculus based on them. An algebraic characterization of sensitivity for implications in FCA is given in forth section. In fifth and sixth sections new versions of attribute exploration are introduced, and in section 7 an application to graph theory is given. We conclude with some remarks about future work.

Background

We assume that the reader is familiar with propositional logic and polynomial algebra on positive characteristics. We setup a propositional language P V = {p 1 , . . . , p n }, P F orm will denote the set of propositional formulas, and var(F ) denotes the set of variables of the propositional formula F .

The ring in which we are working is F 2 [x] (where x = x 1 , . . . , x n ). A key ideal is I 2 := (x 1 + x 2 1 , . . . , x n + x 2 n ). To clarify our proposition, let fix an identification p i → x i (or p → x p ) between PV and the set of indeterminates.

Given α = (α 1 , . . . α n ) ∈ N n , let us define |α| := max{α 1 , . . . , α n }, and sg(α) := (δ 1 , . . . , δ n ), where δ i is 0 if α i = 0 and 1 otherwise. The degree of a(x) ∈

F 2 [x], is deg ∞ (a(x)) :=max{|α| : x α is a monomial of a}, and deg i (a(x)) is the degree w.r.t. x i . If deg ∞ (a(x)) ≤ 1, a(x) is called a polynomial formula.

Three maps represent the relationship between propositional logic and F 2 [x]:

-Φ : F 2 [x] → F 2 [x] is defined by Φ( α∈I x α ) := α∈I x sg(α) .

-The map P : P F orm → F 2 [x] is defined by the following equations

• P (⊥) = 0, P (p i ) = x i , P (¬F ) = 1 + P (F ) • P (F 1 ∧F 2 ) = P (F 1 )•P (F 2 ) and P (F 1 ∨F 2 ) = P (F 1 )+P (F 2 )+P (F 1 )P (F 2 ) • P (F 1 → F 2 ) = 1 + P (F 1 ) + P (F 1 )P (F 2 )

, and

• P (F 1 ↔ F 2 ) = 1 + P (F 1 ) + P (F 2 ) -Θ : F 2 [x] → P F orm is defined by • Θ(0) = ⊥, Θ(1) = , Θ(x i ) = p i , • Θ(a • b) = Θ(a) ∧ Θ(b), and Θ(a + b) = ¬(Θ(a) ↔ Θ(b)).

We have that Θ(P (F )) ≡ F and P (Θ(a)) = a. Since we shall frequently be applying Φ • P , we define the polynomial projection as π := Φ • P . Regarding valuations and polynomials, the key fact is that, if v : P V → {0, 1} is a valutation with v(p i ) = δ i , then for every

F ∈ P F orm, v(F ) = P (F )(δ 1 , . . . δ n )

The behaviour of the ideals of F 2 [x] is well known: If A ⊆ (F 2 ) n , then V (I(A)) = A, and for every I ∈ Ideals(F 2 [x]), I(V (I)) = I + I 2 . Therefore F ≡ F if and only if P (F ) = P (F ) (mod I 2 ) which is also equivalent to Φ • P (F ) = Φ • P (F ). The following theorem states the main relationship between propositional logic and F 2 [x]: Theorem 1. The following conditions are equivalent:

(1) {F 1 , . . . , F m } |= G. (2) 1 + P (G) ∈ (1 + P (F 1 ), . . . , 1 + P (F n )) + I 2 . (3) NF(1 + P (G), GB [(1 + P (F 1 ), . . . , 1 + P (F m )) + I 2 ]) = 0.

(where GB denotes Gröbner basis) and NF denotes normal form.

In the rest of this section we succintly present some elements of FCA we use, although we assume that the reader knows the basic principles of this theory (the fundamental reference is [3]). We represent a formal context as M = (O, A, I), which consists of two sets, O (the objects) and A (the attributes) and a relation I ⊆ O × A. Finite contexts can be represented by a 1-0-table (representing I as a Boolean function on O × A). The main goal in FCA is the computation of the concept lattice associated to the context. Basic logical expressions in FCA are implication between attributes, that is, pair of sets of attributes written as Y 1 → Y 2 . Truth with respect to M = (O, A, I) is defined as follows. A subset

T ⊆ A respects Y 1 → Y 2 if Y 1 ⊆ T or Y 2 ⊆ T . We say that Y 1 → Y 2 holds in M (M |= Y 1 → Y 2 ) if for all o ∈ O, the set {o} respects Y 1 → Y 2 . In that case we say that Y 1 → Y 2 is an implication of M .

From a propositional logic viewpoint, Y 1 → Y 2 is the formula Y 1 → Y 2 , so it is equivalent to a set of Horn clauses (implications with a singleton as right-hand side). On the other hand, the definition of truth can be extended: Given Y ⊆ A, define ¬Y := Y → ⊥, and it holds in the context if for all o ∈ O, Y ⊆ {o} . Given a formula written with {→, ⊥}, M |= F can be defined in the natural way. Since this set of connectives is functionally complete, truth definition can be extended to P F orm. Definition 1. Let L be a set of implications and L an implication of M .

• L follows from L (L |= L) if each subset of A respecting L also respects L. • L is closed if every implication following from L is already in L. • L is complete if every implication of the context follows from L. • L is non-redundant if for each L ∈ L, L \ {L} |= L.

• L is a stem basis for M if it is complete and non-redundant.

For every context we can obtain a stem basis from the pseudo-intents:

Theorem 2. [7] The set L = {Y → Y : Y is a pseudointent} is a stem basis.

Actually one can choose Y → Y \ Y instead of Y → Y , so we will assume, by default, that for every implication Y 1 → Y 2 belonging to a stem basis Y 1 and Y 2 are disjoint. Such a basis for the example of figure 5

(left) is L = {∅ → N, {N, A} → {M o}, {N, Le} → {M o}}.

The called Amstrong rules facilitates implicational reasoning:

R1 : X → X R2 : X → Y X ∪ Z → Y R3 : X → Y, Y ∪ Z → W X ∪ Z → W It has that A:= (H, A, I ∩ (H × A))

One expects that a stem basis associated to M H is also a stem basis for the complete context. To guarantee it, we proceed as follows. Assume that L =

1. Compute pseudo-intent: Find X a pseudo-intent for M H . 2. Soundness of the new implication: Ask to the user X ? → X (the operators are w.r.t. the subcontext). The user must react:

-Confirming the suggested implication (adding it to L), or giving o (a counterexample) such that {o} does not respect the implication. This is added to H, and the implication is discarded.

Fig. 1. Attribute exploration {L 1 , . . . , L k } is a partial set of implications accepted as true, built from pseudo- intents of M H 1 .

Attribute exploration consists in a loop of the two steps shown in fig. 1, and it stops when no new pseudointent is found (see [4] for variants).

Boolean derivatives and non-clausal theorem proving

We introduce an operator on propositional formulas as a translation of the usual derivation on F 2 [x]. In this section we review its basic properties (from [2]).

Recall that a derivation on a ring R is a map

d : R → R verifying that d(a + b) = d(a) + d(b) and d(a • b) = d(a) • b + a • d(b) Definition 2. A map ∂ : P F orm → P F orm is a Boolean derivation if there exists a derivation d on the ring F 2 [x] such that ∂ = Θ • d • π If the derivation on F 2 [x] is d = ∂ ∂xp , we denote ∂ as ∂ ∂p .

It has that:

∂ ∂p F ≡ ¬(F {p/¬p} ↔ F )

Thus, the value of ∂ ∂p F with respect to a valuation does not depend on p. Therefore, we can apply valuations on P V \ {p} to this formula. Definition 3. The independence rule (or ∂-rule) on polynomial formulas is

∂ x (a 1 , a 2 ) : a 1 , a 2 1 + Φ (1 + a 1 • a 2 )(1 + a 1 • ∂ ∂x a 2 + a 2 • ∂ ∂x a 1 + ∂ ∂x a 1 • ∂ ∂x a 2 ) In order to simplify the notation, if a i = b i + x p • c i , with deg xp (b i ) = deg xp (c i ) = 0 (i = 1, 2),.

Then we can rewrite the values as:

∂ xp (a 1 , a 2 ) : b 1 + x p • c 1 , b 2 + x p • c 2 Φ [1 + (1 + b 1 • b 2 )[1 + (b 1 + c 1 )(b 2 + c 2 )]]

The rule is symmetric and generalizes resolution of non-tautological polynomial clauses (see lemma 1). For formulas the rule is translated as

∂ p (F 1 , F 2 ) := Θ(∂ xp (π(F 1 ), π(F 2 ))).

It naturally induces a concept of proof, ∂ . A ∂ -refutation is a proof of ⊥. In [2] the soundness and the refutational completeness of partial has been proved Theorem 4. [2] Let v : P V \ {p} → {0, 1}. The following conditions are equivalent:

1. v |= ∂ p (F 1 , F 2 ). 2. There exists an extension of v to P V is a model of {F 1 , F 2 }. For example, ∂ x1 (x 1 (1 + x 2 ), x 1 (1 + x 2 )) = 1 + x 2 . So the valuation v s.t. v(¬p 2 ) = 1 is the only one that we can extend to a model of p 1 ∧ ¬p 2 . When ∂ p (π(F 1 ), π(F 2 )) = 1, every partial valuation is extendable to a model of {F 1 , F 2 }. Theorem 5. [2] If Γ is inconsistent then Γ ∂ ⊥. Let be ∂ p [Γ ] defined as ∂ p [Γ ] := {∂ p (F, G) : F, G ∈ Γ }. Given Q = {q 1 , . . . , q k } ⊆ P V the operator ∂ Q := ∂ q1 •• • ••∂ q k is

well defined modulo logical equivalence (by corollary 4, for every p, q ∈ P V ,

∂ p • ∂ q [Γ ] ≡ ∂ q • ∂ p [Γ ]

). A consequence of corollary 4 and theorem 5 is that entailment can be located on variables of the goal;

Corollary 1. Γ |= F ⇐⇒ ∂ P V \var(F ) [Γ ] |= F

We can define an explicit equivalent expression for ∂ p when it is applied to implications. To simplify, suppose that the right-side of implications is a singleton.

Lemma 1. Let C i ≡ Y i 1 → Y i 2 be a implications (i = 1, 2, Y i 1 ∩ Y j 2 = ∅), and Γ be a set of implications. Let ∂ c p (C 1 , C 2 ) be the symmetric operator ∂ c p (C 1 , C 2 ) :=            {C 1 , C 2 } p / ∈ var(C 1 ) ∪ var(C 2 ) {C 2 } p ∈ Y 1 1 , p / ∈ var(C 2 ) { Y 1 1 → (Y 1 2 \ {p}), C 2 } p ∈ Y 1 2 , p / ∈ var(C 2 ) { } p ∈ (Y 1 1 ∩ Y 2 1 ) ∪ (Y 1 2 ∩ Y 2 2 ) {Resolvent p (C 1 , C 2 )} p ∈ Y 1 1 ∩ Y 2 2 If ∂ c p [Γ ] := {∂ c p (C 1 , C 2 ) : C 1 , C 2 ∈ Γ }, then ∂ c Q [Γ ] ≡ ∂ Q [Γ ] (Q ⊆ P V ).

Algebraic characterization of sensitive implications

We shall provide an algebraic treatment for implications on a fixed M = (O, A, I).

It is well know that every set X ⊆ (F 2 ) n is an algebraic set; that is, there exists

a X ∈ F 2 [x] such that V (a X ) = X. If |A| = n, M is identified with a sub- set X(M ) of (F 2 ) n (each object identified with the 1-0 expresion of its intent). Let a M ∈ F 2 [x] denote a polynomial formula such that V (a M ) = X(M ). Since IV (a M ) = (a M ) + I 2 , the coordinate ring of M is F 2 [x]/ I(X(M )) ∼ = (F 2 [x]/ (a M ) )/ I2

One might also use an ideal J X such that V (J X ) = X, if it is better to work with them (for example using CoCoA's command IdealsofPoints). Thus we can assume that I 2 ⊆ J M . We choose a M only to simplify the proofs. Also, each o ∈ O defines a valuation v o defined by: v o (p i ) = 1 iff oIp i .

Proposition 1. Let F ∈ P F orm and let L be a stem basis. The following conditions are equivalent:

(1) M |= F.

(

) 1 + π(F ) ∈ (a M ) + I 2 .2

Moreover, if F is an implication, they are also equivalent to (3) {P (L) :

L ∈ L} ∪ {1 + π(F )} ∂ 0. (4) ∂ c P V \var(F ) [L] |= F Proof (1) ⇐⇒ (2): If M |= F , then V (a M ) ⊆ V (1 + π(F )). Thus, IV (1 + π(F )) ⊆ IV (a M ) hence 1 + π(F ) ∈ (a M ) + I 2 .

The converse is similar. If F is an implication and M |= F , then L |= F . Therefore L ∪ {¬F } is inconsistent so by completeness, L ∪ {¬F } ∂ ⊥ hence we have (3). The converse is true by soundness. ( 4) is equivalent to L |= F by lemma 1.

We now deal with the problem of redundant arguments in implications. In the worst case, the recognizing of redundancy requires a complete exploration of intents. An argument is redundant if it is not sensitive:

Definition 4. A formula F is sensitive in p w.r.t. a formal context M if M |= F {p/¬p} ↔ F . We say that F is sensitive w.r.t. M (or simply sensitive, if M is fixed) if F is sensitive in all its variables. Thus, F is not sensitive in p iff M |= ¬ ∂ ∂p F . In this case, there exists G with var(G) =var(F ) \ {p} such that M |= F ↔ G (e.g. F {p/⊥}).

Sensitive implications (also called proper implications) have several advantages over implications obtained from pseudo-intents (see [10]). In attribute exploration, sensitivity analysis is justified: it is possible that implications are based on a nonrepresentative set of examples, and thus they can be refined, basically giving witnesses of the role of the arguments in the implication, or making them more precise, removing redundant arguments:

Lemma 2. Let L = Y 1 → Y 2 be an implication. If M |= L and L is not sensitive in p ∈ Y 1 , then M |= Y 1 \ {p} → Y 2 . If p ∈ Y 2 , then M |= ¬Y 1 .

By default, sensitivity analysis for implications will be always restricted to attributes in the left-hand side.

v o |= ∂ ∂p F , so V (a M ) ⊆ V (π( ∂ ∂p F )) = V ( ∂ ∂xp π(F )), hence ∂ ∂xp π(F ) / ∈ (a M ) + I 2 .

(2) =⇒ (1):

If ∂ ∂xp π(F ) / ∈ (a M ) + I 2 , then O = V (a M ) ⊆ V (π( ∂ ∂p F )). Therefore there exists o ∈ O such that v o |= ∂ ∂p F . Thus F is sensitive in p.

(3) Sensitivity test: If the implication has not been discarded, test whether the implication is sensitive in all its arguments w. r. t. the actual set H (using lemma 2 if necessary). If it is not sensitive in some of them, the user must to react: -Adding a new example o to H, witness of the sensitivity (that is, he/she thinks that it is sensitive), or eliminating the attribute of the implication (it accepts it is not sensitive), changing the accepted implication by the refined one.

Fig. 2. Sensitivity test to add to algorithm of fig. 1 One can recursively apply the above criteria (w.r.t. an order on P V ) to obtain sensitive implications. If L is a stem basis and L is the refinement obtained, since Amstrong's rule R2 states

Y 1 \ {Y } → Y 2 |= Y 1 → Y 2 , one has that L |= L.

Thus L is also a complete set of implications. The set L has an advantage over other sets of proper implications (e.g. [10]) that it directly works on Duquenne-Guigues basis so it does not need an specific algorithm to build it.

Variants of attribute exploration

We shall propose new steps for attribute exploration. All of them are investigated with the translation into polynomials in mind. Although in the exposition we do not explicitely use polynomials -the results and their proofs are more readable in logical form-in practice they will be useful.

The attribute exploration can be extended by adding a sensitivity test w.r.t H (shown in fig. 2). Note that addition of a new object follows the formula a H∪{(δ1,...,δn)} = Φ(a H • (1 + Π n i=1 (x i + δ i + 1)))

For the running example, the implication N ∧ A → M o is obtained and considered as sound. In this case,

a M = x 1 x 2 x 4 + x 1 x 2 + x 1 x 3 + x 1 x 4 + x 1 + 1. A Gröbner basis for a M + I 2 is {x 2 4 + x 4 , x 2 3 + x 3 , x 4 2 + x 2 , x 3 x 4 + x 3 , x 2 x 4 + x 2 + x 3 + x 4 , x 2 x 3 + x 2 , x 1 + 1} It verifies (with CoCoA) that ∂ ∂x1 π(N ∧ A → M o) = x 2 (1 + x 3 ) ∈ (a M ) + I 2

We think that is not really sensitive in N (every live being needs water), so we accept A → M o, which is now sensitive. Reasoning similarly with the other one, it obtains {N, A → M o, L → M o}, a stem basis of sensitive implications.

Sensitivity test can be also added when background knowledge exists. In this case, we deal with hard problems as consistency checking or entailment. It starts with H and a background knowledge Γ for M H , that is, M H |= Γ . Or, in algebraic terms, V (a H ) ⊆ V ({1 + π(F ) : F ∈ Γ }). The step to add is in given figure 3. Condition ( * ) means

1 + ∂ ∂x p π(L) / ∈ ({1 + π(F ) : F ∈ Γ }) + I 2

(3) Sensitivity test: Test whether the implication is sensitive in all its arguments with the actual set H and the background knowledge Γ , that is, whether for each attribute p in the antecedent of L Γ |= L ↔ L{p/¬p} ( * ) If it is not sensitive in some of them, the user must to react:

-Giving o ∈ O, a witness of the sensitivity (which is added to H), that is

vo |= { ∂ ∂p L} ∪ Γ ( * * )

-or else removing the attribute of the implication (he/she accepts it is not sensitive).

Fig. 3. Sensitivity test with background knowledge

Regarding to the existence of an object for ( * * ), if the user does not know one, but believes that it really exists, a model search program may be used to give an anonymous object. Test ( * * ) can be fairly translated into algebraic terms.

Attribute exploration with new attributes

Now we propose how to extend the context by adding new attributes. Formally, one starts with M 0 , a subcontext with partial set of attributes,

M 0 = (H, A 0 , I ∩ (H × A 0 )), with A 0 A

Assume that, at some stage, full extents for a set H of objects are introduced, with the aim of expanding the new attributes to initial objects of M 0 (see fig. 5). The user only knows -about the new attributes-a background knowledge Γ , relating old and new attributes. Since it seems not advisable to add many arguments at once (to facilitate the answers of tests), Γ will be relatively small. It is important to observe that ∆ = L ∪ Γ , where L is the partial set of implications, may be inconsistent with ontological commitments implicitely or unconsciously accepted for the old attributes; that is, it may be false for M 0 , whenever the extents of H were expanded to the full attribute set. Thus one needs an expandability test for objects of H (to simplify assume that the new attributes are {p k+1 , . . . , p n }):

For each o ≡ (δ 1 , . . . , δ k ) of H, is there (δ k+1 , . . . δ n ) ∈ {0, 1} n−k such that {p j : δ j = 1 ∧ j ∈ {1, . . . , n}} respects ∆?

Theorem 6. Let M be an expansion of M 0 to the complete attribute set, with the same set of objects. If Γ is a stem basis (respectively a background knowledge) for M , then ∂ c {p k+1 ,...,pn} [Γ ] is a complete set of implications (respectively ∂ {p k+1 ,...,pn} [Γ ] is a background knowledge) for M 0 .

Proof. Assume that Γ is a stem basis. Let L be an implication in the language A \ {p k+1 , . . . , p n }.

If M |= L, then Γ |= L. By corollary 1, ∂ p [Γ ] |= L so by lemma 1, ∂ c p [Γ ] |= L holds.

If Γ is a background knowledge, the result is a straightforward consequence of corollary 1.

(3) Expansion test: If implication has not been discarded, test whether the set of implications plus background knowledge is extendable to H.

-If it is extendable, the user shall proceed:

• Confirming the suggested implication, or • giving o ∈ O such that {o} does not respect the implication. This is added to H , and the implication is discarded. -Else, it must revise the background knowledge, or to discard the implication Leech

1 1 1 0 Frog 1 1 1 1 Maize 1 0 0 0 Fish 1 1 1 0

Need water Aquatic Mobility Legs Land Cat

1 0 1 1 ? Leech 1 1 1 0 ? Frog 1 1 1 1 ?

Maize

1 0 0 0 ? Fish 1 1 1 0 0 Dog 1 0 1 1 1

Bean

1 0 0 0 1

Fig. 5. Extension of the context on live beings with new attributes

Corollary 2. Let ∆ ⊆ P F orm. The following conditions are equivalent:

(1) Every extension of objects of H can be expanded to the full attribute set, consistently with ∆.

(

) {1 + π(F ) : F ∈ ∂ {p k+1 ,...,pn} [∆]} ⊆ (a H ) + I 22

Assume now that it has previously certified that ∆ is expandable to objects of H, and let L be a new implication. If ∆ ∪ {L} can be consistently extended to H, but the user thinks that it is not true, in a first stage the user is required to give a counterexample for L by completing the extention of some object of H (in this way it bounds the set of new examples), or, if he/she does not know which, a new example. Summarizing, the new step is shown in figure 4.

For example, suppose that we decide to add a new attribute, to live in land (La). Some complete extensions are given (figure 5). We only know as background knowledge that aquatic live beings do not live in land, and we consider the implication every live being with legs and mobility lives in land, that is

∆ = {A → ¬La, Le ∧ M o → La} In this case, π[∆] = {1 + x A x La , 1 + x Le x M o + x Le x M o x La }.

The set H can not be consistently expanded to a model of ∆, because

∂ {x La } [π[∆]] = {1 + x A + x A x Le x M , 1} and x A + x A x Le x M / ∈ (a H ) + I 2 .

A final remark: defining the new attributes

We now see how to extend the above procedure for learning the new attribute. We suppose we have a stem basis consistent with old information; and, in a second stage, we wish to find a definition of the new attribute w.r.t the old ones (if the user thinks it is possible). The next theorem states a solution, which is an adaptation of predicate completion procedure (sect. 6.2 in [5]). That is, we are considering the stem basis is a complete knowledge base for the attribute.

An application: discovering tree notion in graph theory

We shall investigate the relationship among several properties on graphs (with three or more nodes), comparing stem basis produced by classical attribute exploration with the result of the new methods. The properties are: acyclic, connected, 2-connected (if one edge of the graph is removed, the induced subgraph is connected), geodetic (for every two nodes there exists only one shortest path), bipartite (it can be partionated the set of nodes in two sets such that every edge joins a node of each set), nonseparable (connected and, if one removes a node, the resulting graph remains connected), and planar.

We begun (classical) attribute exploration with the two first objects of figure 6 (left). For this we used ConExp, and the result is the formal context of fig. 6 (left. K 5 is the complete graph with five nodes, and K 33 is the complete bipartite graph with two sets of tree nodes each one as partition). The stem basis is:

L 1 : t → a, b, c, g, p L 2 : n → c, d L 3 : g → c L 4 : d → c L 5 : b, c, g, p → a, t L 6 : b, c, d, g → n L 7 : a → b, p L 8 : a, c, b, p → g, t

One might apply completion procedure on tree, obtaining a (messy) definition,

(Bipartite ∧ Connected ∧ Geodetic ∧ Planar) ∨ (Acyclic ∧ Connected ∧ Bipar- tite ∧ Planar)

Even it is not evident that the first conjuction defines a tree; it is necessary to know the fact that every geodetic and bipartite graph is acyclic. For this context, the ideal generated is

J M = (g + b + t + 1, c + d + t, a + d + 1, t 2 + t, pt + t, nt, bt + t, dt, p 2 + p, np + n + p + 1, dp + d + p + 1, n 2 + n, dn + n, b 2 + b, db + d + b + 1, d 2 + d).

The first interesting sensitivity analysis is on L 5 (π(L 5 ) = 1 + bcgp(1 + at)): T ree ↔ (Bipartite ∧ Geodetic) ∨ (Acyclic ∧ Connected) It easy to see that the first conjunction is equivalent to the second one, the original definition of tree.

Our next aim is to expand our set of attributes with a new one, radiusminimal (denoted as variable by r). The distance of two nodes of a graph is the length of a shortest path between them. The eccentricity of a node v is the distance to a node farthest from v. The radius of a graph G, r(G), is the minimum eccentricity of the nodes. Finally, a graph is called radius-minimal if r(G − e) > r(G) for every edge in G. We used the method shown in section 6; the objects of fig. 6 suffices for it.

The exploration starts with the first two objects of figure 6, knowing that the first one is radius-minimal and the second one is not. Also we have the background knowledge {¬c → ¬r}. The procedure gives the basis The last two conjunctions are equivalent to Tree, so we conclude that Radiusminimal and Tree are equivalent. Actually, this result is proved in [6]. Thus we take v o (r) := t to extend the attribute r for objects.

Conclusions and Future work

We present a framework for solving problems of FCA with the assistance of a CAS. We are confident that the tools described here may be useful to facilitate knowledge processing. As mentioned in previous sections, the complexity of some subproblems involved in the improvements of attribute exploration may restrict the method to projects of modest size, if a CAS as CoCoA is not used.

Throughout the paper we remarked some works related with the tools used here. The future work is the extension to many-valued logics and their applications [9].