| date | tags | |||
|---|---|---|---|---|
2020-07-10 |
|
Description logics (DL) are a family of logics, often used in ontologies. (For more discussion on logics, see [[[logics_formalisms_languages_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).
Single individuals in the domain. Correspond to constants in first-order logic.
Examples: garfield, jon.
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.
Binary relations between the individuals. Correspond to binary predicates in first-order logic.
Examples: owner.
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.
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 axioms describe relationships between concepts.
Cat ⊑ Animal is a concept inclusion for "cats are animals".
Mother ≡ Parent ⊓ Woman is a concept equivalence between a shorthand name and its definition using concept intersection.
RBox axioms describe relationships between roles.
(These are not included in the most basic description logics. TODO: restructure this zettel.)
motherOf ⊑ parentOf is a role inclusion for "motherhood is parenthood". All mothers are also parents.
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(parentOf, childOf) expresses that one can't be the parent and the child of the same individual.
TODO
See "Table 1. Common Letters in Description Logic Names" at https://www.lesliesikos.com/description-logics/.