Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

Tableau algorithm for \(\mathcal{ALC}\) TBoxes

We extend the tableau algorithm to check satisfiability of \(\mathcal{ALC}\) TBoxes
  • An \(\mathcal{ALC}\) TBox contains only axioms (GCIs) of form \(C \sqsubseteq D\) (Note that axioms of form \(C \equiv D\) can be rewritten as \(C \sqsubseteq D\) and \(D \sqsubseteq C\))
  • Every GCI is equivalent to \(\top \sqsubseteq \neg C \sqcup D\)

We can internalize the whole TBox into a single axiom:
\[\mathcal{T}=\{C_i \sqsubseteq D_i | 1 \leq i \leq n\}\]

is equivalent to
\[ \top \sqsubseteq \underset{1 \leq i \leq n}{{\LARGE\sqcap}} \neg C_i \sqcup D_i \]

Let \(C_\mathcal{T}\) be the concept on the right side of the GCI, then an additional rule is

\(\mathcal{T}\)-rule if \( C_\mathcal{T} \,\,\not \in L(v), \text{ for some } v \in V\)
then \( L(v):=L(v) \cup \{C_\mathcal{T}\} \)

Content Tools


There are currently no sources for this slide.