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. [http://webdam.inria.fr/Jorge/]