Description logics
Description logics (DL) are a family of logics, often used in ontologies. (For more discussion on logics, see Logics, Formalisms, Languages, and Applications#)
Most DLs are decidable fragments of first-order logic. Krötzsch et al. (2013) explain that there are many DLs, because different applications require different expressivity from the logic. There is a tradeoff between expressivity and performance: inferring easy things is fast, inferring complex things is slow (or undecidable).
Basics
Individuals
Single individuals in the domain. Correspond to constants in first-order logic.
Examples: garfield, jon.
Concepts / Classes
Concepts are sets of individuals, or classes of individuals. Correspond to unary predicates in first-order logic.
Examples: Cat. Top (⊤) and bottom (⊥) are special concepts.
Roles
Binary relations between the individuals. Correspond to binary predicates in first-order logic.
Examples: owner.
Axioms
Axioms are usually divided in three groups: assertional (ABox), terminological (TBox) and relational (RBox).
The following examples contain operations that are not common to all description logics. I’m following mostly Krötzsch et al. (2013), which describes SROIQ. There are resources that explain which DLs allow which operation (e.g. Table 1), but such resources are much more helpful after reading through a list of the operations.
ABox (Assertional axioms)
Cat(garfield) is a concept assertion about a named individual Garfield, who belongs to the set of cats. In other words, Garfield is a cat.
owner(jon,garfield) is a role assertion, describing a relation between Garfield and its owner Jon.
Equality and inequality between individuals are also assertions. For example, garfield ≠ jon asserts that Garfield and Jon are two different individuals, and jon = jon_arbuckle asserts that the two names Jon and Jon Arbuckle refer to the same individual.
TBox (Terminological axioms)
TBox axioms describe relationships between concepts.
Concept inclusion
Cat ⊑ Animal is a concept inclusion for “cats are animals”.
Concept equivalence
Mother ≡ Parent ⊓ Woman is a concept equivalence between a shorthand name and its definition using concept intersection.
RBox (Relational axioms)
RBox axioms describe relationships between roles.
(These are not included in the most basic description logics. TODO: restructure this zettel.)
Role inclusion
motherOf ⊑ parentOf is a role inclusion for “motherhood is parenthood”. All mothers are also parents.
Role composition
brotherOf ◦ parentOf ⊑ uncleOf is a complex role inclusion: the brother of my parent is my uncle. The left-hand side brotherOf ◦ parentOf is a role composition.
Krötzsch et al. (2013) on role composition:
Note that role composition can only appear on the left-hand side of complex role inclusions. Furthermore, in order to retain decidability of reasoning, complex role inclusions are governed by additional structural restrictions that specify whether or not a collection of such axioms can be used together in one ontology.
Explanation why unrestricted role composition becomes undecidable, and how to restrict: https://youtu.be/GdmI85J9fOE
Disjoint roles
Disjoint(parentOf, childOf) expresses that one can’t be the parent and the child of the same individual.
Reflexivity
Symmetry
Transitivity
TODO
SROIQ? SHOIN⁽ᴰ⁾? WTF?
See “Table 1. Common Letters in Description Logic Names” at https://www.lesliesikos.com/description-logics/.
