Knowledge Representation — DL, Allen, RCC-8

chatbot methods-of-ai

Note on scope. This note was originally titled “Description Logics” but has been expanded into the full KR I + II hub for Methods of AI — covering Description Logics (ALC), TBox/ABox, OWA/CWA, Tableaux, OWL, Allen’s tense logic and RCC-8. The filename Description Logics.md is preserved so that existing wikilinks keep working. The original atomic-note content lives at the bottom under Original atomic note — Description Logics (DL).

Companion files for exam prep:

📋 lernzettel_knowledge-representation_30-04-26 — compact 1-page exam sheet

✏️ quiz_knowledge-representation_30-04-26 — 7 questions

Core Ideas
Description Logics — ALC
TBox and ABox
Reasoning tasks in DL
Tableaux Algorithm (Inference)
Open vs. Closed World Assumption (OWA / CWA)
OWL (Web Ontology Language)
Allen’s Tense Logic (Temporal Reasoning)
RCC-8 (Region Connection Calculus)
Formulas & Notation
Common Exam Traps
Quick comparison (DL vs. FOL)
Visualisations (Python)
ALGORITHMS ⭐
Worked examples
Original atomic note — Description Logics (DL)
See also

Core Ideas

Knowledge Representation (KR): formal, structured way to represent information so that machines can reason about it.
Key trade-off: Expressivity vs. Practicality (more expressive = harder / undecidable to reason with).
Description Logics (DL): family of KR languages for describing categories/classes with formal model-theoretic semantics. Decidable fragments of FOL.
A KR knowledge base = TBox (terminological knowledge about classes) + ABox (facts about individuals). Together: an ontology.
DLs underpin OWL (the W3C semantic-web ontology language).

Description Logics — ALC

ALC = Attributive Concept Language with Complements (slide 31 of Session 06).

The four ALC constructors (plus the trivial concepts ⊤, ⊥, atomic A, and complement ¬C) define what concept descriptions can look like. Concepts denote sets of individuals in the interpretation; roles denote binary relations.

Constructor	Syntax	Semantics (interpretation Cᴵ)	Intuition
Atomic concept	A	Aᴵ ⊆ Δᴵ	Named class (e.g. `Student`)
Top	⊤	Δᴵ	Everything in the domain
Bottom	⊥	∅	Empty class
Negation	¬C	Δᴵ \ Cᴵ	Complement
Intersection	C ⊓ D	Cᴵ ∩ Dᴵ	Both C and D
Union	C ⊔ D	Cᴵ ∪ Dᴵ	C or D
Value restriction	∀R.C	{ x \| ∀y (x,y)∈Rᴵ → y∈Cᴵ }	All R-fillers are C
Existential restriction	∃R.C	{ x \| ∃y (x,y)∈Rᴵ ∧ y∈Cᴵ }	Some R-filler is C

Roles (R, S, …) are atomic binary relations (e.g. hasChild, worksAt). Pure ALC has no role hierarchy and no transitivity — those require extension letters (see OWL (Web Ontology Language)).

Concept descriptions — building blocks of TBox/ABox

You compose larger concepts from the constructors above. Examples:

Parent ≡ Person ⊓ ∃hasChild.Person
HappyParent ≡ Parent ⊓ ∀hasChild.Happy
Childless ≡ Person ⊓ ∀hasChild.⊥

TBox and ABox

Component	Contains	Statement form	Analogy
TBox (Terminological Box)	General concept inclusions, equivalences	`C ⊑ D`, `C ≡ D`	Database schema
ABox (Assertion Box)	Facts about named individuals	`a : C` (concept assertion), `(a,b) : R` (role assertion)	Database content

GCI (General Concept Inclusion): C ⊑ D means every C is also a D (set-theoretically: Cᴵ ⊆ Dᴵ).
Concept equivalence: C ≡ D ⇔ C ⊑ D and D ⊑ C.
A knowledge base K = (T, A) is what one usually calls an ontology.

Reasoning tasks in DL

The standard reasoning tasks the algorithms below implement:

Task	Question	Reduction
Satisfiability of C	Is there a model in which Cᴵ ≠ ∅?	Direct via Tableaux
Subsumption C ⊑ D	Is every C also a D?	Test if `C ⊓ ¬D` is unsatisfiable
Equivalence C ≡ D	Are C and D necessarily the same set?	C ⊑ D and D ⊑ C
Disjointness	Is C ⊓ D unsatisfiable?	Test unsatisfiability of `C ⊓ D`
Instance checking	Is `a : C` entailed by K?	Test unsatisfiability of K ∪ {a : ¬C}
Consistency of K	Does K have any model?	Tableaux on the whole KB

⭐ Everything reduces to (un)satisfiability — that is why the Tableaux algorithm is the workhorse.

Tableaux Algorithm (Inference)

