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
∀R.C	—	Value restriction	All R-successors in C
∃R.C	—	Existential	Some R-successor in C
⊑	U+2291	Subsumption	Subclass

Metatheory. EXPTIME-complete. Tableau algorithms. Tree model property. Finite model property. Correspondence to modal K.

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

Limitations. Limited expressiveness. No counting (need extensions). No concrete domains. Extensions increase complexity.