next up previous
Next: Bibliography Up: A Denotational Semantics for Previous: Standard OIL

The semantics of $ \mathcal{SHIQ}(d)$

The meaning of a $ \mathcal{SHIQ}(d)$ terminology, and of the common inference problems, is given in terms of a Tarski style model theoretic semantics using interpretations [2,6,4]. An interpretation $ \ensuremath{\mathcal{I}}\xspace = (\Delta^\ensuremath{\mathcal{I}}\xspace ,\Delta^\mathcal{D},\cdot^\ensuremath{\mathcal{I}}\xspace )$ consists of a set $ \Delta^\ensuremath{\mathcal{I}}\xspace $, called the abstract domain of $ \ensuremath{\mathcal{I}}\xspace $, a set $ \Delta^\mathcal{D}$, called the concrete domain of $ \ensuremath{\mathcal{I}}\xspace $, and a valuation function $ \cdot^\ensuremath{\mathcal{I}}\xspace $. The abstract and concrete domains must be disjoint, i.e., $ \Delta^\ensuremath{\mathcal{I}}\xspace \cap \Delta^\mathcal{D}=
\emptyset$.

The valuation function $ \cdot^\ensuremath{\mathcal{I}}\xspace $ maps every concept to a subset of $ \Delta^\ensuremath{\mathcal{I}}\xspace $ and every role to a subset of $ \Delta^\ensuremath{\mathcal{I}}\xspace \times(\Delta^\ensuremath{\mathcal{I}}\xspace
\cup \Delta^\mathcal{D}$) such that, for all concepts $ C$, $ D$, roles $ R$, $ S$, concrete predicate expressions $ p$ and non-negative integers $ n$, the equations in Figure 5 are satisfied (where $ \sharp M$ denotes the cardinality of a set $ M$). Concrete predicate expressions have the obvious interpretation as shown in Figure 6. The ordering on strings is the standard lexicographic one.

The concrete domain is treated differently from the abstract domain because it is considered to be already sufficiently structured by the predicates min, max etc. Therefore, it is not appropriate to form new classes of concrete objects (values) using the concept language [1].

Figure: $ \mathcal{SHIQ}(d)$ semantics
\begin{figure}\begin{center}
{\small\begin{tabular}{rclr}
\ $(R^-)\ensuremath{^\...
...ace{0.1cm}(functional restriction)
\ \end{tabular}}
\end{center}\ \ \end{figure}

Figure 6: Concrete expression semantics
\begin{figure}\begin{displaymath}\begin{array}{rcl}
\par (p_1 \sqcap\ldots\sqcap...
...box{$\geqslant$\mbox{}$_{x}$}}(y)
\ \end{array}\end{displaymath}\ \ \end{figure}


In order to avoid considering roles such as $ R^{--}$ (i.e., the inverse of an inverse) we will define a function $ \mathit{Inv}$ such that $ \mathit{Inv}(R)$ is $ R^-$ and $ \mathit{Inv}(R^-)$ is $ R$. A role $ R$ is directly subsumed by a role $ S$ w.r.t. a terminology $ \mathcal{T}$ iff either $ \{R \sqsubseteq S\} \subseteq \ensuremath{\mathcal{T}}\xspace $ or $ \{\mathit{Inv}(R) \sqsubseteq \mathit{Inv}(S)\} \subseteq \ensuremath{\mathcal{T}}\xspace $. A role $ R$ is subsumed by a role $ S$ w.r.t. $ \mathcal{T}$ (written $ \ensuremath{\mathcal{T}}\xspace
\models R \sqsubseteq S$) iff $ R$ is directly subsumed by a $ S$ or there is a role $ S'$ such that $ R$ is directly subsumed by a $ S'$ and $ \ensuremath{\mathcal{T}}\xspace \models S' \sqsubseteq S$. A role $ R$ is equivalent to a role $ S$ w.r.t. $ \mathcal{T}$ (written $ \ensuremath{\mathcal{T}}\xspace \models R \doteq S$) iff $ \ensuremath{\mathcal{T}}\xspace
\models R \sqsubseteq S$ and $ \ensuremath{\mathcal{T}}\xspace \models S \sqsubseteq R$. A role $ R$ is transitive in $ \mathcal{T}$ iff $ \{S \in \ensuremath{\mathbf{S}_+}\xspace \} \subseteq \ensuremath{\mathcal{T}}\xspace $ for some role $ S$ such that $ R \doteq S$ or $ \mathit{Inv}(R) \doteq S$ (this defines $ \ensuremath{\mathbf{S}_+}\xspace $, the set of transitive role names). A role $ R$ is a simple role in $ \mathcal{T}$ iff there is no role $ S$ such that $ S$ is transitive in $ \mathcal{T}$ and $ \ensuremath{\mathcal{T}}\xspace \models S \sqsubseteq R$.

An interpretation $ \ensuremath{\mathcal{I}}\xspace $ satisfies a $ \mathcal{SHIQ}$ terminology $ \mathcal{T}$ iff for every axiom $ R \sqsubseteq S$ in $ \mathcal{T}$, $ R^\ensuremath{\mathcal{I}}\xspace \subseteq S^\ensuremath{\mathcal{I}}\xspace $, for every axiom $ C \sqsubseteq D$ in $ \mathcal{T}$, $ C^\ensuremath{\mathcal{I}}\xspace \subseteq D^\ensuremath{\mathcal{I}}\xspace $ and for every transitive role $ S$ in $ \mathcal{T}$, $ S\ensuremath{^\mathcal{I}}\xspace = (S\ensuremath{^\mathcal{I}}\xspace )^+$. Such an interpretation is called a model of $ \mathcal{T}$ (written $ \ensuremath{\mathcal{I}}\xspace \models
\ensuremath{\mathcal{T}}\xspace $).

A concept $ C$ is satisfiable with respect to a $ \mathcal{SHIQ}$ terminology $ \mathcal{T}$ (written $ \ensuremath{\mathcal{T}}\xspace \models C \neq \bot$) iff there is a model $ \ensuremath{\mathcal{I}}\xspace $ of $ \mathcal{T}$ with $ C^\ensuremath{\mathcal{I}}\xspace \neq \emptyset$. A concept $ C$ is subsumed by a concept $ D$ w.r.t. $ \mathcal{T}$ (written $ \ensuremath{\mathcal{T}}\xspace \models C \sqsubseteq D$) $ C^\ensuremath{\mathcal{I}}\xspace \subseteq D^\ensuremath{\mathcal{I}}\xspace $ holds for each model $ \ensuremath{\mathcal{I}}\xspace $ of $ \mathcal{T}$.

An OIL ontology $ \mathcal{O}$ is called consistent iff $ \sigma(\ensuremath{\mathcal{O}}\xspace )
\models \top \neq \bot$. A class $ \textsf{CN}$ in an ontology $ \mathcal{O}$ is called consistent iff $ \sigma(\ensuremath{\mathcal{O}}\xspace ) \models \sigma(\ensuremath{\textsf{CN}}) \neq
\bot$. A class $ \textsf{CN}$ is a subclass of a class $ \textsf{DN}$ in an ontology $ \mathcal{O}$ iff $ \sigma(\ensuremath{\mathcal{O}}\xspace ) \models \sigma(\ensuremath{\textsf{CN}}) \sqsubseteq
\sigma(\ensuremath{\textsf{DN}})$.


next up previous
Next: Bibliography Up: A Denotational Semantics for Previous: Standard OIL
Ian Horrocks 2000-09-10