Description Logic

Origin. Evolved from semantic networks and frame systems (1970s-80s). KL-ONE (Brachman & Schmolze, 1985) was influential. The "description logic" family formalized with attention to computational complexity. Foundation for OWL (Web Ontology Language) and the Semantic Web. Balances expressiveness with decidability.

Models. Concepts (classes), roles (relations), and individuals. Ontologies defining what kinds of things exist and how they relate. "A parent is a person with at least one child." Knowledge representation with formal semantics and decidable reasoning: subsumption, consistency, instance checking.

Formalism.

Basic elements:

Concepts: classes/types (Person, Animal, ...)
Roles: binary relations (hasChild, worksFor, ...)
Individuals: named objects (john, mary, ...)

Concept constructors (ALC and extensions):

Syntax	Name	Semantics
A	Atomic concept	A^I ⊆ Δ^I
⊤	Top	Δ^I (everything)
⊥	Bottom	∅ (nothing)
¬C	Negation	Δ^I \ C^I
C ⊓ D	Intersection	C^I ∩ D^I
C ⊔ D	Union	C^I ∪ D^I
∀r.C	Value restriction	{x \| ∀y. (x,y)∈r^I → y∈C^I}
∃r.C	Existential	{x \| ∃y. (x,y)∈r^I ∧ y∈C^I}
≥n r.C	At-least	{x \| \|{y \| (x,y)∈r^I ∧ y∈C^I}\| ≥ n}
≤n r.C	At-most	{x \| \|{y \| (x,y)∈r^I ∧ y∈C^I}\| ≤ n}

DL naming convention:

AL: attributive language (basic)
C: complement (full negation)
E: existential quantification
N: number restrictions
Q: qualified number restrictions
H: role hierarchies
O: nominals (individuals in concepts)
I: inverse roles
S: ALC + transitive roles

Example: SHOIN (basis for OWL-DL)

Knowledge base:

TBox: terminological axioms (C ⊑ D, C ≡ D)
ABox: assertional axioms (C(a), r(a,b))
RBox: role axioms (r ⊑ s, transitivity)

Reasoning tasks:

Concept satisfiability: is C consistent?
Subsumption: does C ⊑ D hold?
Instance checking: is a ∈ C?
Consistency: is the KB satisfiable?
Classification: compute full subsumption hierarchy

Symbols.

Symbol	Unicode	Name	Meaning
⊤	U+22A4	Top	Universal concept
⊥	U+22A5	Bottom	Empty concept
⊓	U+2293	Intersection	Concept and
⊔	U+2294	Union	Concept or
¬	U+00AC	Complement	Concept negation
∀	U+2200	Value restriction	All related are
∃	U+2203	Existential	Some related is
⊑	U+2291	Subsumption	Subclass of
≡	U+2261	Equivalence	Same extension
≥	U+2265	At-least	Minimum cardinality restriction
≤	U+2264	At-most	Maximum cardinality restriction
Δ	U+0394	Delta / Domain	Universe of an interpretation
ᴵ	U+1D35	Superscript I / Interpretation	Extension of a name under I
⊆	U+2286	Subset	Concept extension inside the domain
∈	U+2208	Membership	Individual belongs to an extension
∅	U+2205	Empty set	Extension of ⊥
∩	U+2229	Set intersection	Semantics of ⊓
∪	U+222A	Set union	Semantics of ⊔
TBox	—	Terminological box	Concept and equivalence axioms
ABox	—	Assertional box	Individual and role assertions
RBox	—	Role box	Role hierarchy and role characteristics

Metatheory. Every member of the family is a fragment of first-order logic — the standard translation sends a concept to a formula with one free variable and a role to a binary predicate — so all are sound and complete for the ordinary Tarskian semantics over interpretations I = (Δᴵ, ·ᴵ), and the substance lies in where decidability and complexity fall. Schild (1991) observed that ALC is a notational variant of multi-modal K, transferring the modal results wholesale: concept satisfiability is PSPACE-complete without a TBox (Schmidt-Schauß and Smolka 1991, matching Ladner's bound for K) and ExpTime-complete with respect to a general TBox, since internalizing axioms destroys the small-model bound. SHOIN, underlying OWL DL, is NExpTime-complete; SROIQ, underlying OWL 2 DL, is N2ExpTime-complete (Kazakov 2008). The tractable profiles run the other way: EL and EL++ subsumption is polynomial (Baader, Brandt and Lutz 2005), and DL-Lite answers conjunctive queries in AC⁰ in data complexity by first-order rewriting. The tree model property is what tableau and automata decision procedures exploit.

Applies to. Ontology engineering (Protégé, OWL). Semantic Web. Biomedical ontologies (SNOMED CT, Gene Ontology). Knowledge graphs. Data integration. Conceptual modeling. Query answering over ontologies.

Limitations. Expressiveness is bounded by the tree model property, which every decidable member of the family is built to preserve. A concept is a variable-free formula close to the two-variable fragment, so relational patterns with cycles — "a person whose two parents are married to each other" — are inexpressible even in SROIQ. Feature combinations break decidability: number restrictions must be confined to simple roles, since counting over transitive roles makes the logic undecidable, and complex role inclusions must satisfy a regularity condition. Inverse roles together with number restrictions destroy the finite model property, so a consistent knowledge base may have only infinite models. The open-world assumption blocks negation as failure, defaults, and any inference from absence, and OWL imposes no unique name assumption, so distinctness must be asserted individual by individual. OWL 2 Full, which drops the layering between classes and individuals, is undecidable.