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.

Completion Rules for \(\mathcal{ALC}\) concept satisfiability

\(\sqcap\)-rule if \( C \sqcap D \in L(v), \text{ for some } v \in V \text{ and } \{C, D\} \not \subseteq L(v) \)
then \(L(v):=L(v) \cup \{C, D\} \)
\(\sqcup\)-rule if \( C \sqcup D \in L(v), \text{ for some } v \in V \text{ and } \{C, D\} \cap L(v) = \emptyset \)
then \( \text{choose } X \in \{C, D\} \text{ and let } L(v) := L(v) \cup \{X\} \)
\(\exists\)-rule if \( \exists r.C \in L(v), \text{ for some } v \in V, \text{ and there is no } r\text{-successor } \) \( v' \text{ of } v \text{ such that } C \in L(v') \)
then \(V:= V \cup \{v'\} , E:=E \cup \{ \langle v,v' \rangle \}, L(v'):=\{C\}\) \( \text{ and } L(\langle v,v' \rangle):=\{r\}\) \(\text{ for a new vertex } v'\)
\(\forall\)-rule if \( v,v' \in V, v' \text{ is } r\text{-successor of } v, \forall r.C \in L(v) \text{ and } C \not \in L(v') \)
then \( L(v'):=L(v') \cup {C} \)

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.