Description Logic ALC

Origin. Schmidt-Schauß and Smolka, "Attributive concept descriptions with complements" (Artificial Intelligence, 1991). Attributive Language with Complements; the basis of OWL (W3C, 2004) and of the SH family of extensions. Core description logic. Basis for OWL. Decidable reasoning about concepts and roles.

Models. Concepts (unary predicates), roles (binary relations). TBox: terminological — concept definitions and subsumptions. ABox: assertional — instance facts. Reasoning tasks: subsumption (is C a subclass of D?), satisfiability, instance checking. An ontology is a TBox plus an ABox.

Formalism.

Concept constructors: ⊤ (top), ⊥ (bottom) A (atomic concept) ¬C (complement) C ⊓ D (intersection) C ⊔ D (union) ∀R.C (value restriction) ∃R.C (existential restriction)

Semantics: Interpretation I = (Δᴵ, ·ᴵ) Aᴵ ⊆ Δᴵ (concept extension) Rᴵ ⊆ Δᴵ × Δᴵ (role extension) (C ⊓ D)ᴵ = Cᴵ ∩ Dᴵ (∃R.C)ᴵ = {x | ∃y. (x,y) ∈ Rᴵ ∧ y ∈ Cᴵ}

TBox (terminological): C ⊑ D (concept inclusion) C ≡ D (concept equivalence) Example: Parent ≡ Person ⊓ ∃hasChild.Person

ABox (assertional): C(a): a is instance of C R(a,b): a related to b by R Example: Parent(john), hasChild(john, mary)

Reasoning tasks: Subsumption: C ⊑ D? Satisfiability: C consistent? Instance checking: C(a)?

Complexity: ALC reasoning: EXPTIME-complete. Without TBox: PSPACE.

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	Universal / Value restriction	All R-successors in C
∃	U+2203	Existential restriction	Some R-successor in C
⊑	U+2291	Subsumption	Subclass
≡	U+2261	Equivalence	Concept definition
Δ	U+0394	Delta / Domain	Universe of the interpretation
ᴵ	U+1D35	Superscript I / Interpretation	Extension of a name under I
⊆	U+2286	Subset	Extension contained in the domain
∈	U+2208	Membership	Element of an extension
∩	U+2229	Set intersection	Semantics of ⊓
×	U+00D7	Cartesian product	Domain of a role extension
∧	U+2227	Conjunction	Metalanguage connective in the semantics
□	U+25A1	Box / Necessity	Modal reading of ∀R.C under Schild's translation
◇	U+25C7	Diamond / Possibility	Modal reading of ∃R.C under Schild's translation
TBox	—	Terminological box	Inclusions and definitions
ABox	—	Assertional box	Concept and role assertions

Metatheory. ALC is sound and complete for the class of all interpretations I = (Δᴵ, ·ᴵ). Its standard translation into first-order logic lands in the two-variable fragment, and Schild (1991) identified it with the multi-modal logic Kₙ: concepts are formulas, roles are accessibility relations, ∃R.C is ◇_R C and ∀R.C is □_R C. Every satisfiable ALC concept has a tree-shaped model whose depth is bounded by the nesting of quantifiers and whose branching is bounded by the number of existential restrictions, and ALC has the finite model property, so unsatisfiability is always witnessed on finite structures. Schmidt-Schauß and Smolka (1991) showed that concept satisfiability without a TBox is PSPACE-complete, matching Ladner's (1977) bound for K. With a general TBox the tree unravels to exponential depth and the problem becomes ExpTime-complete. Subsumption, instance checking and knowledge base consistency are interreducible in polynomial time, since C ⊑ D holds exactly when C ⊓ ¬D is unsatisfiable.

Applies to. OWL ontologies. Semantic web. Knowledge representation. Medical ontologies. Enterprise modeling.

Limitations. ALC cannot count: "has at least two children" is inexpressible and requires the N or Q extensions. It has no inverse roles, so hasChild and hasParent remain unrelated primitives; no nominals, so an individual cannot appear inside a concept and enumerations cannot be written; and no fixpoints, so transitive closure and "ancestor" lie outside it, making ALC strictly weaker than ALC_reg and the modal μ-calculus. Transitivity of a role is itself unexpressible — asserting it yields the different logic S. The tree model property that underwrites decidability is simultaneously the ceiling on expressiveness: no concept can force a cycle, so "whose two parents are married to each other" has no rendering. The semantics is open-world and monotone, nothing follows from an absent assertion, and no unique name assumption holds. Concrete domains such as integers and strings are absent, and admitting them without restriction destroys decidability.