Description logics are knowledge representation and reasoning formalisms which represent conceptual knowledge on an abstract logical level. Concrete domains are a theoretically well-founded approach to the integration of description logic reasoning with reasoning about concrete objects such as numbers, time intervals or spatial regions. In this paper, the complexity of combined reasoning with description logcis and on concrete domains is investigated. We extend ALC(D), which is the basic description logic for reasoning with concrete domains, by the operators 'feature agreement' and 'feature disagreement'. For the extended logic,called ALCF(D), an algorithm for deciding the ABox consistency problem is devised. The strategy employed by this algorithm is vital for the efficient implementation of reasoners for description logics incorporating concrete domains. Based on the algorithm, it is proved that the standard reasoning problems for both logics ALC(D) and ALCF(D) are PSpace-complete - provided that the satisfiability test of the concrete domain used is in PSpace. / This is an extended version of the article in: Proceedings of IJCAI-99, Stockholm, Sweden, July 31-August 6, Morgan Kaufmann Publ. In ., San Mateo, CA, 1999

The problem of rewriting a concept given a terminology can informally be stated as follows: given a terminology T (i.e., a set of concept definitions) and a concept description C that does not contain concept names defined in T , can this description be rewritten into a 'related better' description E by using (some of) the names defined in T ? In this paper, we first introduce a general framework for the rewriting problem in description logics, and then concentrate on one specific instance of the framework, namely the minimal rewriting problem (where 'better' means shorter, and 'related' means equivalent). We investigate the complexity of the decision problem induced by the minimal rewriting problem for the languages FL0, ALN, ALE, and ALC, and then introduce an algorithm for computing (minimal) rewritings for the languages ALE and ALN. Finally, we sketch other interesting instances of the framework. Our interest for the minimal rewriting problem stems from the fact that algorithms for non-standard inferences, such as computing least common subsumers and matchers, usually produce concept descriptions not containing defined names. Consequently, these descriptions are rather large and hard to read and comprehend. First experiments in a chemical process engineering application show that rewriting can reduce the size of concept descriptions obtained as least common subsumers by almost two orders of magnitude. / Please download the revised version LTCS-00-04 containing revised proofs of the technical results. / An abridged version of this report appeared in the Proceedings of the International Conference on Knowledge Representation and Reasoning (KR'2000).

Computing the most specific concept (msc) is an inference task that can be used to support the 'bottom-up' construction of knowledge bases for KR systems based on description logics. For description logics that allow for number restrictions or existential restrictions, the msc need not exist, though. Previous work on this problem has concentrated on description logics that allow for universal value restrictions and number restrictions, but not for existential restrictions. The main new contribution of this paper is the treatment of description logics with existential restrictions. More precisely, we show that, for the description logic ALE (which allows for conjunction, universal value restrictions, existential restrictions, negation of atomic concepts) the msc of an ABox-individual only exists in case of acyclic ABoxes. For cyclic ABoxes, we show how to compute an approximation of the msc. Our approach for computing the (approximation of the) msc is based on representing concept descriptions by certain trees and ABoxes by certain graphs, and then characterizing instance relationships by homomorphisms from trees into graphs. The msc/approximation operation then mainly corresponds to unraveling the graphs into trees and translating them back into concept descriptions.

Axiom pinpointing has been introduced in description logics (DLs) to help the user to understand the reasons why consequences hold and to remove unwanted consequences by computing minimal (maximal) subsets of the knowledge base that have (do not have) the consequence in question. The pinpointing algorithms described in the DL literature are obtained as extensions of the standard tableau-based reasoning algorithms for computing consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL. The purpose of this paper is to develop a general approach for extending a tableau-based algorithm to a pinpointing algorithm. This approach is based on a general definition of „tableau algorithms,' which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.

In a previous ICFCA paper we have shown that, in the Description Logics EL and ELgfp, the set of general concept inclusions holding in a finite model always has a finite basis. In this paper, we address the problem of how to compute this basis efficiently, by adapting methods from formal concept analysis.

Language equations are equations where both the constants occurring in the equations and the solutions are formal languages. They have first been introduced in formal language theory, but are now also considered in other areas of computer science. In the present paper, we restrict the attention to language equations with one-sided concatenation, but in contrast to previous work on these equations, we allow not just union but all Boolean operations to be used when formulating them. In addition, we are not just interested in deciding solvability of such equations, but also in deciding other properties of the set of solutions, like its cardinality (finite, infinite, uncountable) and whether it contains least/greatest solutions. We show that all these decision problems are ExpTime-complete. / This report has also appeared as TUCS Technical Report, Turku Centre for Computer Science, University of Turku, Finland.

Action formalisms based on description logics (DLs) have recently been introduced as decidable fragments of well-established action theories such as the Situation Calculus and the Fluent Calculus. However, existing DL action formalisms fail to include general TBoxes, which are the standard tool for formalising ontologies in modern description logics. We define a DL action formalism that admits general TBoxes, propose an approach to addressing the ramification problem that is introduced in this way, and perform a detailed investigation of the decidability and computational complexity of reasoning in our formalism.

We identify a general property of concrete domains that is sufficient for proving decidability of DLs equipped with them and GCIs. We show that some useful concrete domains, such as temporal one based on the Allen relations and a spatial one based on the RCC-8 relations, have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with such concrete domains.

Recently, it was shown for the DL EL that subsumption and instance problem w.r.t. cyclic terminologies can be decided in polynomial time. In this paper, we show that both problems remain tractable even when admitting general concept inclusion axioms and simple role inclusion axioms.

Description Logics (DLs) with concrete domains are a useful tool in many applications. To further enhance the expressive power of such DLs, it has been proposed to add database-style key constraints. Up to now, however, only uniqueness constraints have been considered in this context, thus neglecting the second fundamental family of key constraints: functional dependencies. In this paper, we consider the basic DL with concrete domains ALC(D), extend it with functional dependencies, and analyze the impact of this extension on the decidability and complexity of reasoning. Though intuitively the expressivity of functional dependencies seems weaker than that of uniqueness constraints, we are able to show that the former have a similarly severe impact on the computational properties: reasoning is undecidable in the general case, and NExpTime-complete in some slightly restricted variants of our logic.