Relational Exploration – Reconciling Plato and Aristotle⋆ Sebastian Rudolph Universitt Karlsruhe Institut AIFB rudolph@aifb.uni-karlsruhe.de Abstract. We provide an interactive method for knowledge acquisition combin- ing approaches from description logic and formal concept analysis. Based on present data, hypothetical rules are formulated and checked against a description logic theory. We propose an abstract framework (Logical Domain Exploration) for this kind of exploration technique before presenting a concrete instantiation: Relational Exploration. We give a completeness result and provide an overview about some application fields for our approach: machine learning, data mining, and ontology engineering. 1 Introduction A plethora of research fields is concerned with the question of finding specifications for a given domain. Research areas like machine learning, frequent pattern discovery, and data mining in general aim at extracting these description on the basis of (examplary or complete) data sets – following the Aristotelian paradigm, that every conceptualization has to start from entities actually present. Other approaches intend to deduce these specifications from pre-specified theories – being somehow more Platonic by assuming the primacy of abstract ideas. The latter is the usual modus operandi e.g. in description logic or theorem proving. We reconcile these two antagonistic approaches by combining techniques from two fields of knowledge representation: description logic (DL) and formal concept analysis (FCA). In our work, we use DL formalisms for defining FCA attributes and FCA explo- ration techniques to obtain or refine DL knowledge representation specifications. More generally, DL exploits FCA techniques for interactive knowledge acquisition and FCA benefits from DL in terms of expressing relational knowledge. In most cases, the process of conceptually specifying a domain cannot dispense of human contribution. However, although all information needed in order to describe a domain is in general implicitly present in an expert’s knowledge, the process of explicit formal specification may nevertheless be tedious and overstraining. Moreover, it might remain unclear whether a specification is complete, i.e., whether it covers all valid state- ments about the domain that can be expressed in the chosen specification language. ⋆ This work has been supported by the European Commission under contract IST-2006-027595 NeOn, and by the Deutsche Forschungsgemeinschaft (DFG) under the ReaSem project. Hence, we provide a method – called Relational Exploration (RE) – that organizes and structures the specification process by successively asking single questions to the domain expert in a way which minimizes the expert’s effort (in particular, it does not ask redundant questions) and guarantees that the resulting specification will be com- plete in the sense stated above. To present our work, which generalize the results from [1] and [2], we will proceed as follows: Section 2 provides a general framework for this kind of procedure, called Logical Domain Exploration. In Section 3, we shortly sketch the FCA basics necessary for our work and give an overview about attribute ex- ploration. Section 4 introduces the notions from description logics needed in this work. In Section 5, we establish the correspondence between DL models and certain formal contexts, which enables us to apply FCA to DL. In Section 6, the RE algorithm is de- scribed in detail. Section 7 shows certain completeness properties of the knowledge acquired via RE. Section 9 displays direction for further work. In Section 8, we discuss our results and consider in which fields the presented technique could be applied. 2 The Epistemic Framework: Logical Domain Exploration Before engaging into the technical details, we sketch the overall setting for our ap- proach, which helps conveying the underlying idea and identifying the contributing components. Doing this on an abstract level, we also give an opportunity to relate alter- native approaches. This framework will be called Logical Domain Exploration. Let ∆ be the considered domain of interest the elements of which we will call ( DOMAIN ) INDIVIDUALS. Let L be a language the elements of which are called FOR - MULAE . We write ∆ |= ϕ in order to state for a formula ϕ that it is valid in the domain. Moreover let the setting be well-behaved in the way that whenever ∆ |= ϕ is not true, there is a finite individual set Γ ⊆ ∆ witnessing this (we then write Γ † ϕ and say Γ SPOILS ϕ). – The EXPERT is supposed to be “omniscient” wrt. the described domain and thus able to answer any question about it. In particular, he knows for all ϕ ∈ L and Γ ⊆ ∆ whether ∆ |= ϕ and whether Γ † ϕ. Mostly, a human or a group of humans will take the role of the expert. – The TERMINOLOGY consists of a theory Th ⊆ LT about the domain consisting of axioms in some language LT ⊇ L and a reasoning functionality, i.e. for any statement ϕ ∈ LT it can be decided whether Th entails ϕ.1 – The DATA consists of a set of known or recorded individuals D ⊆ ∆ and is endowed with a special querying capability, i.e., a procedure providing for any ϕ ∈ L a set Γ ⊆ D with Γ † ϕ if there exists one. – The SCHEDULER can be conceived as an automated procedure initiating and co- ordinating the ”information flow”. It links the other system components by asking questions, processing answers, and assuring that in the end all knowledge is ac- quired to quickly decide for any ϕ ∈ L whether ∆ |= ϕ. 1 Hereby, entailment is as usual defined in a model-theoretic way: Th is said to entail ϕ if any domain ∆′ wherein all formulae of Th are valid also satisfies ∆′ |= ϕ. The system will operate as follows: We start with a (correct but in general incom- plete) terminological theory Th ⊂ {ψ ∈ LT | ∆ |= ψ} and data D ⊆ ∆. The scheduler now comes up with hypothetical formulae. Every such hypothetical formula ϕ ∈ L is passed both to the terminology and the data. The reasoning service of the terminology component checks whether ϕ is entailed by Th. The data is queried for a spoiler of ϕ. Since – due to the starting conditions – the theory is consistent with the data, we get three disjoint possible results: – ϕ is entailed by Th. In this case, ϕ is valid in ∆, which will be responded to the scheduler. – Γ ∈ D spoils ϕ. Then, ϕ is not valid in ∆ and the scheduler will be provided with this negative answer. – Neither of the previous cases occurs. Then, the current specification leaves room for either possibility and the domain expert will have to be asked this about ϕ’s validity in question. If he confirms the validity of ϕ in ∆, it will be added to Th. If he denies it, he has to provide a spoiler Γ for ϕ, which is then added to the data. Note that querying the data and questioning the terminology can be done in either order or even in parallel. After finishing the procedure every formula ϕ ∈ L will either be a consequence of the resulting (updated) terminology or can be excluded via a spoiler present in the data (updated) data. The distinction between L (the EXPLORATION LAN - GUAGE ) and LT (the TERMINOLOGICAL LANGUAGE ) is motivated by the assumption that in most cases not all terminologically expressible axioms will be of interest but only those of a certain shape. In the next chapters, we come down to an instance for the previously described framework for logical domain exploration: Relational Exploration. 3 Formal Concept Analysis In our instantiation, the scheduler’s task will be carried out by an extension of the at- tribute exploration algorithm well established in FCA. This necessitates to briefly intro- duce some basic FCA notions. We mainly follow the notation introduced in [3] being the reference for FCA theory. The basic notion FCA is built on is that of a formal context. It is a common claim in FCA that any kind of grounded data can be represented in this way. Definition 1. A FORMAL CONTEXT K is a triple (G, M, I) with an arbitrary set G (called OBJECTS), an arbitrary set M (called ATTRIBUTES), and a relation I ⊆ G×M (called INCIDENCE RELATION). We read gIm as: “object g has attribute m.” Further- more, let g I := {m | gIm}. The central means of expressing knowledge in FCA is via implications. Thus, in terms of the general framework from Section 2 the underlying language consists of implications on a fixed attribute set of atomic propositions. Definition 2. Let M be an arbitrary set. An IMPLICATION on M is a pair (A, B) with A, B ⊆ M . To support intuition, we write A  B instead of (A, B). A  B HOLDS in a formal context K = (G, M, I), if for all g ∈ G we have that A ⊆ g I implies B ⊆ g I . We then write K |= A  B. For C ⊆ M and a set I of implications on M , let C I denote the smallest set with C ⊆ C I that additionally fulfills A ⊆ CI implies B ⊆ CI for every implication A  B in I.2 If C = C I , we call C I- CLOSED. We say I ENTAILS A  B if B ⊆ AI .3 An implication set I will be called NON - REDUNDANT, if for any (A  B) ∈ I we have that B ⊆ AI\{AB} . An implication set I of a context K will be called COMPLETE, if every implication A  B holding in K is entailed by I. I will be called an IMPLICATION BASE of a formal context K if it is non-redundant and complete. Note that implication entailment is decidable in linear time ([4]). Therefore, know- ing a domain’s implication base allows fast handling of its whole implicational theory. Moreover, for every formal context, there exists a canonical implication base ([5]). The attribute exploration algorithm our work is based on was introduced in [6]. Due to space reasons, we omit to display it in detail and refer the reader to the literature. Essentially, the following happens: the domain to explore is formalized as a formal context K = (U, M, I). Usually, it is not known completely in advance. However, pos- sibly, some entities of the universe g ∈ U are already known, as well as their associated attributes g I . The algorithm now starts presenting questions of the form “Does the implication A  B hold in the context K = (U, M, I)?” to the human expert. The expert might confirm this. In this case, A  B is archived as part of K’s implicational base IB. The other case would be that A  B does not hold in (U, M, I). But then, there must exist a g ∈ U with A ∈ g I and B ∈ g I . The expert is asked to input this g and g I .4 The procedure terminates when the implicational knowledge of the universe is completely acquired, i.e., the implications of the formal context built from the entered counterexamples coincide with those entailed by IB. In the approach presented here, we will exploit the capability of attribute exploration to efficiently determine an implicational theory. Notwithstanding, we extend the under- lying language5 from purely propositional to certain DL expressions being introduced in the next section. 2 Note, that this is well-defined, since the mentioned properties are closed wrt. intersection. 3 Actually, this is a syntactic shortcut. Yet, it can be easily seen that this coincides with the usual entailment notion. 4 Referring to the general framework we mention that in this special case the spoiler (called counterexample) is always a singleton set: {g} † A  B. 5 There exist already other language extensions, e.g. to Horn-logic with a bounded variable set, see [7]. 4 Description Logic We recall basic notions from DL, following (and recommending for further reading) [8]. Unlike the way DL is normally conceived, we use DL expressions to describe or specify one particular, fixed domain. Thus, we will start our considerations by formally defining the kind of relational structure that we want to “talk about.” Definition 3. An INTERPRETATION for a set A of ( PRIMITIVE ) CLASS NAMES and a set R of ROLE NAMES is a pair I = (∆I , (.)I ) where ∆I is some set and (.)I is a function mapping class names to subsets of ∆I and role names to subsets of ∆I × ∆I . Verbally, for some primitive class name A, AI provides all members of that class and for some role name R, RI yields all ordered pairs “connected” by that role. The DL languages introduced here provide constructors for defining new concept descriptions out of the primitive ones. Table 1 shows those constructors, their interpre- tation (as usual defined recursively), and their availabilities in the description logics considered here. FLE ALE FL0 EL name interpretation A atomic concept AI ×××× ⊤ universal concept ∆I ×××× ⊥ bottom concept ∅ ×××× ¬A atomic negation ∆I \ A I × C ⊓ D conjunction CI ∩ DI ×××× ∀R.C value restriction {δ | ∀ǫ : (δ, ǫ) ∈ RI → ǫ ∈ CI } × × × ∃R.C existential quantification {δ | ∃ǫ : (δ, ǫ) ∈ RI ∧ ǫ ∈ CI } ××× Table 1. syntax and semantics of the DLs considered in this paper In the sequel, we will in general speak of a description logic DL if the presented result or definition refers to any DL ∈ {F L0 , EL, F LE, ALE}. Definition 4. Let I be an interpretation and C, D be DL concept descriptions. We say C IS SUBSUMED BY D in I (written: C ⊑I D) if CI ⊆ DI . This kind of subsumption statements is also called GENERAL CONCEPT INCLUSION AXIOM (GCI). Moreover, we say C and D are EQUIVALENT in I (written: C ≡I D) if CI = DI . 5 Subsumptions as Implications Combinations of FCA and DL have already been described in several publications, e.g. in [9], [10], and [11]. Our approach is motivated by [9] insofar as we use the same way of transferring a DL setting into a formal context by considering the domain individuals as objects and DL concept expressions as attributes. Definition 5. Given an interpretation I = (∆I , (.)I ) and a set M of DL concept descriptions, we define the corresponding DL- CONTEXT KI (M ) := (∆I , M, I) where δIC :⇐⇒ δ ∈ CI , for all δ ∈ ∆I and C ∈ M . The observation in the next theorem – though easy to see – is crucial for applying attribute exploration for the intended purpose. Theorem 1. Let I be an arbitrary interpretation and KI (M ) a corresponding DL- context. Then for finite C, D ⊆ M , the implication C D holds in KI (M ) if and only if 6   C ⊑I D. In the sequel, we will exploit this correspondence in the following way: employ- ing the FCA exploration method allows us to collect all information that is valid in a (not explicitly given) interpretation and can be expressed by DL subsumptions with restricted maximal role depth7 . 6 The Relational Exploration Algorithm The algorithm we present here is an iterative one. In each step the maximal role depth of the considered DL concept descriptions will be incremented by one. In each step, the results from previous steps will be exploited in several ways. In the worst case, the time needed for the attribute exploration algorithm is expo- nential with respect to the number of attributes. Thus, it is essential to see how the set of attributes can be reduced without losing completeness. The first exploration step is aimed at clarifying the implicational interdependencies of DL concept descriptions with quantifier depth 0. Therefore, no roles occur yet and we start with  {⊥} ∪ {A, ¬A | A ∈ A} if DL = ALE M0 := {⊥} ∪ A otherwise. In the actual exploration step – the interview-like procedure described in Section 3 – takes place with respect to the context KIi = KIi (Mi ). Every hypothetical implication A  B for A, B⊆ Mi presented  to the expert has to be interpreted as question about the validity of A ⊑I B, and will be passed to the “answering components” as described in Section 2. 6    We use {C1 , . . . , Cn } to abbreviate C1 ⊓. . .⊓Cn . Moreover, let {C} := C and {∅} := ⊤. 7 As usual, a concept description’s role depth indicates how deep quantifiers are nested in it. The exploration step ends up with an implication base IBi , which – as we will prove in Section 7 – represents the complete subsumptional knowledge of the consid- ered domain up to role depth i. For the next exploration step – incrementing the considered role depth – we have to stipulate the next attribute set Mi+1 . In case of the concept descriptions preceded by an existential quantification, the previously acquired implication base IBi can be used to reduce the number of attributes to consider, keeping the completeness property. Mi+1 := M0 ∪{∀R.C | R ∈ R, C ∈ Mi } ∪{∃R. C | R ∈ R, C = C IBi , ⊥ ∈ C} If considering EL or F L0 , simply discard the second resp. third line from the defi- nition. In addition to minimizing the cardinality of Mi+1 , we can accelerate the explo- ration process by providing implications on Mi+1 that are already known to be valid. These are the following: – {⊥}  Mi+1 , – {(A)i+1 | A ∈ A}  {(B)i+1 | B ∈ B} for every implication A  B from IBi (i.e., translate8 all known implications from Mi into Mi+1 ), – {∀R.A | A ∈ A}  {∀R.B | B ∈ B} for every implication A  B from IBi ,   – {∃R. A}  {∃R. B} for all IBi -closed sets A, B ⊆ Mi with A  B where there is no IBi -closed set C with A  C  B, and   – {∃R. A, ∀R.A}  {∃R. (A ∪ {A})IBi } for every IBi -closed set A ⊆ Mi \ {A} and every concept description A ∈ Mi . With this attribute set Mi+1 and the a-priori implications we start the next explo- ration step. In theory, this procedure can be continued to arbitrary role depths. In some but not in all cases a complete acquisition of knowledge can be achieved. Yet in practice, with increasing role depth, the questions brought up by the exploration procedure will be increasingly numerous as well as less intuitional and thus difficult to answer for a human expert. So in many cases, one will restrict to small role depths. 7 Verification of the Algorithm Let DLi denote the set of all DL concept descriptions with maximal role depth i. Now we show a way how the validity of any subsumption on DLi can be checked by us- ing just the attribute sets M0 , . . . , Mi as well as the corresponding implication bases IB0 , . . . , IBi on those sets. First, we will define functions that provide  for any concept description C ∈ DLi a set of attributes C ⊆ Mi such that C ≡I C. The following definitions and proofs are carried out for ALE but can be easily adapted to the other DLs by simply removing the irrelevant parts. 8 We will formally define and justify this translation (.)i+1 in Section 7. Definition 6. Let I be an interpretation and the corresponding sequences (Mi ), (KIi ) defined as above. Given the according sequence IB0 , . . . , IBn of implication bases, we define a sequence of functions τi : DLi → P(DLi ) in a recursive way: τi (C) = {C} for C ∈ M0   τi ( C) = {τi (C) | C ∈ C} τi (∀R.C) = {∀R.D | D ∈ τi−1 (C)} if ⊥ ∈ (τi−1 (C))IBi−1 ,  {⊥}  τi (∃R.C) = {∃R. (τi−1 (C))IBi−1 } otherwise. Moreover, let τ̄i (C) := (τi (C))IBi for all C ∈ DLi .  Note that by this definition, we also have τ̄i (⊤) = τ̄i ( ∅) = ∅IBi . Next, we have to show that the functions just defined behave in the desired way. The following lemma ensures that τ̄i and τi indeed map to Mi . Lemma 1. Suppose C ∈ DLi . Then we have τi (C) ⊆ Mi and τ̄i (C) ⊆ Mi . Proof. Obviously, τ̄i (C) ⊆ Mi whenever τi (C) ⊆ Mi . We show the latter by induction on the role depth considering four cases: – C ∈ {A, ¬A | A ∈ A} ∪ {⊥}. Then by definition C ∈ Mi . – C = ∃R.D. If ⊥ ∈ τ̄i−1 (D), we get τi (C) = τi (∃R.D) = {⊥} ⊆ Mi . Now suppose ⊥ ∈ τ̄i−1 (D). As immediate consequence of the induction hypothesis  τ̄i−1 (D) ⊆ Mi−1 . Since τ̄i−1 gives an IBi−1 -closed set, we have also we have ∃R. τ̄i−1 (D) ∈ Mi , as a look to the constructive  definition of Mi immediately shows. Therefore, τi (C) = τi (∃R.D) = {∃R. τ̄i−1 (D)} ⊆ Mi – C = ∀R.D. Again, our induction hypothesis yields τi−1 (D) ⊆ Mi−1 which implies {∀R.E | E ∈ τi−1 (D)} ⊆ Mi due to the definition of Mi and therefore also τi (C)= τi (∀R.D) = {∀R.E | E ∈ τi−1 (D)} ⊆ Mi . – C = C. W.l.o.g., we presuppose that there is no conjunction outside the quantifier range in any D ∈ C. So we have  τi (D)  ⊆ Mi due to thethree cases above, and subsequently also τi (C) = τi ( C) = {τi (D) | C ∈ C} ⊆ Mi . 2 The next lemma and theorem show that in our fixed interpretation I, for any concept description C ∈ DLi , the entity sets fulfilling C on the one hand and τ̄i (C) as well as τi (C) on the other hand coincide.   Lemma 2. For any C ⊆ Mi , we have C ≡I C IBi .  Proof. First, observe ( C)I = {(C)I | C ∈ C} = {CIi | C ∈ C} = {δ ∈ ∆I |   δ ∈ CI for all C ∈ C}. Now, consider KIi . Since IBi is an implication base of KIi , C  C IBi is an implication valid in KIi , ergo all objects of KIi (being the individuals δ ∈ ∆I ) fulfill C ⊆ δ Ii ⇒ C IBi ⊆ δ Ii . Therefore, one δ has all attributes from C exactly if it has all attributes IBi  I from CIBi . Finally,  IB we have then {δ ∈ ∆I | δ ∈ I C for all C ∈ C IBi } = {C | C ∈ C } = ( C i )I . 2   Theorem 2. Let C ∈ DLi . Then C ≡I τi (C) ≡I τ̄i (C). Proof. The second equivalence is a direct consequence of Lemma 2. We show the first one again via induction on the role depth:  – C ∈ {A, ¬A | A ∈ A} ∪ {⊥}. Then, we trivially have CI  = ( {C})I . – C = ∃R.D. By  induction hypothesis, we get DI = ( τ̄i−1 (D))I , therefore (∃R.D) = (∃R. τ̄i−1 (D))I which by definition equals ( τi (∃R. I I  D̃)) . I I – C = ∀R.D. Again, by induction hypothesis, we get D = ( τ̄i−1 (D)) = {EI | E ∈ τ̄i−1 I (D)}. Now, observe that the statement (δ, δ̃) ∈ R → δ̃ ∈ D I is equivalent to E∈τi−1 (D) (δ, δ̃) ∈ RI → δ̃ ∈ EI and thus (∀R.D)I = {δ | (δ, δ̃) ∈ RI → δ̃ ∈ {DI }} = {δ | E∈τi−1 (D) δ ∈ (∀R.E)I } =    {(∀R.E)I| E ∈ τi−1 (D)} = ( {∀R.E | E ∈ τi−1 (D)})I which by defini-  tion isjust ( τi (∀R.D))I . – C = C. Again, wecan presume  no conjunction outside the  quantifier range in any D ∈ C. Then ( C)I = {(D)I | D ∈ C} = {( τi (D))I |D ∈ C} I because of the cases shown  theI same as {(E) |  before. Now, this isI obviously E ∈ τi (D), D ∈ C} = ( ( {τi (D) | D ∈ C})) = (τi ( C)) . 2 Using these propositions, we can easily provide a method to check – using only the closure operators IB0 , . . . , IBi – the validity of any subsumption on DLi with respect to a fixed (but not explicitly known) interpretation I. It suffices to apply τ̄i on both sides and then check for inclusion. Corollary 1. Let C1 , C2 ∈ DLi . Then C1 ⊑I C2 if and only if τ̄i (C2 ) ⊆ τ̄i (C1 ).   Proof. Due to Theorem 2, C1 ⊑I C2 is equivalent to τ̄i (C1 ) ⊑I τ̄i (C2 ). Accord- ing to Lemma 1, we have τ̄i (C1 ) ⊆ Mi and τ̄i (C2 ) ⊆ Mi . In view of Theorem 1, this means the same as the validity of the implication τ̄i (C1 )  τ̄i (C2 ) in Ki . Now, since the application of τ̄ always gives a closed set with respect to all implications valid in Ki , this is equivalent to τ̄i (C2 ) ⊆ τ̄i (C1 ). 2 Finally, consider the function τi from Definition 6. It is easy to see that for any C ∈ Mi−1 by calculating τi (C) we get a singleton set {D} with D ∈ Mi . We then have even C ≡I D. For the sake of readability we will just write D = (C)i . Roughly spoken, D is just the “equivalent Mi -version” of C. Note that evaluating τi does not need the implication base IBi but only IB0 , . . . , IBi−1 . So we have provided the translation function we promised in Section 6. 8 Conclusion We have introduced an interactive knowledge acquisition technique for finding DL-style subsumption statements valid in a domain of interest. Its outstanding properties are – minimal workload for the domain expert (i.e., no redundant questions will be posed) and – completeness of the resulting specification (any statement from the exploration lan- guage is known to hold or not to hold). Several current fields of AI can benefit from the results presented here. Ontology engineering would be the first to mention. Since based on DL formalisms, our method can obviously contribute to the development and refinement of ontologies. RE can be used for an organized search for new GCIs9 of a certain shape (namely those expressible by DL concept descriptions). Clearly, the description logics nowaday’s on- tology specifications are based on are much more complex than any of DL. Nonethe- less, our algorithm is still applicable since all of them incorporate the DLs considered as exploration language candidates. Hence, any of the existent reasoning algorithms for deciding subsumption (as for instance KAON2 [12] or FaCT [13], both capable of rea- soning in SHIQ(D) – see [14]) can be used for the terminology part. All information beyond DL would then be treated as background knowledge and “hidden” from the exploration algorithm. As already pointed out, one major advantage of applying this technique is the guarantee that all valid axioms expressible as subsumption statements on DL with a certain role depth will certainly be found and specified. Another topic RE can contribute to is machine learning. The supervised case cor- responds almost directly to the RE algorithm – mostly one would have large data sets and (almost) empty theories in this setting. Yet also unsupervised machine learning can be carried out – by “short-circuiting” the expert such that every potential statement di- rected to him would be automatically confirmed. Essentially, the same would be the case for data mining tasks. Finally, we are confident that an implementation of the RE algorithm will be a very helpful and versatile tool for eliciting information from various knowledge resources. 9 Future Work So, as the very next step, we plan an implementation of the presented algorithm includ- ing interfaces for database querying as well as for DL reasoning. Applying this tool in the ontology engineering area will in turn enable us to investigate central questions concerning practical usability; in particular performance on real-life problems and scal- ability (being of unprecedented relevance in the Semantic Web Technologies sector), as well as issues concerning user acceptance will be of special interest for evaluation. References 1. Rudolph, S.: An FCA method for the extensional exploration of relational data. In Ganter, B., de Moor, A., eds.: Using Conceptual Structures, Contributions to ICCS 2003, Dresden, Germany, Shaker, Aachen (2003) 197 – 210 2. Rudolph, S.: Exploring relational structures via FLE. In Wolff, K.E., Pfeiffer, H.D., Del- ugach, H.S., eds.: Conceptual Structures at Work: 12th International Conference on Con- ceptual Structures. Volume 3127 of LNCS., Huntsville, AL, USA, Springer (2004) 196 – 212 9 I.e., GCIs not already logically entailed by the present specification. 3. Ganter, B., Wille, R.: Formal Concept Analysis: Mathematical Foundations. Springer-Verlag New York, Inc., Secaucus, NJ, USA (1997) Translator-C. Franzke. 4. Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of proposi- tional Horn formulae. J. Log. Program. 1 (1984) 267–284 5. Guigues, J.L., Duquenne, V.: Familles minimales d’implications informatives resultant d’un tableau de données binaires. Math. Sci Humaines 95 (1986) 5–18 6. Ganter, B.: Two basic algorithms in concept analysis. Technical Report 831, FB4, TH Darmstadt (1984) 7. Zickwolff, M.: Rule Exploration: First Order Logic in Formal Concept Analysis. PhD thesis, FB4, TH Darmstadt (1991) 8. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F., eds.: The Description Logic Handbook: Theory, Implementation, and Applications. In Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F., eds.: Description Logic Handbook, Cambridge University Press (2003) 9. Prediger, S.: Terminologische Merkmalslogik in der formalen Begriffsanalyse. In Stumme, G., Ganter, B., eds.: Begriffliche Wissensverarbeitung: Methoden und Anwendungen, Springer (2000) 99–124 10. Baader, F.: Computing a minimal representation of the subsumption lattice of all conjunc- tions of concepts defined in a terminology. In: Proceedings of the International Symposium on Knowledge Retrieval, Use, and Storage for Efficiency, KRUSE 95, Santa Cruz, USA (1995) 168–178 11. Baader, F., Sertkaya, B.: Applying formal concept analysis to description logics. In: ICFCA. (2004) 261–286 12. Motik, B.: Reasoning in Description Logics using Resolution and Deductive Databases. PhD thesis, Universität Karlsruhe (TH), Germany (2006) 13. Horrocks, I.: Using an expressive description logic: FaCT or fiction? In Cohn, A.G., Schu- bert, L., Shapiro, S.C., eds.: Principles of Knowledge Representation and Reasoning: Pro- ceedings of the Sixth International Conference (KR’98), Morgan Kaufmann Publishers, San Francisco, California (1998) 636–647 14. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for expressive description logics. In Ganzinger, H., McAllester, D., Voronkov, A., eds.: Proceedings of the 6th International Con- ference on Logic for Programming and Automated Reasoning (LPAR’99). Number 1705, Springer-Verlag (1999) 161–180