A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Description Logics <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> BIB001 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Description Logics <s> Description logics are embodied in several knowledge-based systems and are used to develop various real-life applications. Now in paperback, The Description Logic Handbook provides a thorough account of the subject, covering all aspects of research in this field, namely: theory, implementation, and applications. Its appeal will be broad, ranging from more theoretically oriented readers, to those with more practically oriented interests who need a sound and modern understanding of knowledge representation systems based on description logics. As well as general revision throughout the book, this new edition presents a new chapter on ontology languages for the semantic web, an area of great importance for the future development of the web. In sum, the book will serve as a unique resource for the subject, and can also be used for self-study or as a reference for knowledge representation and artificial intelligence courses. <s> BIB002 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Description Logics <s> Abstract The OWL Web Ontology Language is a new formal language for representing ontologies in the Semantic Web. OWL has features from several families of representation languages, including primarily Description Logics and frames. OWL also shares many characteristics with RDF, the W3C base of the Semantic Web. In this paper, we discuss how the philosophy and features of OWL can be traced back to these older formalisms, with modifications driven by several other constraints on OWL. Several interesting problems have arisen where these influences on OWL have clashed. <s> BIB003 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Description Logics <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> BIB004 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Description Logics <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> BIB005 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Description Logics <s> Color evaluation of a color sample is effected by producing in a simultaneous field of vision a plurality of separate color comparison regions each differing in color slightly from one another and juxtaposed with a multiplicity of images of a single small area of a color sample. The color of the sample images can be compared simultaneously with the colors of the comparison regions and a color attribute of the comparison regions varied until visual correspondence is obtained between the sample color and one of the comparison regions. <s> BIB006 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Description Logics <s> CEL (Classifier for ${\mathcal{E}{L}}$) is a reasoner for the small description logic ${\mathcal{E}{L}}^+$ which can be used to compute the subsumption hierarchy induced by ${\mathcal{E}{L}}^+$ ontologies. The most distinguishing feature of CEL is that, unlike all other modern DL reasoners, it is based on a polynomial-time subsumption algorithm, which allows it to process very large ontologies in reasonable time. In spite of its restricted expressive power, ${\mathcal{E}{L}}^+$ is well-suited for formulating life science ontologies. <s> BIB007 </s> A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis <s> Description Logics <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> BIB008
Description Logics (DLs) BIB002 are a class of knowledge representation formalisms that are used to represent the terminological knowledge of an application domain in a structured way. Since their introduction, DLs have been used in various application domains such as medical informatics, software engineering, configuration of technical systems, natural language processing, databases and web-based information systems. But their most notable success so far is the adoption of the DL-based language OWL 1 BIB003 as the standard ontology language for the semantic web  . Syntax In DLs, one formalizes the relevant notions of an application domain by concept descriptions. A concept description is an expression built from atomic concepts, which are unary predicates, and atomic roles, which are binary predicates, by using the concept constructors provided by the particular DL language in use. DL languages are identified with the concept constructors they allow. For instance the smallest propositionally closed language allowing for the constructors ⊓ (conjunction), ⊔ (disjunction), ¬ (negation), ∀ (value restriction) and ∃ (existential restriction) is called ALC. Typically, a DL knowledge base consists of a terminological box (TBox ), which defines the terminology of an application domain, and an assertional box (ABox ), which contains facts about a specific world. In its simplest form, a TBox is a set of concept definitions of the form A ≡ C that assigns the concept name A to the concept description C. We call a finite set of general concept inclusion (GCI) axioms a general TBox. A GCI is an expression of the form C ⊑ D, where C and D are two possibly complex concept descriptions. It states a subconcept/superconcept relationship between the two concept descriptions. An ABox is a set of concept assertions of the form C(a), which means that the individual a is an instance of the concept C, and role assertions of the form R(a, b), which means that the individual a is in R-relation with individual b. For instance the following TBox contains the definition of a landlocked country, which is a country that only has borders on land, and the definition of an ocean country that has a border to an ocean. The following ABox states the facts about the individuals P ortugal, Austria, and Atlantic Ocean. A := {LandlockedCountry(Austria), Country(P ortugal), Ocean(Atlantic Ocean), hasBorderTo(P ortugal, Atlantic Ocean)} Semantics The meaning of DL concepts is given by means of an interpretation I, which is a tuple consisting of a domain ∆ I and an interpretation function · I . The interpretation function maps every concept occurring in the TBox to a subset of the domain, every role to a binary relation on the domain, and every individual name occurring in the ABox to an element of the domain. The meaning of complex concept descriptions is given inductively based on the constructors used in the concept description. For instance, the concept description Country ⊓ ∃hasBorderTo.Ocean is interpreted as the intersection of the set of countries and the set of elements of the domain that have a border to an ocean. We say that an interpretation I is a model of a TBox T if it satisfies all concept definitions in T , i.e., for every concept definition A ≡ C in T , it maps A and C to the same subset of the domain. Similarly, we say that I is a model of an ABox A, if it satisfies all concept and role assertions in A, i.e., for every concept assertion A(a) in A, the interpretation of a is an element of the interpretation of A, and for every role assertion r(a, b) the interpretation of r contains the pair consisting of the interpretations of a and b. The semantics of DL ABoxes is the open-world semantics, i.e., absence of information about an individual is not interpreted as negative information, but it only indicates lack of knowledge about that individual. Inferences In an application, once we get a description of the application domain using DLs as described above, we can make inferences, i.e., deduce implicit consequences from the explicitly represented knowledge. The basic inference on concept descriptions is subsumption. Given two concept descriptions C and D, the subsumption problem C ⊑ D is the problem of checking whether the concept description D is more general than the concept description C. In other words, it is the problem of determining whether the first concept always, i.e., in every interpretation denotes a subset of the set denoted by the second one. We say that C is subsumed by D w.r.t. a TBox T , if in every model of T , D is more general than C, i.e., the interpretation of C is a subset of the interpretation of D. We denote this as C ⊑ T D. For instance, in the example above, the concepts LandlockedCountry and OceanCountry are both trivially subsumed by the concept Country. The typical inference problem for ABoxes is instance checking, which is the problem of deciding whether the interpretation of a given individual is an element of the interpretation of a given concept in every common model of the TBox and the ABox. For instance, from T and A given above it follows that P ortugal is an ocean country, although A does not contain the assertion OceanCountry(P ortugal). Modern DL systems like FaCT++ BIB005 , Racer BIB001 , Pellet BIB004 , KAON2 BIB006 , Hermit BIB008 and CEL BIB007 provide their users with inference services that solve these inference problems, which are also known as standard inferences.