A model-construction procedure: given a concept C, try to build a finite interpretation (a tree of “individuals” with concept labels) in which C is non-empty.
Tests satisfiability of concept descriptions.
All other DL reasoning tasks reduce to (un)satisfiability — see table above.
Step 1: convert concept to Negation Normal Form (NNF) — push ¬ inward so only atomic concepts get negated.
Step 2: apply expansion rules for ⊓, ⊔, ∃, ∀ until either every branch contains a clash (an explicit contradiction A and ¬A on the same individual) — then unsatisfiable — or some branch is complete and clash-free — then satisfiable.

See the pseudocode and the worked example below.

Two families of DL reasoning algorithms

The WiSe 2024_25 slides explicitly contrast two families of subsumption algorithms:

Algorithm family	Approach	Strengths	Weaknesses	Typical use
Structural Subsumption	Syntactic comparison of concept descriptions in normal form (e.g. compare two `∀R.C ⊓ ∃S.D` patterns directly)	Very fast (polynomial in many cases); easy to implement	Only works for weak DLs (e.g. FL₀, EL); fails as soon as full negation, disjunction, or number restrictions are added	Lightweight ontologies, OWL EL profile
Tableau-based (the workhorse described above)	Model construction: try to build a model of `C ⊓ ¬D`; if impossible, then `C ⊑ D`	General technique — works for the full ALC family up to SROIQ. Decidable for ALC.	Worst case exponential in concept size	Full OWL DL reasoners (HermiT, Pellet, Konclude)

⭐ In an exam: if asked to “name the two main types of DL inference algorithms” → structural subsumption (cheap, for weak DLs) and tableaux (general, decidable for ALC). The hub here covers tableaux in detail because that’s the workhorse; structural subsumption is mentioned for completeness.

Open vs. Closed World Assumption — external background

⚠️ Not covered explicitly in the KR I/II slides — included here because it shows up in exam Q120–122 and is essential context for understanding what DL/OWL inference actually means.

Assumption	What “not stated” means	Where used
Closed World Assumption (CWA)	False	STRIPS planning, relational databases, Prolog (with NAF)
Open World Assumption (OWA)	Unknown	Situation Calculus, Description Logics, OWL, Semantic Web

Practical consequence in DL/OWL. If the KB does not assert Alice : Parent, you may not conclude Alice : ¬Parent. You can only conclude what is entailed by the KB.

OWL (Web Ontology Language)

OWL is the W3C standard ontology language for the semantic web. It is built on top of description logics. The expressivity profile of an OWL dialect is described by stacking DL “extension letters”:

Letter	Adds
S	ALC + transitive roles
H	role Hierarchies (`R ⊑ S`)
O	nominals (`{a}` — singleton concepts from individuals)
I	Inverse roles (`R⁻`)
N	unqualified Number restrictions (`≥ n R`, `≤ n R`)
Q	Qualified number restrictions (`≥ n R.C`)
(D)	concrete datatypes (strings, ints, …)

So e.g. ALCH = ALC plus role hierarchy, SHOIN(D) ≈ OWL DL, SROIQ(D) ≈ OWL 2 DL.

⚠️ The Session 06/07 slides only list the extension letters (U, C, O, E, N, H and the family above). The OWL Lite / OWL DL / OWL Full trichotomy is not in the lecture slides — it is part of the W3C standard and external background. Don’t cite slide numbers for it.

Allen’s Tense Logic (Temporal Reasoning)

Reasoning about time intervals (not points). The 7 base relations plus their 6 inverses give 13 distinct relations (EQUAL is symmetric, so its inverse is itself).

Base relation	Notation	Inverse
before	b	after (bi)
meets	m	met-by (mi)
overlaps	o	overlapped-by (oi)
starts	s	started-by (si)
finishes	f	finished-by (fi)
during	d	contains (di)
equal	=	= (symmetric — no separate inverse)

⇒ 6 pairs × 2 + 1 = 13 relations.

