Semantic Web Logics

In Semantic Web, there are formal models behind reasoning

  • FOL give formal definitions of RDFS and OWL statements
    • Classes - unary predicates
    • Properties - binary predicates
  • DL is a subset of FOL where many interesting properties are decidable


Formal Definitions

Observe that these statements all have the same general form:

  • $\forall \ ... \ (... \ \exists \ ...)$


RDFS

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

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^−$


OWL

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, ...\}$


See Also

Sources

  • Web Data Management, Manolescu, Ioana, et al. [1]