We propose a novel technique for proving the consistency of large, complex and heterogeneous theories for which ‘standard’ automated reasoning methods are considered insufficient. In particular, we exemplify the applicability of the method by establishing the consistency of the foundational ontology DOLCE, a large, first-order ontology. The approach we advocate constructs a global model for a theory, in our case DOLCE, built from smaller models of subtheories together with amalgamability properties between such models. The proof proceeds by (i) hand-crafting a so-called architectural specification of DOLCE which reflects the way models of the theory can be built, (ii) an automated verification of the amalgamability conditions, and (iii) a (partially automated) series of relative consistency proofs.

Many Knowledge Bases (KBs) are now readily available and encompass colossal quantities of information thanks to either a long-term funding effort (e.g. WordNet, OpenCyc) or a collaborative process (e.g. Freebase, DBpedia). However, each of them is based on a different rigorous symbolic framework which makes it hard to use their data in other systems. It is unfortunate because such rich structured knowledge might lead to a huge leap forward in many other areas of AI like nat- ural language processing (word-sense disambiguation, natural language understanding, ...), vision (scene classification, image semantic annotation, ...) or collaborative filtering. In this paper, we present a learning process based on an innovative neural network architecture designed to embed any of these symbolic representations into a more flexible continuous vector space in which the original knowledge is kept and enhanced. These learnt embeddings would allow data from any KB to be easily used in recent machine learning meth- ods for prediction and information retrieval. We illustrate our method on WordNet and Freebase and also present a way to adapt it to knowledge extraction from raw text.

ABox abduction is an important aspect for abductive reasoning in Description Logics (DLs). It finds all minimal sets of ABox axioms that should be added to a background ontology to enforce entailment of a specified set of ABox axioms. As far as we know, by now there is only one ABox abduction method in expressive DLs computing abductive solutions with certain minimality. However, the method targets an ABox abduction problem that may have infinitely many abductive solutions and may not output an abductive solution in finite time. Hence, in this paper we propose a new ABox abduction problem which has only finitely many abductive solutions and also propose a novel method to solve it. The method reduces the original problem to an abduction problem in logic programming and solves it with Prolog engines. Experimental results show that the method is able to compute abductive solutions in benchmark OWL DL ontologies with large ABoxes.

We also require a generic model of provenance The Web has evolved from a collection of hyperlinked documents in order to support the diverse ecosystem of sensor to a complex ecosystem of interconnected documents, platforms and data. We have investigated a number of existing services and devices. Due to the inherent open nature of the models for representing provenance information but Web, data can be published by anyone or any'thing'. As a found many of these to be tailored to specific domains result of this, there is enormous variation in the quality of (e.g.

OWL 2 has been standardized by the World Wide Web Consortium (W3C) as a family of ontology languages for the Semantic Web. The most expressive of these languages is OWL 2 Full, but to date no reasoner has been implemented for this language. Consistency and entailment checking are known to be undecidable for OWL 2 Full. We have translated a large fragment of the OWL 2 Full semantics into first-order logic, and used automated theorem proving systems to do reasoning based on this theory. The results are promising, and indicate that this approach can be applied in practice for effective OWL reasoning, beyond the capabilities of current Semantic Web reasoners. This is an extended version of a paper with the same title that has been published at CADE 2011, LNAI 6803, pp. 446-460. The extended version provides appendices with additional resources that were used in the reported evaluation.

Recently there have been some unexpected results concerning Fuzzy Description Logics (FDLs) with General Concept Inclusions (GCIs). They show that, unlike the classical case, the DL ALC with GCIs does not have the finite model property under Lukasiewicz Logic or Product Logic and, specifically, knowledge base satisfiability is an undecidable problem for Product Logic. We complete here the analysis by showing that knowledge base satisfiability is also an undecidable problem for Lukasiewicz Logic.

Debugging of ontologies is an important prerequisite for their wide-spread application, especially in areas that rely upon everyday users to create and maintain knowledge bases, as in the case of the Semantic Web. Recent approaches use diagnosis methods to identify causes of inconsistent or incoherent ontologies. However, in most debugging scenarios these methods return many alternative diagnoses, thus placing the burden of fault localization on the user. This paper demonstrates how the target diagnosis can be identified by performing a sequence of observations, that is, by querying an oracle about entailments of the target ontology. We exploit a-priori probabilities of typical user errors to formulate information-theoretic concepts for query selection. Our evaluation showed that the proposed method significantly reduces the number of required queries compared to myopic strategies. We experimented with different probability distributions of user errors and different qualities of the a-priori probabilities. Our measurements showed the advantageousness of information-theoretic approach to query selection even in cases where only a rough estimate of the priors is available.

Uncertainty is unavoidable when modeling most application domains. In medicine, for example, symptoms (such as pain, dizziness, or nausea) are always subjective, and hence imprecise and incomparable. Additionally, concepts and their relationships may be inexpressible in a crisp, clear-cut manner. We extend the description logic ALC with multi-valued semantics based on lattices that can handle uncertainty on concepts as well as on the axioms of the ontology. We introduce reasoning methods for this logic w.r.t. general concept inclusions and show that the complexity of reasoning is not increased by this new semantics.

As more and more application areas require higher scalability, the study of fragments of expressive The high computational complexity of the expressive DLs with better computational properties has become an Description Logics (DLs) that underlie the important area of research. OWL standard has motivated the study of their Horn fragments of DLs, which are obtained by restricting Horn fragments, which are usually tractable in data the syntax of a DL in such a way that disjunction is not complexity and can also have lower combined complexity, expressible, were first considered in [Hustadt et al., 2005] particularly for query answering. In this paper as expressive fragments with tractable data complexity (see we provide algorithms for answering conjunctive also [Krötzsch et al., 2007]). It was later identified that they 2-way regular path queries (2CRPQs), a nontrivial can also exhibit lower combined complexity when it comes generalization of plain conjunctive queries, to query answering. Indeed, answering conjunctive queries in the Horn fragments of the DLs SHOIQ and (CQs), a kind of database-inspired queries that have become SROIQ underlying OWL 1 and OWL 2. We show the standard for querying DLs, is in ExpTime for the Horn that the combined complexity of the problem is ExpTime-complete fragment of the prominent SHIQ [Eiter et al., 2008], while it for Horn-SHOIQ and 2ExpTimecomplete is already 2ExpTime-hard for quite restricted (non Horn) fragments for the more expressive Horn-SROIQ, of SHIQ, like ALCI [Lutz, 2008] and SH [Eiter et but is PTime-complete in data complexity for both.

Largely motivated by Semantic Web applications, many highly scalable, but incomplete, query answering systems have been recently developed. Evaluating the scalability-completeness trade-off exhibited by such systems is an important requirement for many applications. In this paper, we address the problem of formally comparing complete and incomplete systems given an ontology schema (or TBox) T. We formulate precise conditions on TBoxes T expressed in the EL, QL or RL profile of OWL 2 under which an incomplete system is indistinguishable from a complete one w.r.t. T, regardless of the input query and data. Our results also allow us to quantify the "degree of incompleteness" of a given system w.r.t. T as well as to automatically identify concrete queries and data patterns for which the incomplete system will miss answers.