Description Logic – Exam-style Problems and Last-minute Checklist¶

Part 6 of the DL revision notes:
- typical problem types for the second class test
- solution templates (step-by-step skeletons, no full answers)
- a concise last-minute checklist

6.1 Typical problem types¶

From the lecture content and style, the most natural exam questions around DL + tableau are:

KB consistency
Given a TBox \(T\) and ABox \(A\), decide whether the knowledge base \(K = (T, A)\) is consistent.
Method: full 6-step tableau.
Concept coherence
Given a concept \(C\) and TBox \(T\), decide whether \(C\) is coherent (satisfiable) w.r.t. \(T\) (or \(K\)).
Method: reduction to consistency + tableau.
Entailment of assertions
Given \(K = (T, A)\) and some assertion (e.g. \(a : C\)), decide whether \(K \models a : C\).
Method: reduction to consistency + tableau.
(Possibly) Subsumption
Given \(T\) and concepts \(C, D\), decide whether \(T \models C \sqsubseteq D\).
Method: reduction to coherence/consistency (e.g. \(C \sqcap \neg D\) unsatisfiable).
Short theory questions
Define or explain in words:
- ABox / TBox / knowledge base
- consistency / coherence / entailment
- purpose of tableau
Possibly: “explain how to test entailment using the tableau method.”

6.2 Template: checking consistency of a KB with tableau¶

Problem pattern¶

Given a knowledge base \(K = (T, A)\). Decide whether \(K\) is consistent.

Solution template¶

Write down the input clearly
List the TBox axioms (subsumptions/equivalences) in a clean form.
List the ABox assertions: concept and role assertions.
Step 1 – Eliminate subsumptions in TBox
For each axiom of the form \(A \sqsubseteq C\),
rewrite using a star-concept:
\(A \equiv C \sqcap A^{*}\).
Replace subsumptions so that the TBox consists only of equivalences \(A \equiv \dots\).
Step 2 – Expand (unfold) the TBox
Using the assumption that the TBox is acyclic:
- iteratively replace defined concepts by their definitions,
- until every definition is written only in terms of primitive concepts and role restrictions.
Result: an “expanded” TBox where definitions are fully unfolded.
Step 3 – Eliminate defined concepts in the ABox
For each ABox assertion \(a : A\) where \(A\) is a defined concept:
- replace it by \(a : C\), where \(A \equiv C\) in the expanded TBox.
Repeat until no defined concept names remain in the ABox.
From now on, you can ignore the TBox: all necessary information is in the ABox.
Step 4 – Convert ABox to Negation Normal Form (NNF)
For each assertion \(a : \varphi\), push negations inwards so they only apply to atomic concepts.
Use the equivalences:
- \(\neg (C \sqcap D) \equiv \neg C \sqcup \neg D\)
- \(\neg (C \sqcup D) \equiv \neg C \sqcap \neg D\)
- \(\neg \neg C \equiv C\)
- \(\neg \forall r.C \equiv \exists r.\neg C\)
- \(\neg \exists r.C \equiv \forall r.\neg C\)
The output is an ABox whose concepts are in NNF.
Step 5 – Apply completion rules to build a tableau
Start from the (NNF) ABox as the root node of your tableau.
Repeat:
- If possible, apply the ⊥-rule (clash detection) to close branches early.
- Apply ∧-rule: if \(a : C \sqcap D\), add both \(a : C\) and \(a : D\).
- Apply ∃-rule: if \(a : \exists r.C\), create a fresh individual \(b\) with \((a,b) : r\) and \(b : C\).
- Apply ∀-rule: if \(a : \forall r.C\) and \((a,b):r\), add \(b : C\).
- Apply ∨-rule (branching): if \(a : C \sqcup D\), split into two branches:
- one branch with \(a : C\),
- one branch with \(a : D\).
Stop a branch when:
- a clash is found → mark the branch closed,
- or no more rules are applicable → branch is open (saturated).
Step 6 – Inspect leaves and conclude
If all branches are closed:
- the ABox (and hence the original \(K\)) is inconsistent.
If at least one branch is open:
- the ABox (and \(K\)) is consistent.
Write a clear conclusion
“Since there exists an open branch, the knowledge base \(K\) is consistent.”
or “Since every branch closes with a clash, the knowledge base \(K\) is inconsistent.”

6.3 Template: checking coherence of a concept¶

Problem pattern¶

Given a TBox \(T\) (and possibly an ABox \(A\)), and a concept \(C\).
Decide whether \(C\) is coherent (satisfiable) w.r.t. \(T\) (or \(K\)).

Solution template¶

