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}\) concept satisfiablity - Example 2

We check whether \(C=A \sqcap \exists r.B \sqcap \forall r.\neg B\) is satisfiable. It is in NNF, so we can directly apply the tableau algorithm to

\[C=A \sqcap \exists r.B \sqcap \forall r.\neg B.\]

An application of \(\sqcap-\text{rule}\) gives

\[L(x)=\{C, A, \exists r.B, \forall r.\neg B\}.\]

An application of \(\exists-\text{rule}\) gives

\(\begin{align*} L(x)&=\{C, A, \exists r.B, \forall r.\neg B\}\\ L(y)&=\{B\}\\ L(\langle x,y \rangle)&=\{r\} \end{align*} \)

An application of \(\forall-\text{rule}\) gives

\(\begin{aligned} L(x)&=\{C, A, \exists r.B, \forall r.\neg B\}\\ L(y)&=\{B, \neg B\}\\ L(\langle x,y \rangle)&=\{r\} \end{aligned} \)

We obtained a clash and no other choices are possible. Thus, \(A \sqcap \exists r.B \sqcap \forall r.\neg B\) is unsatisfiable and there exists no model.


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.