Composition table. Given R₁(I₁, I₂) and R₂(I₂, I₃), what relations can hold between I₁ and I₃? The composition table lists, for every pair of base relations, the set of possible composed relations. Used to propagate constraints in a temporal CSP — directly analogous to AC-3 (see [[#4. Allen’s composition-table propagation (temporal AC-3)|algorithm #4]]).

RCC-8 (Region Connection Calculus)

8 jointly-exhaustive pairwise-disjoint topological relations between regions (not points), based on the connection predicate C(x, y):

Relation	Meaning
DC	Disconnected
EC	Externally Connected (touch but don’t overlap)
PO	Partial Overlap
TPP	Tangential Proper Part (x inside y, touching boundary)
TPPi	inverse of TPP
NTPP	Non-Tangential Proper Part (strictly inside)
NTPPi	inverse of NTPP
EQ	Equal

No metric needed — purely topological. Like Allen, RCC-8 has a composition table used for constraint propagation.

Formulas & Notation

Symbol	Meaning
C ⊑ D	C is subsumed by D (every C is D)
C ≡ D	Concept equivalence
C ⊓ D, C ⊔ D, ¬C	Intersection, union, complement
⊤, ⊥	Top (universe), bottom (empty)
a : C	Individual `a` is an instance of concept C
(a,b) : R	`a` and `b` stand in role relation R
∃R.C	Existential restriction (some R-filler is C)
∀R.C	Value restriction (all R-fillers are C)
Cᴵ, Rᴵ, Δᴵ	Interpretation of concept / role / domain
K = (T, A)	Knowledge base = TBox + ABox
NNF	Negation Normal Form (negations only on atomic)
clash	`A(x)` and `¬A(x)` for some individual `x`

Common Exam Traps ⚠️

TBox ≠ ABox: TBox = general schema rules about classes; ABox = specific facts about individuals.
OWA vs. CWA: DLs and OWL use OWA — absence of info does NOT mean it’s false. Critical difference from databases/STRIPS.
C ⊑ D means “every C is a D” — NOT “D is a subset of C”. Direction matters!
ALC has no role hierarchy — that requires adding the H extension (giving ALCH). Don’t say “ALC + H = SROIQ” — SROIQ has far more (S, R, O, I, Q).
ALC name = “Attributive Concept Language with Complements” (slide 31), not “Attributive Language with Complement”.
Tableaux proves (un)satisfiability, not truth in a specific model. Subsumption C ⊑ D is tested by checking if C ⊓ ¬D is unsatisfiable.
∀R.C vacuous-truth trap: ∀R.C(x) is trivially true if x has no R-successors at all. So Childless ≡ Person ⊓ ∀hasChild.⊥ correctly includes people with no children. This costs students points every exam.
Allen relations: 7 base + 6 inverses = 13 total (EQUAL is symmetric).
RCC-8 is topological, not metric — uses regions and the C(x,y) predicate.
OWL Lite / DL / Full is not in the slides — the slides only list the DL extension letters. Cite the letters, not the dialect names, when referencing slide material.

Quick comparison table

Aspect	Classical Logic (FOL)	Description Logic (ALC)
Focus	Arbitrary statements over individuals & relations	Categories (concepts) and roles
Semantics	Model-theoretic (Tarski)	Model-theoretic over (Δᴵ, ·ᴵ)
Variables	Free use of variables, quantifiers	No explicit variables in concept syntax
Reasoning	Resolution / theorem provers (semi-decidable in general)	Tableaux — decidable for ALC
Expressivity	Very high (undecidable in general)	Deliberately restricted to stay decidable
World assumption	Either CWA or OWA, depending on use	OWA (always)
Use case	Mathematical formalisation	Ontologies, semantic web (OWL)

Visualisations (Python)

Three Pyodide figures that make the trickiest parts of the KR module visual: Allen’s 13 temporal interval relations, RCC-8’s 8 topological region relations, and the TBox / ABox split of an ontology. Render each toggle and read the explanation underneath.

🐍 Figure — Allen's 13 temporal interval relations

import micropip
await micropip.install("matplotlib")
 
import matplotlib.pyplot as plt
from matplotlib.patches import FancyBboxPatch
 
# Each relation is described as: (label, A-interval (x0, x1), B-interval (x0, x1))
# The 13 relations are 6 base + 6 inverses + EQUAL (symmetric).
RELATIONS = [
    ("BEFORE  (b)",       (0.5, 2.0), (3.0, 4.5)),
    ("AFTER  (bi)",       (3.0, 4.5), (0.5, 2.0)),
    ("MEETS  (m)",        (0.5, 2.5), (2.5, 4.5)),
    ("MET-BY  (mi)",      (2.5, 4.5), (0.5, 2.5)),
    ("OVERLAPS  (o)",     (0.5, 3.0), (2.0, 4.5)),
    ("OVERLAPPED-BY (oi)",(2.0, 4.5), (0.5, 3.0)),
    ("STARTS  (s)",       (0.5, 2.5), (0.5, 4.5)),
    ("STARTED-BY  (si)",  (0.5, 4.5), (0.5, 2.5)),
    ("FINISHES  (f)",     (2.5, 4.5), (0.5, 4.5)),
    ("FINISHED-BY  (fi)", (0.5, 4.5), (2.5, 4.5)),
    ("DURING  (d)",       (1.5, 3.5), (0.5, 4.5)),
    ("CONTAINS  (di)",    (0.5, 4.5), (1.5, 3.5)),
    ("EQUAL  (=)",        (0.5, 4.5), (0.5, 4.5)),
]
 
A_COLOR = "#e74c3c"   # interval A
B_COLOR = "#3498db"   # interval B
 
fig, axes = plt.subplots(5, 3, figsize=(13, 11))
axes = axes.flatten()
 
for ax, (label, (ax0, ax1), (bx0, bx1)) in zip(axes, RELATIONS):
    # Interval A on y=0.7, Interval B on y=0.3
    ax.add_patch(FancyBboxPatch((ax0, 0.6), ax1 - ax0, 0.18,
                                boxstyle="round,pad=0.02",
                                fc=A_COLOR, ec="black", lw=1.2))
    ax.add_patch(FancyBboxPatch((bx0, 0.22), bx1 - bx0, 0.18,
                                boxstyle="round,pad=0.02",
                                fc=B_COLOR, ec="black", lw=1.2))
    ax.text(ax0 - 0.15, 0.69, "A", ha="right", va="center",
            fontsize=9, fontweight="bold", color=A_COLOR)
    ax.text(bx0 - 0.15, 0.31, "B", ha="right", va="center",
            fontsize=9, fontweight="bold", color=B_COLOR)
    ax.set_xlim(-0.5, 5.2); ax.set_ylim(0, 1)
    ax.set_title(label, fontsize=10, fontweight="bold")
    ax.axis("off")
 
# Last spare cell: empty (we used 13 of 15 slots)
for spare in axes[len(RELATIONS):]:
    spare.axis("off")
 
fig.suptitle("Allen's Interval Algebra — the 13 distinct relations between A and B",
             fontsize=13, fontweight="bold")
plt.tight_layout(rect=[0, 0, 1, 0.96]); plt.show()

What this figure shows. Every cell illustrates one of the 13 Allen relations by placing interval A (red, top) above interval B (blue, bottom) on a shared timeline. The 6 base relations (b, m, o, s, f, d) are paired with their 6 inverses (bi, mi, oi, si, fi, di). EQUAL is the symmetric one — it is its own inverse, which is why the total is 13 and not 14.

How to read it.

BEFORE: A entirely to the left of B with a gap.
MEETS: A’s right endpoint = B’s left endpoint (no gap, no overlap).
OVERLAPS: A starts before B starts and ends inside B.
STARTS: A and B share the same left endpoint, A ends earlier.
FINISHES: A and B share the same right endpoint, A starts later.
DURING: A is strictly inside B (both endpoints strictly inside).
EQUAL: same interval.

The “inverse” of each relation just swaps the roles of A and B. This is exactly the table on lines 164-173 of this note, made concrete.

🐍 Figure — RCC-8 spatial relations between two regions

import micropip
await micropip.install("matplotlib")
 
import matplotlib.pyplot as plt
from matplotlib.patches import Circle
 
A_COLOR = "#e74c3c"  # region X (red, semi-transparent)
B_COLOR = "#3498db"  # region Y (blue, semi-transparent)
 
# Each relation: label, (x_center, y_center, radius) for X and for Y
RELATIONS = [
    ("DC — Disconnected",
        (-1.2, 0, 0.8), (1.2, 0, 0.8)),
    ("EC — Externally Connected",
        (-0.8, 0, 0.8), (0.8, 0, 0.8)),
    ("PO — Partial Overlap",
        (-0.5, 0, 0.9), (0.5, 0, 0.9)),
    ("EQ — Equal",
        (0, 0, 0.9),    (0, 0, 0.9)),
    ("TPP — Tangential Proper Part (X in Y)",
        (-0.4, 0, 0.5), (0, 0, 0.9)),
    ("TPPi — inverse of TPP (Y in X)",
        (0, 0, 0.9),    (-0.4, 0, 0.5)),
    ("NTPP — Non-Tangential Proper Part",
        (0, 0, 0.4),    (0, 0, 0.95)),
    ("NTPPi — inverse of NTPP",
        (0, 0, 0.95),   (0, 0, 0.4)),
]
 
fig, axes = plt.subplots(2, 4, figsize=(14, 7))
axes = axes.flatten()
 
for ax, (label, (xa, ya, ra), (xb, yb, rb)) in zip(axes, RELATIONS):
    # Draw Y first (often the larger / container)
    ax.add_patch(Circle((xb, yb), rb, facecolor=B_COLOR, alpha=0.45,
                        edgecolor="#1f5d8c", lw=2, zorder=1))
    ax.add_patch(Circle((xa, ya), ra, facecolor=A_COLOR, alpha=0.55,
                        edgecolor="#8a2a1f", lw=2, zorder=2))
    # Centre labels (only if circles are well separated)
    ax.text(xa, ya + ra + 0.15, "X", ha="center", va="bottom",
            fontsize=10, fontweight="bold", color="#8a2a1f")
    ax.text(xb, yb - rb - 0.15, "Y", ha="center", va="top",
            fontsize=10, fontweight="bold", color="#1f5d8c")
    ax.set_xlim(-2.4, 2.4); ax.set_ylim(-1.8, 1.8)
    ax.set_aspect("equal")
    ax.set_title(label, fontsize=10, fontweight="bold")
    ax.axis("off")
 
fig.suptitle("RCC-8 — the 8 jointly-exhaustive pairwise-disjoint topological relations",
             fontsize=13, fontweight="bold")
plt.tight_layout(rect=[0, 0, 1, 0.95]); plt.show()

What this figure shows. The 8 RCC-8 relations between two regions X (red) and Y (blue), drawn as circle pairs. RCC-8 is purely topological — no distances, no shapes matter, only the connection structure.

How to read it.

DC: regions don’t touch.
EC: boundaries touch but interiors are disjoint.
PO: regions properly overlap (each has parts inside and outside the other).
EQ: regions coincide.
TPP / TPPi: one region is inside the other AND touches the outer boundary (tangential).
NTPP / NTPPi: strictly inside (no boundary touch).

The 8 relations are JEPD (Jointly Exhaustive, Pairwise Disjoint): exactly one of them holds between any two regions. Like Allen, RCC-8 has a composition table used by the same constraint-propagation algorithm ([[#4. Allen’s composition-table propagation (temporal AC-3)|algorithm #4]]).

🐍 Figure — Ontology = TBox + ABox (schema + facts)

import micropip
await micropip.install("matplotlib")
 
import matplotlib.pyplot as plt
from matplotlib.patches import FancyBboxPatch, Circle, FancyArrowPatch
 
fig, ax = plt.subplots(figsize=(11, 8))
 
# --- TBox region (top) ---
ax.add_patch(FancyBboxPatch((0.3, 5.0), 9.4, 3.4,
                            boxstyle="round,pad=0.1",
                            fc="#fdf6e3", ec="#cba135", lw=2, zorder=1))
ax.text(5.0, 8.15, "TBox  (Terminological — schema)",
        ha="center", va="center", fontsize=13, fontweight="bold",
        color="#8a6d1f")
 
# Concepts as rectangles
CONCEPTS = {
    "Person":  (5.0, 7.2),
    "Student": (3.0, 5.8),
    "Teacher": (7.0, 5.8),
}
CONCEPT_COLOR = "#f1c40f"
 
for name, (x, y) in CONCEPTS.items():
    ax.add_patch(FancyBboxPatch((x - 0.75, y - 0.3), 1.5, 0.6,
                                boxstyle="round,pad=0.05",
                                fc=CONCEPT_COLOR, ec="black", lw=1.5, zorder=2))
    ax.text(x, y, name, ha="center", va="center",
            fontsize=11, fontweight="bold", zorder=3)
 
# GCI arrows: Student ⊑ Person, Teacher ⊑ Person
for (cx, cy) in [CONCEPTS["Student"], CONCEPTS["Teacher"]]:
    px, py = CONCEPTS["Person"]
    ax.annotate("", xy=(px, py - 0.32), xytext=(cx, cy + 0.32),
                arrowprops=dict(arrowstyle="-|>", color="#444",
                                lw=1.8, mutation_scale=15),
                zorder=2)
 
ax.text(3.85, 6.55, "⊑", ha="center", va="center", fontsize=14,
        fontweight="bold", color="#444")
ax.text(6.15, 6.55, "⊑", ha="center", va="center", fontsize=14,
        fontweight="bold", color="#444")
 
# TBox axiom captions
ax.text(5.0, 4.85,
        r"Student $\sqsubseteq$ Person     Teacher $\sqsubseteq$ Person",
        ha="center", va="top", fontsize=10, style="italic", color="#7d6517")
 
# --- ABox region (bottom) ---
ax.add_patch(FancyBboxPatch((0.3, 0.3), 9.4, 3.4,
                            boxstyle="round,pad=0.1",
                            fc="#eaf6ff", ec="#3a7fb8", lw=2, zorder=1))
ax.text(5.0, 3.45, "ABox  (Assertional — facts)",
        ha="center", va="center", fontsize=13, fontweight="bold",
        color="#205a85")
 
# Individuals as circles
INDIVIDUALS = {
    "mary": (3.0, 2.0),
    "john": (7.0, 2.0),
}
IND_COLOR = "#3498db"
 
for name, (x, y) in INDIVIDUALS.items():
    ax.add_patch(Circle((x, y), 0.45, fc=IND_COLOR, ec="black",
                        lw=1.5, zorder=2))
    ax.text(x, y, name, ha="center", va="center",
            fontsize=11, fontweight="bold", color="white", zorder=3)
 
# Optional role assertion: (mary, john) : knows
ax.annotate("", xy=(6.55, 2.0), xytext=(3.45, 2.0),
            arrowprops=dict(arrowstyle="->", color="#205a85",
                            lw=1.5, mutation_scale=15), zorder=2)
ax.text(5.0, 2.18, "knows", ha="center", va="bottom",
        fontsize=9, style="italic", color="#205a85")
 
# ABox assertion captions
ax.text(5.0, 0.85,
        r"mary : Student     john : Teacher     (mary, john) : knows",
        ha="center", va="top", fontsize=10, style="italic", color="#205a85")
 
# --- instance-of edges crossing the TBox/ABox boundary ---
# mary -> Student
ax.annotate("", xy=CONCEPTS["Student"], xytext=(INDIVIDUALS["mary"][0],
                                                 INDIVIDUALS["mary"][1] + 0.5),
            arrowprops=dict(arrowstyle="->", color="#888", lw=1.3,
                            linestyle="dashed", mutation_scale=12), zorder=2)
# john -> Teacher
ax.annotate("", xy=CONCEPTS["Teacher"], xytext=(INDIVIDUALS["john"][0],
                                                 INDIVIDUALS["john"][1] + 0.5),
            arrowprops=dict(arrowstyle="->", color="#888", lw=1.3,
                            linestyle="dashed", mutation_scale=12), zorder=2)
ax.text(2.45, 4.0, "instance-of", ha="center", va="center",
        fontsize=9, color="#666", style="italic", rotation=72)
ax.text(7.55, 4.0, "instance-of", ha="center", va="center",
        fontsize=9, color="#666", style="italic", rotation=-72)
 
# Title
ax.set_title("Ontology = TBox (schema) + ABox (facts)\n"
             "rectangles = concepts · circles = individuals · "
             "solid arrows = ⊑ · dashed = instance-of",
             fontsize=12, fontweight="bold")
 
ax.set_xlim(0, 10); ax.set_ylim(0, 9)
ax.set_aspect("equal"); ax.axis("off")
plt.tight_layout(); plt.show()

What this figure shows. A complete tiny ontology K = (T, A) for a university domain.

TBox (yellow, top). Schema-level knowledge — the concepts (Person, Student, Teacher) as rectangles, with GCI arrows Student ⊑ Person and Teacher ⊑ Person. This is what a database analogy would call the schema.

ABox (blue, bottom). Fact-level knowledge — two individuals (mary, john) as circles, plus a role assertion (mary, john) : knows. This is what the database analogy calls the rows.

Crossing arrows (dashed). Instance-of — mary : Student and john : Teacher. These are the ABox’s concept assertions. Note that from mary : Student and the TBox GCI Student ⊑ Person, a DL reasoner entails mary : Person even though it was never asserted — that is the value of the TBox.

Why this matters. The TBox/ABox split is the single most-tested concept on the KR exam. If a statement uses a named individual (mary, john), it’s ABox. If it talks about all members of a class (Student ⊑ Person), it’s TBox.

ALGORITHMS (full reference) ⭐

Pseudocode + intuition + complexity for the reasoning algorithms behind the KR module. All DL reasoning tasks reduce to (un)satisfiability via the Tableaux algorithm — so #1 is the workhorse and #2, #3 are reductions to it. #4 is the temporal-CSP analogue for Allen’s logic.

1. Tableaux satisfiability test

Goal. Decide whether a concept C₀ (optionally w.r.t. a TBox T) is satisfiable, i.e. whether some interpretation makes C₀ᴵ ≠ ∅.

Idea. Try to build a finite “completion forest” — a tree of (would-be) individuals labelled with concept assertions — that satisfies C₀. If every attempt clashes, C₀ is unsatisfiable.

TABLEAUX-SAT(C₀):
    C₀ ← to-NNF(C₀)                              # push negations to atoms
    forest ← single node x with L(x) = { C₀ }    # L = label = set of concepts
    repeat:
        pick a non-clashing branch and an applicable rule:
 
        # ⊓-rule
        if (C ⊓ D) ∈ L(x) and {C, D} ⊄ L(x):
            L(x) ← L(x) ∪ { C, D }
 
        # ⊔-rule (non-deterministic → branching)
        if (C ⊔ D) ∈ L(x) and {C, D} ∩ L(x) = ∅:
            branch:  L(x) ← L(x) ∪ { C }
            branch:  L(x) ← L(x) ∪ { D }
 
        # ∃-rule (creates a new individual)
        if (∃R.C) ∈ L(x) and no R-successor y with C ∈ L(y):
            create fresh y;  add edge (x, y) labelled R
            L(y) ← { C }
 
        # ∀-rule
        if (∀R.C) ∈ L(x) and (x, y) is an R-edge and C ∉ L(y):
            L(y) ← L(y) ∪ { C }
 
        # GCI rule (only if a TBox is involved)
        for every GCI  C ⊑ D ∈ T:
            for every node x:
                L(x) ← L(x) ∪ { ¬C ⊔ D }         # in NNF
 
    until no rule applies on any branch.
 
    if some branch is clash-free (no { A, ¬A } in any L(x)):
        return SATISFIABLE
    else:
        return UNSATISFIABLE

Clash. A node x whose label contains both A and ¬A for some atomic A (or contains ⊥).

Termination. For pure ALC without GCIs, tableaux terminates because labels can only grow with sub-concepts of C₀ (finitely many). With GCIs you need blocking (don’t expand a node whose label is a subset of an ancestor’s) to guarantee termination.

Complexity. Concept satisfiability in ALC is PSPACE-complete. With general TBoxes (GCIs) it becomes EXPTIME-complete.

2. Subsumption via unsatisfiability (`C ⊑ D`)

Reduction. C ⊑ D holds w.r.t. T iff C ⊓ ¬D is unsatisfiable w.r.t. T.

SUBSUMES(C, D, T):
    return  TABLEAUX-SAT( to-NNF(C ⊓ ¬D), T )  ==  UNSATISFIABLE

Intuition. “Every C is a D” ⇔ “there is no C that fails to be a D” ⇔ “the set of things that are C but not D is empty”.

Equivalence C ≡ D is two subsumption tests: SUBSUMES(C, D) ∧ SUBSUMES(D, C).

Disjointness of C and D: TABLEAUX-SAT(C ⊓ D) = UNSATISFIABLE.

3. Instance checking (`a : C`)

Reduction. Given K = (T, A) and an individual a, is a : C entailed by K?
⇔ Is K ∪ {a : ¬C} inconsistent?

INSTANCE-CHECK(K, a, C):
    K' ← K with ABox extended by { a : ¬C }
    return  TABLEAUX-SAT(K')  ==  UNSATISFIABLE

The Tableaux algorithm runs on the entire KB (TBox + ABox), starting with the labels given by the ABox assertions.

4. Allen’s composition-table propagation (temporal AC-3)

Setting. A temporal CSP: nodes = intervals, edges = sets of Allen relations that might hold (a disjunction, e.g. R(I₁, I₂) ∈ { before, meets, overlaps }).

Goal. Propagate constraints via the composition table so that every triple (I₁, I₂, I₃) is path-consistent. Exactly analogous to AC-3 from CSP, but the “revise” step uses the Allen composition table ∘.

ALLEN-PROPAGATE(network):
    queue ← all triples (i, j, k) of distinct intervals
 
    while queue not empty:
        (i, j, k) ← queue.pop()
 
        # R(i, k) must be consistent with  R(i, j) ∘ R(j, k)
        new_ik ← R(i, k) ∩ ( R(i, j) ∘ R(j, k) )    # use composition table
 
        if new_ik = ∅:
            return INCONSISTENT
        if new_ik ⊊ R(i, k):
            R(i, k) ← new_ik
            for every interval m ∉ {i, k}:
                queue.push((m, i, k))
                queue.push((i, k, m))
 
    return CONSISTENT (path-consistent)

REVISE step. R(i, k) ← R(i, k) ∩ ( R(i, j) ∘ R(j, k) ), where ∘ is composition (look up each pair (r₁, r₂) ∈ R(i,j) × R(j,k) in the table, union the results).

Cost. O(n³ · |B|²) in the worst case for n intervals and base relation set B (|B| = 13 for Allen).

Caveat. Path consistency is necessary but not sufficient for global consistency over the full set of 13 relations — the general satisfiability problem for Allen’s algebra is NP-complete.

RCC-8 analogue. Same algorithm; just swap the Allen composition table for the RCC-8 one and use the 8 base relations.

Worked examples

Example A — Tableaux on a small concept

Goal: show that C₀ := A ⊓ ∃R.B ⊓ ∀R.¬B is unsatisfiable.

NNF — already in NNF.
Start: node x, L(x) = { A, ∃R.B, ∀R.¬B }.
⊓-rule already applied (label contains all three conjuncts).
∃-rule on ∃R.B: create new node y, edge R(x, y), L(y) = { B }.
∀-rule on ∀R.¬B: for the R-successor y, add ¬B to L(y) ⇒ L(y) = { B, ¬B }.
Clash on y (contains B and ¬B).
Only this branch existed (no ⊔ ever introduced branching), so the tableau is closed.

Conclusion. C₀ is unsatisfiable. Therefore the subsumption (A ⊓ ∃R.B) ⊑ ∃R.B is trivially true (which it is), and more interestingly: A ⊓ ∃R.B ⊑ ¬∀R.¬B.

Example B — A satisfiable concept

C₀ := ∃R.A ⊓ ∀R.(A ⊔ B).

Node x, L(x) = { ∃R.A, ∀R.(A ⊔ B) }.
∃-rule → create y with L(y) = { A }, edge R(x, y).
∀-rule on ∀R.(A ⊔ B): add A ⊔ B to L(y) ⇒ L(y) = { A, A ⊔ B }.
⊔-rule branches; the branch L(y) = { A, A ⊔ B, A } is clash-free and complete.

Conclusion. C₀ is satisfiable. A witness model: Δ = {x, y}, R = {(x, y)}, Aᴵ = {y}.

Example C — Allen composition

Given:

R(I₁, I₂) = { before (b) }
R(I₂, I₃) = { before (b) }

Composition table lookup: b ∘ b = { b } (if I₁ is before I₂, and I₂ is before I₃, then I₁ is before I₃).

So R(I₁, I₃) ← R(I₁, I₃) ∩ {b}. If the initial constraint was R(I₁, I₃) = { all 13 }, it tightens to { b }. If it had been { after }, intersection = ∅ ⇒ network inconsistent.

A less degenerate case: b ∘ d (before then during). Then I₁ < I₂ and I₂ ⊂ I₃. The composed set is { b, m, o, s, d } — I₁ could be before, meet, overlap, start, or be during I₃, depending on where I₃ extends.

Original atomic note — Description Logics (DL)

The original short atomic note about Description Logics is preserved here so its unique framing (database analogy, “where DLs are challenged”, real-world deployments) isn’t lost.

Description Logics (DL) are a family of formal knowledge representation languages designed for describing categories and their relationships. They’re the formal foundation of OWL (the Semantic Web ontology language) and are used in medical ontologies (SNOMED CT), enterprise data integration, and configuration systems.

DL is a decidable fragment of First-Order Logic. It trades expressivity for tractability — you can’t say everything FOL can, but the things you can say are guaranteed to have terminating reasoning algorithms.

The basic language: ALC (short version)

ALC = Attributive Language with Complement. The minimal DL with negation. Concepts in ALC are built from:

Constructor	Syntax	Reads as	Example
Atomic concept	`A`	A class	`Student`
Top	`⊤`	Everything	the universe
Bottom	`⊥`	Nothing	the empty set
Negation	`¬C`	Not C	`¬Student`
Intersection	`C ⊓ D`	C and D	`Student ⊓ Person`
Union	`C ⊔ D`	C or D	`Student ⊔ Lecturer`
Existential restriction	`∃R.C`	has some R that is C	`∃teaches.Course`
Universal restriction	`∀R.C`	all R relations go to C	`∀hasChild.Doctor`

Larger DLs (ALCN, SHIQ, SROIQ — the OWL 2 DL fragment) add number restrictions (≥3 hasChild), role hierarchies, inverse roles, transitive roles, etc.

TBox vs. ABox — database analogy

	TBox (Terminological Box)	ABox (Assertion Box)
What it stores	General statements about concepts/classes	Statements about specific individuals
Examples	`Student ⊑ Person`, `Mother ≡ Female ⊓ ∃hasChild.⊤`	`alice : Student`, `(alice, cs100) : teaches`
Database analogy	Schema	Data / rows
Reasoning task	Subsumption (is C ⊑ D?), Classification	Instance check (is `a : C`?), Realization
Updates frequency	Rarely (you fix the schema)	Often (you add new facts)

Rule of thumb: if it uses a variable / individual name (like alice), it’s ABox. If it talks about all members of a class (like Student ⊑ Person), it’s TBox.

OWA — the big mental shift (intuitive framing)

DLs use OWA: absence of information ≠ negation. If the KB doesn’t say Alice teaches CS500, you cannot conclude that Alice does not teach CS500 — only that you don’t know. To assert non-teaching, you must add it explicitly.

Compare:

Databases / Prolog / STRIPS: Closed World (CWA) — “what’s not asserted is false.” Convenient but loses information about uncertainty.
DL / OWL: Open World — “what’s not asserted is unknown.” More accurate for the Semantic Web (the world is bigger than your KB).

The four key reasoning tasks (cheat-sheet form)

Task	Question	TBox or ABox?
Subsumption	Does TBox entail C ⊑ D?	TBox
Classification	Build the full concept hierarchy from the TBox	TBox
Instance Check	Does the KB entail a : C?	ABox (uses both)
Realization	What’s the most specific concept(s) that `a` belongs to?	ABox (uses both)
Consistency	Is the KB satisfiable at all?	Both

These are all decidable for ALC (in EXPTIME for combined complexity). Tableau algorithms solve them.

Where DLs are used today

OWL (Web Ontology Language) — W3C standard, the entire Semantic Web is built on DL. SPARQL endpoints (DBpedia, Wikidata) use DL reasoning.
SNOMED CT — the world’s largest medical ontology (~360,000 concepts). Used by NHS, US Medicare, healthcare systems globally.
Gene Ontology (GO) — bioinformatics standard for describing gene functions, used in every major genomics database.
Enterprise data integration — companies use DLs to align schemas across databases (e.g. merging customer records from CRM systems).
Configurator systems — product configurators (cars, computers) use DL reasoning to check which option combinations are valid.
Pellet, HermiT, Fact++, ELK — production DL reasoners deployed in industry tools (Protégé editor, OWLAPI).

Where DLs are challenged — and by what

Domain	DLs being replaced by …	Why
Open-domain QA over text	LLMs (GPT-4, Claude)	LLMs don’t need a formal ontology — they “know” from training data; trade formal rigor for coverage
Schema mapping / data integration	Vector embeddings + LLMs	Semantic similarity in embedding space replaces formal ontology alignment
Knowledge graph completion	Graph neural networks (GNNs), KG embeddings	TransE, RotatE, etc. learn embeddings that predict missing edges — no axioms required
Enterprise knowledge bases	RAG (Retrieval-Augmented Generation)	Combine LLMs with vector databases instead of hand-curated ontologies

Where DLs still win: when you need provable reasoning (medical, legal, safety-critical) where “the model believes it” isn’t acceptable. LLMs are great at the 80% but cannot replace formal ontologies in regulated domains.

Brain Online

Explorer

Description Logics