Description Logic – Consistency, Coherence, Entailment and Tableau¶

This file continues the revision notes, focusing on:
Part 3 – Consistency / Coherence / Entailment
Part 4 – Overview of the tableau method
Part 5 – Detailed six-step tableau procedure

Part 3. Consistency, coherence, entailment¶

These three notions are central in the exam and are tightly connected.
The tableau method is used to decide them (via reductions).

3.1 Consistency of a knowledge base¶

Informal idea¶

A knowledge base \(K = (T, A)\) is consistent if it is "logically possible":
there exists at least one interpretation (model) in which all axioms in \(T\) and all assertions in \(A\) hold simultaneously.
It is inconsistent if there is no such interpretation.

Semi-formal definition¶

\(K\) is consistent iff there exists an interpretation \(\mathcal{I}\) such that:
\(\mathcal{I} \models T\) and \(\mathcal{I} \models A\).
Otherwise, \(K\) is inconsistent.

Examples (intuitive)¶

Consistent:
TBox: \(Student \sqsubseteq Person\)
ABox: \(a : Student\)
There is clearly a model where a is a student and all students are persons.
Inconsistent:
TBox: \(Student \sqsubseteq Person\)
ABox: \(a : Student, a : \neg Person\)
No model can make a both a Student and not a Person, given the TBox.

Exam relevance¶

You should be able to:

state (in words) what “K is consistent” means,
use the tableau method to decide whether a given \(K\) is consistent.

3.2 Coherence of concepts (with respect to a TBox / KB)¶

Informal idea¶

A concept is incoherent (or unsatisfiable) if it is impossible for any individual to ever be an instance of that concept, given the background knowledge.
A concept is coherent if it is possible for at least one individual to be an instance.

We always talk about coherence with respect to a TBox or a KB.

Semi-formal definition¶

Let \(C\) be a concept and \(K = (T, A)\) a knowledge base (often we just consider \(T\)).
\(C\) is satisfiable (coherent) w.r.t. \(K\) iff there exists a model \(\mathcal{I}\) of \(K\) such that \(C^{\mathcal{I}} \neq \emptyset.\)
\(C\) is unsatisfiable (incoherent) w.r.t. \(K\) if for every model \(\mathcal{I}\) of \(K\), we have \(C^{\mathcal{I}} = \emptyset.\)

Example¶

Suppose the TBox contains:

\(Vegetarian \sqsubseteq Person\)
\(MeatLover \sqsubseteq Person\)
\(Vegetarian \sqsubseteq \neg MeatLover\)

Now consider the concept:

\(VegMeatFan \equiv Vegetarian \sqcap MeatLover\)

Intuitively, VegMeatFan is incoherent, because:

any instance would be both Vegetarian and MeatLover,
but \(Vegetarian \sqsubseteq \neg MeatLover\) says this is impossible.

Exam relevance¶

You should be able to:

explain what it means for a concept to be (in)coherent,
reduce coherence checking to consistency checking (see below),
follow the tableau-based test once the reduction is given.

3.3 Entailment¶

Informal idea¶

Entailment is about what logically follows from a knowledge base.
If \(K\) entails a statement \(\varphi\), then whenever \(K\) is true, \(\varphi\) must also be true.

Semi-formal definition¶

Let \(K = (T, A)\) be a knowledge base and \(\varphi\) some statement (e.g. a concept assertion or a subsumption).

We write \(K \models \varphi\) (K entails \(\varphi\)) iff
for every interpretation \(\mathcal{I}\) such that \(\mathcal{I} \models K\), we also have \(\mathcal{I} \models \varphi\).

Examples of typical \(\varphi\):

Concept assertion: \( a : C \)
Role assertion: \( (a, b) : r \)
Subsumption: \( C \sqsubseteq D \)

Simple example¶

Let:

TBox: \(Student \sqsubseteq Person\)
ABox: \(a : Student\)

Then:

\(K \models a : Person\).

Intuitively: if in every model all students are persons and a is a student, a must be a person.

Exam relevance¶

You should be able to:

understand entailment in words,
use a standard reduction from entailment to consistency:
typically by adding the negation of the queried statement to the KB and checking (in)consistency with tableau.

3.4 Reducing coherence and entailment to consistency¶

The tableau method is defined as a consistency checker for ABoxes (after preprocessing).
To use it for coherence and entailment, we reduce those problems to consistency problems.

You need to know at least the high-level patterns (you might not have to memorise formal proofs, but you should recognise the constructions).

1) Testing coherence of a concept \(C\)¶

Goal: check if \(C\) is satisfiable (coherent) w.r.t. a TBox \(T\).

Typical reduction:

