We investigate conjunctive query inseparability of description logic (DL) knowledge bases (KBs) with respect to a given signature, a fundamental problem for KB versioning, module extraction, forgetting and knowledge exchange. We study the data and combined complexity of deciding KB query inseparability for fragments of Horn-ALCHI, including the DLs underpinning OWL 2 QL and OWL 2 EL. While all of these DLs are P-complete for data complexity, the combined complexity ranges from P to EXPTIME and 2EXPTIME. We also resolve two major open problems for OWL 2 QL by showing that TBox query inseparability and the membership problem for universal UCQ-solutions in knowledge exchange are both EXPTIME-complete for combined complexity.

In the last few years, there has been a large effort for analyzing the computational properties of reasoning in fuzzy description logics. This has led to a number of papers studying the complexity of these logics, depending on the chosen semantics. Surprisingly, despite being arguably the simplest form of fuzzy semantics, not much is known about the complexity of reasoning in fuzzy description logics w.r.t. witnessed models over the Gödel t-norm. We show that in the logic G-IALC, reasoning cannot be restricted to finitely-valued models in general. Despite this negative result, we also show that all the standard reasoning problems can be solved in exponential time, matching the complexity of reasoning in classical ALC.

Two-way regular path queries (2RPQs) have received increased attention recently due to their ability to relate pairs of objects by flexibly navigating graph structured data. They are present in property paths in SPARQL 1.1, the new standard RDF query language, and in the XML query language XPath. In line with XPath, we consider the extension of 2RPQs with nesting, which allows one to require that objects along a path satisfy complex conditions, in turn expressed through (nested) 2RPQs. We study the computational complexity of answering nested 2RPQs and conjunctions thereof (CN2RPQs) in the presence of domain knowledge expressed in description logics (DLs). We establish tight complexity bounds in data and combined complexity for a variety of DLs, ranging from lightweight DLs (DL-Lite, EL) up to highly expressive ones. Interestingly, we are able to show that adding nesting to (C)2RPQs does not affect worst-case data complexity of query answering for any of the considered DLs. However, in the case of lightweight DLs, adding nesting to 2RPQs leads to a surprising jump in combined complexity, from P-complete to ExpTime-complete.

We design temporal description logics suitable for reasoning about temporal conceptual data models and investigate their computational complexity. Our formalisms are based on DL-Lite logics with three types of concept inclusions (ranging from atomic concept inclusions and disjointness to the full Booleans), as well as cardinality constraints and role inclusions. In the temporal dimension, they capture future and past temporal operators on concepts, flexible and rigid roles, the operators `always' and `some time' on roles, data assertions for particular moments of time and global concept inclusions. The logics are interpreted over the Cartesian products of object domains and the flow of time (Z,<), satisfying the constant domain assumption. We prove that the most expressive of our temporal description logics (which can capture lifespan cardinalities and either qualitative or quantitative evolution constraints) turn out to be undecidable. However, by omitting some of the temporal operators on concepts/roles or by restricting the form of concept inclusions we obtain logics whose complexity ranges between PSpace and NLogSpace. These positive results were obtained by reduction to various clausal fragments of propositional temporal logic, which opens a way to employ propositional or first-order temporal provers for reasoning about temporal data models.

In the last 20 years many proposals have been made to incorporate non-monotonic reasoning into description logics, ranging from approaches based on default logic and circumscription to those based on preferential semantics. In particular, the non-monotonic description logic $\mathcal{ALC}$+T$_{\mathsf{min}}$ uses a combination of the preferential semantics with minimization of a certain kind of concepts, which represent atypical instances of a class of elements. One of its drawbacks is that it suffers from the problem known as the \emph{property blocking inheritance}, which can be seen as a weakness from an inferential point of view. In this paper we propose an extension of $\mathcal{ALC}$+T$_{\mathsf{min}}$, namely $\mathcal{ALC}$+T$^+_{\mathsf{min}}$, with the purpose to solve the mentioned problem. In addition, we show the close connection that exists between $\mathcal{ALC}$+T$^+_{\mathsf{min}}$ and concept-circumscribed knowledge bases. Finally, we study the complexity of deciding the classical reasoning tasks in $\mathcal{ALC}$+T$^+_{\mathsf{min}}$.

We present a novel reasoning calculus for the description logic SHOIQ^+---a knowledge representation formalism with applications in areas such as the Semantic Web. 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.

In the last two decades, modal and description logics have been applied to numerous areas of computer science, including knowledge representation, formal verification, database theory, distributed computing and, more recently, semantic web and ontologies. For this reason, the problem of automated reasoning in modal and description logics has been thoroughly investigated. In particular, many approaches have been proposed for efficiently handling the satisfiability of the core normal modal logic K(m), and of its notational variant, the description logic ALC. Although simple in structure, K(m)/ALC is computationally very hard to reason on, its satisfiability being PSPACE-complete. In this paper we start exploring the idea of performing automated reasoning tasks in modal and description logics by encoding them into SAT, so that to be handled by state-of-the-art SAT tools; as with most previous approaches, we begin our investigation from the satisfiability in K(m). We propose an efficient encoding, and we test it on an extensive set of benchmarks, comparing the approach with the main state-of-the-art tools available. Although the encoding is necessarily worst-case exponential, from our experiments we notice that, in practice, this approach can handle most or all the problems which are at the reach of the other approaches, with performances which are comparable with, or even better than, those of the current state-of-the-art tools.

The problem of Natural Language Query Formalization (NLQF) is to translate a given user query in natural language (NL) into a formal language () so that the semantic interpretation has equivalence with the NL interpretation. Formalization of NL queries enables logic based reasoning during information retrieval, database query, question-answering, etc. Formalization also helps in Web query normalization and indexing, query intent analysis, etc. In this paper we are proposing a Description Logics based formal methodology for wh-query intent (also called desire) identification and corresponding formal translation. We evaluated the scalability of our proposed formalism using Microsoft Encarta 98 query dataset and OWLS TC v.4.0 dataset.

We study a general framework for query rewriting in the presence of an arbitrary first-order logic ontology over a database signature. The framework supports deciding the existence of a safe-range first-order equivalent reformulation of a query in terms of the database signature, and if so, it provides an effective approach to construct the reformulation based on interpolation using standard theorem proving techniques (e.g., tableau). Since the reformulation is a safe-range formula, it is effectively executable as an SQL query. At the end, we present a non-trivial application of the framework with ontologies in the very expressive ALCHOIQ description logic, by providing effective means to compute safe-range first-order exact reformulations of queries.

The Beth definability property, a well-known property from classical logic, is investigated in the context of description logics: if a general L-TBox implicitly defines an L-concept in terms of a given signature, where L is a description logic, then does there always exist over this signature an explicit definition in L for the concept? This property has been studied before and used to optimize reasoning in description logics. In this paper a complete classification of Beth definability is provided for extensions of the basic description logic ALC with transitive roles, inverse roles, role hierarchies, and/or functionality restrictions, both on arbitrary and on finite structures. Moreover, we present a tableau-based algorithm which computes explicit definitions of at most double exponential size. This algorithm is optimal because it is also shown that the smallest explicit definition of an implicitly defined concept may be double exponentially long in the size of the input TBox. Finally, if explicit definitions are allowed to be expressed in first-order logic, then we show how to compute them in single exponential time.