The Description Logic Handbook covers all aspects of the research in the field of knowledge representation. Written by some of the most prominent researchers in the field, and covering the basic technical material and implementational aspects, it is both a unique reference and a self-study guide.

Knowledge representation, which lies at the core of artificial intelligence, is concerned with encoding knowledge on computers to enable systems to reason automatically. The aims are to help readers make their computer smarter, handle qualitative and uncertain information, and improve computational tractability.

Spatial reasoning is essential for many AI applications. In most existing systems the representation is primarily numerical, so the information that can be handled is limited to precise quantitative data. However, for many purposes the ability to manipulate high-level qualitative spatial information in a flexible way would be extremely useful. Such capabilities can be proveded by logical calculi; and indeed 1st-order theories of certain spatial relations have been given [20]. But computing inferences in 1st-order logic is generally intractable unless special (...) methods are known.0-order modal logics provide an alternative representation which is more expressive than classical 0-order logic and yet often more amenable to automated deduction than 1st-order formalisms. These calculi are usually interpreted as propositional logics: non-logical constants are taken as denoting propositions. However, they can also be given a nominal interpretation in which the constants stand for some kind of object. I show how 0-order logics can be given a spatial interpretation: constants denote regions and logical operators correspond to operations on regions which are important for characterising spatial situations.Representing certain spatial concepts requires the introduction of modal operators, interpreted as functions generating regions related in specific ways to those denoted by their arguments. A significant example is the convex-hull operator whose value is the smallest convex region containing its argument. I investigate how this this operator can be captured in a multi-medal logic. (shrink)

This paper addresses questions of universality related to ontological engineering, namely aims at substantiating (negative) answers to the following three basic questions: (i) Is there a ‘universal ontology’?, (ii) Is there a ‘universal formal ontology language’?, and (iii) Is there a universally applicable ‘mode of reasoning’ for formal ontologies? To support our answers in a principled way, we present a general framework for the design of formal ontologies resting on two main principles: firstly, we endorse Rudolf Carnap’s principle of logical (...) tolerance by giving central stage to the concept of logical heterogeneity, i.e. the use of a plurality of logical languages within one ontology design. Secondly, to structure and combine heterogeneous ontologies in a semantically well-founded way, we base our work on abstract model theory in the form of institutional semantics, as forcefully put forward by Joseph Goguen and Rod Burstall. In particular, we employ the structuring mechanisms of the heterogeneous algebraic specification language HetCasl for defining a general concept of heterogeneous, distributed, highly modular and structured ontologies, called hyperontologies. Moreover, we distinguish, on a structural and semantic level, several different kinds of combining and aligning heterogeneous ontologies, namely integration, connection, and refinement. We show how the notion of heterogeneous refinement can be used to provide both a general notion of sub-ontology as well as a notion of heterogeneous equivalence of ontologies, and finally sketch how different modes of reasoning over ontologies are related to these different structuring aspects. (shrink)

Modal logics, originally conceived in philosophy, have recently found many applications in computer science, artificial intelligence, the foundations of mathematics, linguistics and other disciplines. Celebrated for their good computational behaviour, modal logics are used as effective formalisms for talking about time, space, knowledge, beliefs, actions, obligations, provability, etc. However, the nice computational properties can drastically change if we combine some of these formalisms into a many-dimensional system, say, to reason about knowledge bases developing in time or moving objects. To study (...) the computational behaviour of many-dimensional modal logics is the main aim of this book. On the one hand, it is concerned with providing a solid mathematical foundation for this discipline, while on the other hand, it shows that many seemingly different applied many-dimensional systems (e.g., multi-agent systems, description logics with epistemic, temporal and dynamic operators, spatio-temporal logics, etc.) fit in perfectly with this theoretical framework, and so their computational behaviour can be analyzed using the developed machinery. We start with concrete examples of applied one- and many-dimensional modal logics such as temporal, epistemic, dynamic, description, spatial logics, and various combinations of these. Then we develop a mathematical theory for handling a spectrum of 'abstract' combinations of modal logics - fusions and products of modal logics, fragments of first-order modal and temporal logics - focusing on three major problems: decidability, axiomatizability, and computational complexity. Besides the standard methods of modal logic, the technical toolkit includes the method of quasimodels, mosaics, tilings, reductions to monadic second-order logic, algebraic logic techniques. Finally, we apply the developed machinery and obtained results to three case studies from the field of knowledge representation and reasoning: temporal epistemic logics for reasoning about multi-agent systems, modalized description logics for dynamic ontologies, and spatio-temporal logics. The genre of the book can be defined as a research monograph. It brings the reader to the front line of current research in the field by showing both recent achievements and directions of future investigations (in particular, multiple open problems). On the other hand, well-known results from modal and first-order logic are formulated without proofs and supplied with references to accessible sources. The intended audience of this book is logicians as well as those researchers who use logic in computer science and artificial intelligence. More specific application areas are, e.g., knowledge representation and reasoning, in particular, terminological, temporal and spatial reasoning, or reasoning about agents. And we also believe that researchers from certain other disciplines, say, temporal and spatial databases or geographical information systems, will benefit from this book as well. Key Features: Integrated approach to modern modal and temporal logics and their applications in artificial intelligence and computer science Written by internationally leading researchers in the field of pure and applied logic Combines mathematical theory of modal logic and applications in artificial intelligence and computer science Numerous open problems for further research Well illustrated with pictures and tables. (shrink)

We propose and investigate a uniform modal logic framework for reasoning about topology and relative distance in metric and more general distance spaces, thus enabling the comparison and combination of logics from distinct research traditions such as Tarski’s for topological closure and interior, conditional logics, and logics of comparative similarity. This framework is obtained by decomposing the underlying modal-like operators into first-order quantifier patterns. We then show that quite a powerful and natural fragment of the resulting first-order logic can be (...) captured by one binary operator comparing distances between sets and one unary operator distinguishing between realised and limit distances . Due to its greater expressive power, this logic turns out to behave quite differently from both and conditional logics. We provide finite axiomatisations and ExpTime-completeness proofs for the logics of various classes of distance spaces, in particular metric spaces. But we also show that the logic of the real line is not recursively enumerable. This result is proved by an encoding of Diophantine equations. (shrink)

ABSTRACT The paper studies propositional logics in a bimodal language, in which the first modality is interpreted as the local truth, and the second as the universal truth. The logic S4UC is introduced, which is finitely axiomatizable, has the f.m.p. and is determined by every connected separable metric space.

In [14], we studied the computational behaviour of various first-order and modal languages interpreted in metric or weaker distance spaces. [13] gave an axiomatisation of an expressive and decidable metric logic. The main result of this paper is in showing that the technique of representing metric spaces by means of Kripke frames can be extended to cover the modal (hybrid) language that is expressively complete over metric spaces for the (undecidable) two-variable fragment of first-order logic with binary pred-icates interpreting the (...) metric. The frame conditions needed correspond rather directly with a Boolean modal logic that is, again, of the same expressivity as the two-variable fragment. We use this representation to derive an axiomatisation of the modal hybrid variant of the two-variable fragment, discuss the compactness property in distance logics, and derive some results on (the failure of) interpolation in distance logics of various expressive power. (shrink)

In [STU 00, KUT 03] we introduced a family of ‘modal' languages intended for talking about distances. These languages are interpreted in ‘distance spaces' which satisfy some of the standard axioms of metric spaces. Among other things, we singled out decidable logics of distance spaces and proved expressive completeness results relating classical and modal languages. The aim of this paper is to axiomatize the modal fragments of the semantically defined distance logics of [KUT 03] and give a new proof of (...) their decidability. (shrink)