A Uniform Framework for Concept Definitions in Description Logics

TL;DR

This paper introduces muALCQ, a description logic framework that supports multiple semantics for class definitions, including recursive constructs, enabling more flexible and expressive knowledge representation in AI and databases.

Contribution

It presents muALCQ, a novel description logic formalism that incorporates fixpoint constructs for recursive definitions, with proven decidability and complexity results.

Findings

muALCQ supports recursive class definitions.

Decidability and complexity of reasoning in muALCQ are established.

The framework allows for diverse semantics in class definitions.

Abstract

Most modern formalisms used in Databases and Artificial Intelligence for describing an application domain are based on the notions of class (or concept) and relationship among classes. One interesting feature of such formalisms is the possibility of defining a class, i.e., providing a set of properties that precisely characterize the instances of the class. Many recent articles point out that there are several ways of assigning a meaning to a class definition containing some sort of recursion. In this paper, we argue that, instead of choosing a single style of semantics, we achieve better results by adopting a formalism that allows for different semantics to coexist. We demonstrate the feasibility of our argument, by presenting a knowledge representation formalism, the description logic muALCQ, with the above characteristics. In addition to the constructs for conjunction, disjunction, negation, quantifiers, and qualified number restrictions, muALCQ includes special fixpoint constructs to express (suitably interpreted) recursive definitions. These constructs enable the usual frame-based descriptions to be combined with definitions of recursive data structures such as directed acyclic graphs, lists, streams, etc. We establish several properties of muALCQ, including the decidability and the computational complexity of reasoning, by formulating a correspondence with a particular modal logic of programs called the modal mu-calculus.