A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> We give the mathematical theory of a simple knowledge acquisition procedure based on implications and counter examples, and show examples of application. <s> BIB001 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> Computing the least common subsunier (les) is an inference task that can be used to support, the "bottom-up" construction of knowledge bases for KR systems based on description logics. Previous work on how to compute the lcs has concentrated on description logics that allow for universal value restrictions, but not for existential restrictions. The main new contribution of this paper is the treatment of description logics with existential restrictions. Our approach for computing the lcs is based on an appropriate representation of concept descriptions by certain trees, and a characterization of subsumption by homomorphisins between these trees. The lcs operation then corresponds to the product operation on trees. <s> BIB002 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> Computing the least common subsumer (lcs) has proved to be useful in a variety of different applications. Previous work on the lcs has concentrated on description logics that either allow for number restrictions or for existential restrictions. Many applications, however, require to combine these constructors. In this work, we present an lcs algorithm for the description logic ALEN, which allows for both constructors, thereby correcting previous algorithms proposed in the literature. <s> BIB003 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> RACER implements a TBox and ABox reasoner for the logic SHIQ. RACER was the first full-fledged ABox description logic system for a very expressive logic and is based on optimized sound and complete algorithms. RACER also implements a decision procedure for modal logic satisfiability problems (possibly with global axioms). <s> BIB004 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> In order to gain experience with description logic reasoner, and to contribute to the OWL Candidate Recommendation process, a small team at MINDSWAP set out to implement a tableau reasoner for the Lite and DL dialects of OWL (corresponding roughly to the description logics SHIF(D) and SHION(D)). Our group found existing, available DL reasoners lacking for our purposes, because we needed an open-source tool that provides ABox reasoning, that does not make Unique Name assumption, supports entailment checks and works with XML Schema datatypes. Pellet has been developed to addresses these issues and has become both our test bed for experiments with DL and Semantic Web reasoning, as well as our standard reasoning component. While not (yet) in the performance range of Racer or Fact, it has many usability features that makes it a good choice for various lighter weight situations. Technically, Pellet is a sound and complete tableau reasoners for SHIN(D) and SHON(D) (with ABoxes), and a sound but incomplete tableau reasoner for SHION(D) (with ABoxes). Pellet has the usual suite of optimizations including lazy unfolding, absorption, dependency directed backjumping, and semantic branching. It incorporates datatype reasoning for the built-in primitive XML Schema datatypes. Pellet is implemented in pure Java and available as open source software. <s> BIB005 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> Methods for computing the least common subsumer (lcs) are usually restricted to rather inexpressive Description Logics (DLs) whereas existing knowledge bases are written in very expressive DLs. In order to allow the user to re-use concepts defined in such terminologies and still support the definition of new concepts by computing the lcs, we extend the notion of the lcs of concept descriptions to the notion of the lcs w.r.t. a background terminology. We will both show a theoretical result on the existence of the least common subsumer in this setting, and describe a practical approach (based on a method from formal concept analysis) for computing good common subsumers, which may, however, not be the least ones. <s> BIB006 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> A well-known result is that the inference problem for propositional Horn formulae can be solved in linear time. We show that this remains true even in the presence of arbitrary (static) propositional background knowledge. Our main tool is the notion of a cumulated clause, a slight generalization of the usual clauses in Propositional Logic. We show that each propositional theory has a canonical irredundant base of cumulated clauses, and present an algorithm to compute this base. <s> BIB007 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> This is a system description of the Description Logic reasoner FaCT++. The reasoner implements a tableaux decision procedure for the well known SHOIQ description logic, with additional support for datatypes, including strings and integers. The system employs a wide range of performance enhancing optimisations, including both standard techniques (such as absorption and model merging) and newly developed ones (such as ordering heuristics and taxonomic classification). FaCT++ can, via the standard DIG interface, be used to provide reasoning services for ontology engineering tools supporting the OWL DL ontology language. <s> BIB008 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> We describe two algorithms for closure systems. The purpose of the first is to produce all closed sets of a given closure operator. The second constructs a minimal family of implications for the ”logic” of a closure system. These algorithms then are applied to problems in concept analysis: Determining all concepts of a given context and describing the dependencies between attributes. The problem of finding all concepts is equivalent, e.g., to finding all maximal complete bipartite subgraphs of a bipartite graph. <s> BIB009 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Supporting bottom-up construction of DL Ontologies <s> We present a novel reasoning calculus for the description logic SHOIQ+--a knowledge representation formalism with applications in areas such as the SemanticWeb. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce anywhere pairwise blocking. We also present an improved nominal introduction rule that ensures termination in the presence of nominals, inverse roles, and number restrictions--a combination of DL constructs that has proven notoriously difficult to handle. Our implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies. <s> BIB010
Traditionally, DL knowledge bases are built in a top-down manner, in the sense that first the relevant notions of the domain are formalized by concept descriptions, and then these concept descriptions are used to specify properties of the individuals occurring in the domain. However, this top-down approach is not always adequate. On the one hand, it might not always be intuitive which notions of the domain are the relevant ones for a particular application. On the other hand, even if this is intuitive, it might not always be easy to come up with a clear formal description of these notions, especially for a domain expert who is not an expert in knowledge engineering. In order to overcome this, in BIB002 a new approach, called "bottom-up approach", was introduced for constructing DL knowledge bases. In this approach, instead of directly defining a new concept, the domain expert introduces several typical examples as objects, which are then automatically generalized into a concept description by the system. This description is then offered to the domain expert as a possible candidate for a definition of the concept. The task of computing such a concept description can be split into two subtasks: -computing the most specific concepts of the given objects, -and then computing the least common subsumer of these concepts. The most specific concept (msc) of an object o is the most specific concept description C expressible in the given DL language that has o as an instance. The least common subsumer (lcs) of concept descriptions C 1 , . . . , C n is the most specific concept description C expressible in the given DL language that subsumes C 1 , . . . , C n . The problem of computing the lcs and (to a more limited extent) the msc has already been investigated in the literature BIB002 BIB003  . The methods for computing the least common subsumer are restricted to rather inexpressive descriptions logics not allowing for disjunction (and thus not allowing for full negation). In fact, for languages with disjunction, the lcs of a collection of concepts is just their disjunction, and nothing new can be learned from building it. In contrast, for languages without disjunction, the lcs extracts the "commonalities" of the given collection of concepts. Modern DL systems like FaCT++  BIB008 , Racer BIB004 , Pellet BIB005 , and Hermit BIB010 are based on very expressive DLs, and there exist large knowledge bases that use this expressive power and can be processed by these systems. In order to allow the user to re-use concepts defined in such existing knowledge bases and still support the user in defining new concepts with the bottom-up approach sketched above, in BIB006 BIB006 BIB006 we have proposed the following extended bottom-up approach: assume that there is a fixed background terminology defined in an expressive DL; e.g., a large ontology written by experts, which the user has bought from some ontology provider. The user then wants to extend this terminology in order to adapt it to the needs of a particular application domain. However, since the user is not a DL expert, he employs a less expressive DL and needs support through the bottom-up approach when building this user-specific extension of the background terminology. There are several reasons for the user to employ a restricted DL in this setting: first, such a restricted DL may be easier to comprehend and use for a non-expert; second, it may allow for a more intuitive graphical or frame-like user interface; third, to use the bottom-up approach, the lcs must exist and make sense, and it must be possible to compute it with reasonable effort. To make this more precise, consider a background terminology (TBox) T defined in an expressive DL L 2 . When defining new concepts, the user employs only a sublanguage L 1 of L 2 , for which computing the lcs makes sense. However, in addition to primitive concepts and roles, the concept descriptions written in the DL L 1 may also contain names of concepts defined in T . Let us call such concept descriptions L 1 (T )-concept descriptions. Given L 1 (T )-concept descriptions C 1 , . . . , C n , we want to compute their lcs in L 1 (T ), i.e., the least L 1 (T )-concept description that subsumes C 1 , . . . , C n w.r.t. T . In BIB006 BIB006 we have considered the case where L 1 is the DL ALE and L 2 is the DL ALC, and shown the following result: -If T is an acyclic ALC-TBox, then the lcs w.r.t. T of ALE(T )-concept descriptions always exists. Unfortunately, the proof of this result does not yield a practical algorithm. Due to this, in BIB006 BIB006  we have developed a more practical approach. Assume that L 1 is a DL for which least common subsumers (without background TBox) always exist. Given L 1 (T )-concept descriptions C 1 , . . . , C n , one can compute a common subsumer w.r.t. T by just ignoring T , i.e., by treating the defined names in C 1 , . . . , C n as primitive and computing the lcs of C 1 , . . . , C n in L 1 . However, the common subsumer obtained this way will usually be too general. In BIB006 BIB006  , work we presented a method for computing "good" common subsumers w.r.t. background TBoxes, which may not be the least common subsumers, but which are better than the common subsumers computed by ignoring the TBox. In the present work we do not give the gcs algorithm in detail. We only demonstrate it on an example. The algorithm is described in detail in BIB006 . By ignoring the TBox, we obtain the ALE(T )-concept description ∃has-child.⊤ as a common subsumer of C, D. However, if we take into account that both NoSon ⊓ DaughterHappyDoctor and NoDaughter ⊓ SonRichDoctor are subsumed by the concept ChildrenDoctor, then we obtain the more specific common subsumer ∃has-child.ChildrenDoctor. The gcs of C, D is even more specific. In fact, the least conjunction of (negated) concept names subsuming both NoSon ⊓ DaughterHappyDoctor and NoDaughter ⊓ SonRichDoctor is The conjunct ChildrenDoctor is actually redundant since it is implied by the remainder of the conjunction. ⋄ In order to implement the gcs algorithm, we must be able to compute the smallest conjunction of (negated) concept names that subsumes two such conjunctions C 1 and C 2 w.r.t. T . In principle, one can compute this smallest conjunction by testing, for every (negated) concept name whether it subsumes both C 1 and C 2 w.r.t. T , and then take the conjunction of those (negated) concept names for which the test was positive. However, this results in a large number of (possibly expensive) calls to the subsumption algorithm for L 2 w.r.t. (general or (a)cyclic) TBoxes. Since, in our application scenario (bottom-up construction of DL knowledge bases w.r.t. a given background terminology), the TBox T is assumed to be fixed, it makes sense to precompute this information. This is where FCA comes into play. By using the attribute exploration method BIB009 (possibly with background knowledge BIB001 BIB007 BIB007 ), we compute the abovementioned smallest conjunction, which is required for computing a gcs. To this purpose we define a formal context whose concept lattice is isomorphic to the subsumption hierarchy we are interested in. In general, the subsumption relation induces a partial order, and not a lattice structure on concepts. However, in the case of conjunctions of (negated) concept names, all infima exist, and thus also all suprema, i.e., this hierarchy is a complete lattice. The experimental results in BIB006 have shown that the use of this hierarchy and its use in gcs computation are indeed quite efficient.