Description Logic - Tableaux Method
Decision Method
It is important to find a decision method for the consistency checking problem.
The tableaux method allows us to solve this problem but only for acyclic knowledge bases.
Using Concepts
An atomic concept $A$ directly uses an atomic concept $B$ if there is a subsumption $A\sqsubseteq X$ or $A\equiv X$ in $\mathcal T$ such that $B$ occurs in $X$.
For example if the following is in $\mathcal T$:
\[\text{granparent}\equiv\text{person}\sqcap\exists\text{hasChild}.\text{parent}\]then $\text{grandparent}$ directly uses $\text{person}$ and $\text{parent}$.
An atomic concept $A$ indirectly uses an atomic concept $B$ if there is a finite sequence $A_1, \ldots, A_n$ of atomic concepts such that $A$ directly uses $A_1$, $A_1$ directly uses $A_2, \ldots,A_{n-1}$ directly uses $A_n$ and $A_n$ directly uses $B$.
For example if the following are in $\mathcal T$:
\[\begin{aligned} \text{mother}&\equiv\text{parent}\sqcap\text{female}\\ \text{parent}&\equiv\text{person}\sqcap\exists\text{hasChild}.\top \end{aligned}\]then $\text{mother}$ does not directly use $\text{person}$, but $\text{mother}$ does use $\text{person}$.
Cycles
- A knowledge base $\mathcal K$ contains a terminological cycle if there is a concept that uses itself.
- A knowledge base $\mathcal K$ is acyclic if:
- $\mathcal K$ contains no terminological cycle
- Every atomic conept occurs on the left-hand side of at most one subsumption in $\mathcal T$.
Cyclical Example
| TBox |
|---|
| $\text{person}\equiv\text{person}\sqcap\exists\text{hasChild}.\top$ |
| $\text{person}\sqsubseteq\exists\text{isChildOf}.\text{parent}$ |
The Tableaux Method
Let $\mathcal K=(\mathcal A,\mathcal T)$ be an acyclic knowledge base. Consistency of $\mathcal K$ is checked in six steps.
1. Eliminate $\sqsubseteq$
Suppose $A\sqsubseteq X$ occurs in $\mathcal T$:
-
Add a new atomic concept $A^*$ that characterises those $X$ that are $A$.
$A^*$ is the property that distinguishes those $X$ that are $A$ from those $X$ that are $\neg A$.
- Replace the concept with $A\equiv X\sqcap A^*$
- Call the resulting knowledge base $\mathcal K^*$.
2. Expand the TBox
-
If $A\equiv X$ is in $\mathcal T^*$, then every occurrence of $A$ in other concept definitions can be replaced by $X$.
Replace simple objects with their definitions.
- Keep replacing until no futher replacements are possible.
- Call the resulting TBox $\mathcal T^{*e}$.
If $\text{
3. Eliminate Defined Concepts from the ABox
Suppose $o:A$ is in $\mathcal A$ and $A\equiv X$ is in $\mathcal T^{*e}$:
-
Then we can replace $o:A$ by $o:X$.
We replace objects by their definitions.
-
Call the resulting ABox $\mathcal A^e$.
4. Put the ABox in Negation Normal Form
This step removes negations from the ABox.
- Rewrite formulas in $\mathcal A^e$ in such a way that negations only occur immediatley in front of atomic concepts.
- Call the resulting ABox $\mathcal A^{en}$.
In order to put formulas in NNF, you can use the following replacement rules:
| Original | Replacement |
|---|---|
| $\neg\top$ | $\bot$ |
| $\neg\bot$ | $\top$ |
| $\neg\neg X$ | $X$ X |
| $\neg(X\sqcap Y)$ | $\neg X\sqcup \neg Y$ |
| $\neg(X \sqcup Y)$ | $\neg X\sqcap \neg Y$ |
| $\neg\forall r.X$ | $\exists r.\neg X$ |
| $\neg\exists r.X$ | $\forall r.\neg X$ |
5. Apply Completion Rules to the ABox
This step builds a tree of sets of concept and role assertions:
- The root of the tree is $\mathcal A^{en}$.
Whenever one of the following rules can be applied to any node $\Gamma$, use them to generate new nodes:
| Originals | New Successors |
|---|---|
| $o:X\sqcap Y\in\Gamma$ and $o:X\notin\Gamma$ | $\Gamma\cup\{o:X, o:Y\}$ |
| $o:X\sqcup Y\in\Gamma$ and neither $o:X\in\Gamma$ or $o:Y\in\Gamma$ | $\Gamma\cup\{o:X\}$ and $\Gamma\cup\{o:Y\}$ |
| $o_1:\exists r.X\in\Gamma$ and there is no $o_2$ where $o_s:X\in\Gamma$ and $(0_1, o_2):r\in\Gamma$ | Take an object $o_3$ that does not occur in $\Gamma$ and create $\Gamma\cup\{(o_1,o_3):r,o_3:X\}$ |
| $o_1:\forall.rX\in\Gamma$ and $(o_1,o_2):r\in\Gamma$ but $o_2:X\notin\Gamma$ | $\Gamma\cup\{o_2:X\}$ |
| $o:\forall\in\Gamma$, $o:\neg A\in\Gamma$ and $o:\bot\notin\Gamma$ | $\Gamma\cup\{o:\bot\}$ |
6. Check the Leaves for Contradictions
A set $\Gamma$ contains an immediate contradiction if $o:\bot\in\Gamma$ for some $o$.
If no more rules can be applied, check the leaves (endpoints):
- If all endpoints contain immediate contradictions, $\mathcal K$ is inconsistent.
- If at least one endpoint contains no immediate contradiction, $\mathcal K$ is consistent.