In Semantic Web, there are formal models behind reasoning
Observe that these statements all have the same general form:
RDFS statements | FOL translation | DL notation |
---|---|---|
i rdf:type C |
$C(i)$ | $i \ : \ C$ or $C(i)$ |
i P j |
$P(i, j)$ | $i \ P \ j$ or $P(i, j)$ |
C rdfs:subClassOf D |
$\forall X \ \big( C(X) \ \exists \ D(X) \big)$ | $C \sqsubseteq D$ |
P rdfs:subPropertyOf R |
$\forall X, Y \ \big( P(X, Y) \ \exists \ R(X, Y) \big)$ | $P \sqsubseteq R$ |
P rdfs:domain C |
$\forall X, Y \ \big( P(X, Y) \ \exists \ C(X) \big)$ | $\exists P \sqsubseteq C$ |
P rdfs:range D |
$\forall X, Y \ \big( P(X, Y) \ \exists \ D(Y) \big)$ | $\exists P^- \sqsubseteq D$ |
RDFS-Plus | FOL | DL |
---|---|---|
P rdf:type owl:FunctionalProperty |
$\forall X, Y, Z \ \big( P(X, Y ) \land P(X, Z) \Rightarrow Y = Z \big)$ | $(\text{funct} P)$ or $\exists P \sqsubseteq (\leqslant 1 P)$ |
P rdf:type owl:InverseFunctionalProperty |
$\forall X, Y, Z \ \big( P(X, Y) \land P(Z, Y) \Rightarrow X = Z)$ | $(\text{funct} P^− )$ or $\exists P^− (\leqslant 1 P^− )$ |
P owl:inverseOf Q |
$\forall X, Y \ \big(P(X, Y) \Leftrightarrow Q(Y, X) \big)$ | $P \equiv Q^−$ |
P rdf:type owl:SymmetricProperty |
$\forall X, Y \ \big(P(X, Y) \Rightarrow P(Y, X) \big)$ | $P \sqsubseteq P^−$ |
Restrictions
OWL | FOL | DL |
---|---|---|
owl:onProperty P; owl:allValuesFrom C |
$\forall Y \ \big(P(X, Y) \Rightarrow C(Y) \big)$ | $\forall P.C$ |
owl:onProperty P; owl:someValuesFrom C |
$\exists Y \ \big( P(X, Y) \land C(Y) \big)$ | $\exists P.C$ |
owl:onProperty P; owl:minCardinality n |
$\exists Y_1 ... Y_n \ \big(P(X, Y_1) \land ... \land P(X, Y_n) \land [\forall i, j, i \ne j: Y_i \ne Y_j ]\big)$ | $(\geqslant n P)$ |
owl:maxCardinality n |
(too complex) | $(\leqslant n P)$ |
Sets
OWL | FOL | DL |
---|---|---|
C owl:disjointWith D |
$\forall X \ \big( C(X) \Rightarrow \lnot D(X) \big)$ | $C \sqsubseteq \lnot D$ |
owl:intersectionOf (C, D...) |
$C(X) \land D(X) \land ...$ | $C \sqcap D \ \sqcap \ ...$ |
owl:unionOf ( C, D...) |
$C(X) \lor D(X) \lor ...$ | $C \sqcup D \ \sqcup \ ...$ |
owl:oneOf (e, f ...) |
$X = e \lor X = f \ \lor ...$ | $\text{OneOf} \{e, f, ...\}$ |