Overview
\mathcal{ALC} is a foundational description logic used to describe classes of individuals and their relationships via binary roles. It supports Boolean concept operations and role restrictions while remaining decidable.
Syntax
From concept names A and role names r, concepts are formed using
C ::= A\mid\top\mid\bot\mid\neg C\mid C\sqcap C\mid C\sqcup C \mid\exists r.C\mid\forall r.C.
A knowledge base can contain a TBox of concept inclusions C\sqsubseteq D and an ABox of assertions about named individuals.
Semantics
An interpretation has a nonempty domain \Delta^I. Concepts denote subsets of \Delta^I; roles denote binary relations. In particular,
(\exists r.C)^I=\{x\in\Delta^I\mid\exists y\,((x,y)\in r^I\land y\in C^I)\}.
The universal restriction \forall r.C denotes those individuals all of whose r-successors belong to C.
Decidability and Complexity
Concept satisfiability without general TBox axioms is PSPACE-complete. With unrestricted general concept inclusions, standard ALC concept satisfiability and knowledge-base consistency are EXPTIME-complete. These bounds assume ordinary ALC, not extensions with nominals, number restrictions, or complex roles.
Relationships to Other Logics
ALC concepts have a standard translation into first-order logic using two variables, closely relating the formalism to FO² and guarded reasoning. Some expressive extensions of description logic correspond to stronger first-order fragments.
References
- Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, eds. (2003). The Description Logic Handbook. Cambridge University Press.
- Franz Baader, Ian Horrocks, Carsten Lutz, and Uli Sattler (2017). An Introduction to Description Logic. Cambridge University Press.