Build a knowledge base \(K' = (T, A')\) where \(A'\) contains a fresh individual name \(a\) with assertion:
\( a : C \)
Then:
If \(K'\) is consistent, then \(C\) is coherent (there is a model where some individual is in \(C\)).
If \(K'\) is inconsistent, then \(C\) is incoherent.

2) Testing whether \(K \models a : C\) (entailment of an assertion)¶

Goal: does \(K = (T, A)\) entail that individual \(a\) is an instance of concept \(C\)?

Typical reduction:

Form a new KB
\( K' = (T, A \cup \{ a : \neg C \}) \)
Intuition:
if we can consistently assume that \(a\) is not in \(C\), then \(K\) does not entail \(a : C\).
if this assumption leads to inconsistency, then \(K\) forces \(a : C\).

So:

If \(K'\) is inconsistent, then \(K \models a : C\).
If \(K'\) is consistent, then \(K \not\models a : C\).

3) Similar patterns for subsumption \(C \sqsubseteq D\)¶

You might see reductions like:

Check if concept \(C \sqcap \neg D\) is incoherent w.r.t. \(T\):
if it is incoherent, then \(C \sqsubseteq D\) holds in all models of \(T\).

Exam relevance¶

You should be able to:
write down (or at least understand) the “augmented KB” used in the reduction,
then run the tableau procedure on that KB to derive a consistency/inconsistency judgment.

Part 4. Tableau method – high-level overview¶

The tableau method is your main algorithmic tool for this class test.
It decides satisfiability/consistency by systematically trying to build a model.

4.1 Intuition: what does the tableau do?¶

术语说明：本文中 "branch" = 分支，"saturated" = 饱和（无规则可应用），"clash" = 冲突（矛盾）。

Conceptually, the tableau method:

starts from an ABox (after preprocessing the TBox into it),
repeatedly applies expansion rules (completion rules),
tries to construct a tree-shaped structure that could represent a model,
detects contradictions (e.g. both \(C\) and \(\neg C\) for the same individual),
and concludes:
if every branch ends in a contradiction, the ABox is unsatisfiable (inconsistent),
if at least one branch remains open (no contradiction), the ABox is satisfiable (consistent).

So tableau is a refutation-style search procedure:

satisfiable = "there is some open branch (a candidate model)"
unsatisfiable = "all branches close."

4.2 Global structure: six steps¶

In the lectures, the tableau method for DL knowledge bases is presented as a 6-step algorithm:

Eliminate subsumptions in the TBox (introduce *-concepts).
Expand the TBox by unfolding definitions (ensuring acyclicity).
Eliminate defined concepts in the ABox (replace by their definitions).
Convert ABox to Negation Normal Form (NNF).
Apply completion rules to build a tableau tree.
Inspect leaves of the tableau to determine (in)satisfiability.

For the exam, you should:

know what happens at each step in words,
be able to execute Steps 1–4 on small examples,
know and apply the completion rules correctly in Step 5,
correctly interpret open/closed branches in Step 6.

Part 5. Tableau method – detailed six-step procedure¶

This section refines each step. The exact notation may vary slightly from slides, but the ideas are the same.

5.1 Step 1–3: preprocessing the TBox and ABox¶

5.1.1 Step 1: eliminate subsumptions (introduce "star" concepts)¶

Motivation¶

The TBox may contain axioms of the form \( A \sqsubseteq C \) (subsumptions).
For the algorithm, it is convenient to rewrite these into equivalences, using special "star" concepts like \(A^*\), so that the TBox ultimately consists only of definitions of the form \(A \equiv C\).

Typical transformation¶

Given:

\( A \sqsubseteq C \)

We introduce a new “starred” concept \(A^*\) and rewrite as:

\( A \equiv C \sqcap A^* \)

Intuition:

\(A\) is at least as strong as \(C\),
\(A^*\) captures any additional information about \(A\) beyond \(C\).

Exam relevance¶

On simple examples, you may be asked to:
apply this kind of rewriting,
understand why it avoids losing information about \(A\).

5.1.2 Step 2: expand (unfold) the TBox¶

Acyclic TBox¶

The lectures assume an acyclic TBox:
no concept is (directly or indirectly) defined in terms of itself.
This allows us to “unfold” definitions safely:
replace defined concepts by their definitions until only primitive concepts remain.

Expansion¶

For each defined concept \(A\) (with a definition like \(A \equiv C\)):
recursively replace occurrences of \(A\) in other definitions by \(C\),
making sure we do not create infinite loops (hence acyclicity).

Goal¶

Obtain a TBox where:
all definitions are fully expanded into primitive concepts and role restrictions,
so that later, when we push definitions into the ABox, we do not need to look back at the TBox.

5.1.3 Step 3: eliminate defined concepts in the ABox¶

After TBox expansion:

whenever the ABox contains an assertion \( a : A \) where \(A\) is a defined concept (with definition \(A \equiv C\)), we replace it by \( a : C \).

We repeat this until:

the ABox contains only primitive concepts and role restrictions,
with no remaining defined concept names.

At this point:

the TBox is no longer needed for the tableau rules,
all relevant information is encoded directly in the ABox.

Exam relevance¶

You should be able to:
take a small \(K = (T, A)\),
unfold TBox definitions,
rewrite the ABox by substituting definitions,
obtain a “flattened” ABox suitable for tableau.

5.2 Step 4: Negation Normal Form (NNF)¶

Idea¶

In Negation Normal Form, all negations apply only to atomic concepts:
i.e. no negations in front of complex expressions like \(C \sqcap D\) or \(\forall r.C\).
This makes the application of tableau rules uniform and simpler.

Standard NNF transformations¶

We use logical equivalences to push negation inwards:

\( \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 \)

So in ABox assertions:

whenever we see something like \( a : \neg (C \sqcap D) \), we replace it by \( a : (\neg C \sqcup \neg D) \), etc.

Exam relevance¶

You should:
know what NNF means,
be able to convert a small set of ABox assertions to NNF,
be careful with quantifier rules (∀/∃).

5.3 Step 5: completion rules (tableau expansion)¶

After Steps 1–4, we have an ABox in a suitable normal form.
We now build a tableau tree by repeatedly applying completion rules.

Each rule has:

a positive condition (when it can be applied),
a negative condition (when not to apply it again),
and a conclusion (how the ABox is extended or branched).

The exact rule set may vary slightly, but commonly we have:

5.3.1 Conjunction rule (∧-rule)¶

If the ABox contains:

\( a : (C \sqcap D) \)

and we do not yet have both \( a : C \) and \( a : D \), then we add them.

Intuition:

to satisfy \(C \sqcap D\), the individual must satisfy both.

5.3.2 Disjunction rule (∨-rule) – branching¶

If the ABox contains:

\( a : (C \sqcup D) \)

and we have not yet branched on this, we split the branch into two:

one branch with \( a : C \),
another branch with \( a : D \).

Intuition:

to satisfy \(C \sqcup D\), the individual must satisfy at least one of them, but we do not know which, so we explore both possibilities.

5.3.3 Existential rule (∃-rule)¶

If the ABox contains:

\( a : \exists r.C \)

and there is no existing \(r\)-successor of \(a\) that is known to be in \(C\),
then we create a new individual \(b\) and add:

\( (a, b) : r \)
\( b : C \)

Intuition:

to satisfy \(\exists r.C\), there must be some r-successor in \(C\), so we create a fresh one.

5.3.4 Universal rule (∀-rule)¶

If the ABox contains:

\( a : \forall r.C \)
and we have \( (a, b) : r \) in the ABox,
but not yet \( b : C \),

then we add:

\( b : C \)

Intuition:

if all r-successors of \(a\) must be in \(C\), then every known r-successor gets the assertion \(b : C\).

5.3.5 Clash / ⊥-rule (closure)¶

A clash occurs if, for some individual \(a\), the ABox contains one of:

\( a : C \) and \( a : \neg C \),
or explicitly \( a : \bot \),

for some concept \(C\).

When a clash occurs on a branch:

that branch is marked closed (no model can extend it).

Rule application order (heuristic)¶

In practice (and in exams), it is good to:

detect clashes as early as possible (⊥-rule),
apply ∧ and ∀ rules before ∨,
delay ∨-rule (branching) as long as possible to avoid blow-up.

The recommended (but not mandatory) order often is:

apply ⊥-rule if possible,
then ∧-rule,
then ∃-rule,
then ∀-rule,
only then use ∨-rule to branch.

5.4 Step 6: inspecting leaves and reading the result¶

After repeatedly applying completion rules, we will reach a point where:

no rule is applicable on a branch (it is saturated),
and each branch is either:
closed (contains a clash),
or open (no clash and no further rule applies).

Satisfiability / consistency decision¶

If all branches are closed:
the initial ABox is unsatisfiable (inconsistent).
If at least one branch is open:
the initial ABox is satisfiable (consistent),
and the open branch can be read as a "partial model".

Connecting to different reasoning tasks¶

Checking consistency of \(K = (T, A)\):
after preprocessing, run tableau on the resulting ABox.
if some branch is open → K is consistent,
if all branches close → K is inconsistent.
Checking coherence of a concept \(C\):
build an augmented KB (e.g. add a fresh individual \(a : C\)),
run tableau for consistency,
interpret the result as in Part 3.4.
Checking entailment \(K \models \varphi\):
add the negation of \(\varphi\) to the ABox,
run tableau:
- if all branches close, then the augmented KB is inconsistent ⇒ \(K \models \varphi\),
- if some branch is open, then \(K \not\models \varphi\).

Summary of what you should be able to do¶

By the end of your revision, you should:

Explain (in words) the notions of:
consistency of a KB,
coherence of a concept,
entailment.
Recognise and apply standard reductions:
coherence → consistency,
entailment → consistency.
Execute the six-step tableau method on small examples:
TBox rewriting (star concepts),
TBox unfolding,
eliminating defined concepts in ABox,
converting ABox to NNF,
applying completion rules,
reading open/closed branches.
Avoid common mistakes:
forgetting to push negations into NNF,
misapplying ∃/∀ rules,
missing clashes,
stopping before the ABox is fully saturated.