Calvanese, D., Lenzerini, M., Nardi, D.

The notion of class is ubiquitous in computer science and is central in many formalisms for the representation of structured knowledge used both in knowledge representation and in databases. In this paper we study the basic issues underlying such representation formalisms and single out both their common characteristics and their distinguishing features. Such investigation leads us to propose a unifying framework in which we are able to capture the fundamental aspects of several representation languages used in different contexts. The proposed formalism is expressed in the style of description logics, which have been introduced in knowledge representation as a means to provide a semantically well-founded basis for the structural aspects of knowledge representation systems. The description logic considered in this paper is a subset of first order logic with nice computational characteristics. It is quite expressive and features a novel combination of constructs that has not been studied before. The distinguishing constructs are number restrictions, which generalize existence and functional dependencies, inverse roles, which allow one to refer to the inverse of a relationship, and possibly cyclic assertions, which are necessary for capturing real world domains. We are able to show that it is precisely such combination of constructs that makes our logic powerful enough to model the essential set of features for defining class structures that are common to frame systems, object-oriented database languages, and semantic data models. As a consequence of the established correspondences, several significant extensions of each of the above formalisms become available. The high expressiveness of the logic we propose and the need for capturing the reasoning in different contexts forces us to distinguish between unrestricted and finite model reasoning. A notable feature of our proposal is that reasoning in both cases is decidable. We argue that, by virtue of the high expressive power and of the associated reasoning capabilities on both unrestricted and finite models, our logic provides a common core for class-based representation formalisms.

More precisely, an interpr etation I ( I; I) consists of a domain of interpr etation I, and an interpr etation function I mapping ev ery atomic concept A to a subset of I and ev ery atomic role R to a subset of I I . The in terpretation function I is extended to complex concepts of ALC Q (note that in ALC Q roles are alw a ys atomic) as follo ws: I I? I; (: C) I I C I ( C 1 u C 2) I C I 1 \ C I 2 ( C 1 t C 2) I C I 1 [ C I 2 ( 9 R: C) I f s 2 I j9 s 0: ( s; s 0) 2 R I and s 0 2 C I g ( 8 R: C) I f s 2 I j8 s 0: ( s; s 0) 2 R I implies s 0 2 C I g ( nR: C) I f s 2 I j # f s 0 j ( s; s 0) 2 R I and s 0 2 C I g n g ( nR: C) I f s 2 I j # f s 0 j ( s; s 0) 2 R I and s 0 2 C I g n g 89 De Gia como & Lenzerini where # S denotes the cardinalit y of the set S . A c onc ept C is satisable i there exists an in terpretation I suc h that C I 6;, otherwise C is unsatisable . A c onc ept C 1 is subsume d by a c onc ept C 2, written as C 1 v C 1, i for ev ery in terpretation I, C I 1 C I 2 . Our kno wledge expressed in terms of concepts and roles is assem bled in to a sp ecial kno wledge base, traditionally called TBox, whic h consists of a nite (p ossibly empt y) set of assertions. In order to b e as general as p ossible, w e assume that ev ery assertion has the form of an inclusion assertion (or simply inclusion): C 1 v C 2 without an y restriction on the form of the concepts C 1 and C 2 . A pair of inclusions of the form f C 1 v C 2;C 2 v C 1 g is often written as C 1 C 2 and is called e quivalenc e assertion .

A class of interval-based temporal languages for uniformly representing and reasoning about actions and plans is presented. Actions are represented by describing what is true while the action itself is occurring, and plans are constructed by temporally relating actions and world states. The temporal languages are members of the family of Description Logics, which are characterized by high expressivity combined with good computational properties. The subsumption problem for a class of temporal Description Logics is investigated and sound and complete decision procedures are given. The basic language TL-F is considered first: it is the composition of a temporal logic TL -- able to express interval temporal networks -- together with the non-temporal logic F -- a Feature Description Logic. It is proven that subsumption in this language is an NP-complete problem. Then it is shown how to reason with the more expressive languages TLU-FU and TL-ALCF. The former adds disjunction both at the temporal and non-temporal sides of the language, the latter extends the non-temporal side with set-valued features (i.e., roles) and a propositionally complete language.

We study the complexity of the combination of the Description Logics ALCQ and ALCQI with a terminological formalism based on cardinality restrictions on concepts. These combinations can naturally be embedded into C^2, the two variable fragment of predicate logic with counting quantifiers, which yields decidability in NExpTime. We show that this approach leads to an optimal solution for ALCQI, as ALCQI with cardinality restrictions has the same complexity as C^2 (NExpTime-complete). In contrast, we show that for ALCQ, the problem can be solved in ExpTime. This result is obtained by a reduction of reasoning with cardinality restrictions to reasoning with the (in general weaker) terminological formalism of general axioms for ALCQ extended with nominals. Using the same reduction, we show that, for the extension of ALCQI with nominals, reasoning with general axioms is a NExpTime-complete problem. Finally, we sharpen this result and show that pure concept satisfiability for ALCQI with nominals is NExpTime-complete. Without nominals, this problem is known to be PSpace-complete.

Borgida, A., Patel-Schneider, P. F.

Journal of Arti cial In telligence Researc h 1 (1994) 277{308 Submitted 3/94; published 6/94 A Seman tics and Complete Algorithm for Subsumption in the CLASSIC Description Logic Alex Borgida bor gid a@cs.r A T&T Bel l L ab or atories 600 Mountain A venue Murr ay Hil l, NJ 07974 U. S. A. Abstract This pap er analyzes the correctness of the subsumption algorithm used in classic, a description logic-based kno wledge represen tation system that is b eing used in practical applications. In order to deal e cien tly with individuals in classic descriptions, the de-v elop ers ha v e had to use an algorithm that is incomplete with resp ect to the standard, mo del-theoretic seman tics for description logics. The soundness and completeness of the p olynomial-tim e subsumption algorithm is established using description graphs, whic h are an abstracted v ersion of the implemen tati on structures used in classic, and are of indep enden ti n terest.