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 .
Terminological knowledge representation systems (TKRSs) are tools for designing and using knowledge bases that make use of terminological languages (or concept languages). We analyze from a theoretical point of view a TKRS whose capabilities go beyond the ones of presently available TKRSs. The new features studied, often required in practical applications, can be summarized in three main points. First, we consider a highly expressive terminological language, called ALCNR, including general complements of concepts, number restrictions and role conjunction. Second, we allow to express inclusion statements between general concepts, and terminological cycles as a particular case. Third, we prove the decidability of a number of desirable TKRS-deduction services (like satisfiability, subsumption and instance checking) through a sound, complete and terminating calculus for reasoning in ALCNR-knowledge bases. Our calculus extends the general technique of constraint systems. As a byproduct of the proof, we get also the result that inclusion statements in ALCNR can be simulated by terminological cycles, if descriptive semantics is adopted.
An important characteristic of many logics for Artificial Intelligence is their nonmonotonicity. This means that adding a formula to the premises can invalidate some of the consequences. There may, however, exist formulae that can always be safely added to the premises without destroying any of the consequences: we say they respect monotonicity. Also, there may be formulae that, when they are a consequence, can not be invalidated when adding any formula to the premises: we call them conservative. We study these two classes of formulae for preferential logics, and show that they are closely linked to the formulae whose truth-value is preserved along the (preferential) ordering. We will consider some preferential logics for illustration, and prove syntactic characterization results for them. The results in this paper may improve the efficiency of theorem provers for preferential logics.
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.
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.