State the task in your own words
“We want to know whether it is possible for some individual to be an instance of \(C\), given \(T\) (and \(A\)).”
Build an augmented KB \(K'\)
Introduce a fresh individual name \(a\) (not used elsewhere).
Form a new ABox:
- \(A' = A \cup \{ a : C \}\) (if there is no ABox, use \(A = \emptyset\)).
Define:
- \(K' = (T, A')\).
Explain the reduction
If \(K'\) is consistent, then there exists a model in which some individual (namely \(a\)) is in \(C\).
- So \(C\) is coherent (satisfiable).
If \(K'\) is inconsistent, then no model of \(T\) can contain an instance of \(C\).
- So \(C\) is incoherent (unsatisfiable).
Apply the tableau method to \(K'\)
Use the same 6-step procedure as in 6.2:
- preprocess \(T\) and \(A'\),
- run the tableau on the resulting ABox,
- check open/closed branches.
Conclude about coherence
If tableau finds some open branch:
- \(K'\) is consistent
  → \(C\) is coherent w.r.t. \(T\) (or \(K\)).
If all branches close:
- \(K'\) is inconsistent
  → \(C\) is incoherent (unsatisfiable) w.r.t. \(T\) (or \(K\)).
Write a clear final statement
Example:
- “Since the tableau for \(K'\) has an open branch, the concept \(C\) is coherent w.r.t. \(T\).”
- or “Since all branches close, \(C\) is incoherent w.r.t. \(T\).”

6.4 Template: checking entailment of an assertion¶

Problem pattern¶

Given \(K = (T, A)\) and an assertion \(\varphi\) (often of the form \(a : C\)),
decide whether \(K \models \varphi\).

Standard reduction¶

To test whether \(K \models \varphi\), we try to see whether it is possible that \(K\) is true but \(\varphi\) is false.
If no such model exists, then \(K\) forces \(\varphi\).

Solution template (for \(\varphi = a : C\))¶

State the goal
We want to know whether in every model of \(K\), individual \(a\) is in concept \(C\).
Construct the augmented KB \(K'\)
Add the negation of the assertion to the ABox:
- \(A' = A \cup \{ a : \neg C \}\).
Define:
- \(K' = (T, A')\).
Explain the logic of the reduction
If \(K'\) is consistent, then there exists a model of \(K\) in which \(a : \neg C\) holds.
- So \(K\) does not entail \(a : C\).
If \(K'\) is inconsistent, then no such model exists.
- So \(K\) entails \(a : C\).
Apply tableau to \(K'\)
Again, use the standard 6-step tableau procedure:
- preprocess \(T\) and \(A'\),
- build the tableau and look at branches.
Conclude about entailment
If all branches close:
- \(K'\) is inconsistent
  → \(K \models a : C\).
If there is an open branch:
- \(K'\) is consistent
  → \(K \not\models a : C\).
Write a final explicit answer
“Because the tableau for \(K'\) closes on all branches, \(K \models a : C\).”
or “Because there is an open branch, \(K\) does not entail \(a : C\).”

(The same pattern can be adapted to other assertions, e.g. role assertions \((a,b):r\) or subsumptions.)

6.5 Last-minute exam checklist¶

Use this section as a quick self-test 15–30 minutes before the exam.

6.5.1 Core concepts checklist¶

Can you, in your own words:

Explain the difference between:
TBox (terminological knowledge) and
ABox (assertional knowledge)?
Define a knowledge base \(K = (T, A)\)?
State what it means for \(K\) to be:
consistent,
inconsistent?
Explain what it means for a concept \(C\) to be:
coherent (satisfiable),
incoherent (unsatisfiable) w.r.t. a TBox?
Explain the notion of entailment:
what does \(K \models \varphi\) mean?
State the purpose of the tableau method:
what problem does it solve?

If you cannot answer some of these in 1–2 sentences, revisit Parts 2–3.

6.5.2 Reduction patterns checklist¶

Can you recall (even informally) how to:

Reduce coherence of \(C\) to consistency:
add a fresh \(a : C\) and test consistency?
Reduce entailment \(K \models a : C\) to consistency:
add \(a : \neg C\) and test consistency?
Reduce subsumption \(C \sqsubseteq D\) to coherence/consistency:
consider \(C \sqcap \neg D\) and check whether it is unsatisfiable?

You do not need to write full proofs, but you should remember:

“coherence/entailment/subsumption → build a new KB → test consistency with tableau.”

6.5.3 Tableau procedure checklist¶

Can you:

List the six steps of the tableau method (even briefly)?
eliminate subsumptions in TBox (star concepts),
expand/unfold TBox,
eliminate defined concepts in ABox,
convert ABox to NNF,
apply completion rules,
inspect branches (open/closed) and conclude.
Convert simple ABox assertions to NNF correctly?
Apply each completion rule correctly (on paper):
∧-rule, ∨-rule, ∃-rule, ∀-rule, clash/⊥-rule?
Decide when a branch is:
closed (clash),
open (no clash, saturated)?

If in doubt about a rule, write down a tiny example (1–2 assertions) and test yourself.

6.5.4 Common mistakes to avoid¶

Watch out for:

Forgetting to push negations fully into NNF (e.g. stopping at \(\neg (C \sqcap D)\)).
Mixing up ∃ and ∀ rules:
∃ creates a new individual,
∀ propagates concepts along existing role edges.
Forgetting to apply ∀ to all r-successors of an individual.
Missing a clash:
not noticing both \(a:C\) and \(a:\neg C\) on the same branch.
Stopping tableau too early:
there might still be applicable rules (e.g. a ∀ not yet applied to a new edge).

6.6 Final advice¶

Focus your revision time on:
understanding the definitions,
and being able to execute a small tableau example from start to finish.
Ignore:
Epistemic Logic,
complexity results and extended DLs,
anything the lecturer marked as “not on the class test”.

If you can confidently follow the templates in Sections 6.2–6.4 on a fresh example,
you are in a strong position for the DL part of the second class test.