OWL 2 Web Ontology Language
RDF-Based Semantics

Assume that the premises of the correspondence theorem hold for given RDF graphs G₁^* and G₂^*. This allows for applying the balancing lemma, which provides the existence of certain RDF graphs G₁ and G₂ that are OWL 2 DL ontologies in RDF graph form. Hence, it is possible to build OWL 2 DL ontologies in Functional Syntax form F(G₁) and F(G₂) by applying the reverse OWL 2 RDF mapping to G₁ and G₂, respectively.

The balancing lemma further provides that the pair ⟨ G₁ , G₂ ⟩ is balanced.

The claimed property (1) of the correspondence theorem follows directly from property (1) of the balancing lemma and from property (1) of the "Balanced"-definition. The claimed properties (2) and (3) of the correspondence theorem follow directly from properties (2) and (3) of the balancing lemma, respectively.

The rest of this proof will treat the claimed property (4) of the correspondence theorem, which states that if F(G₁) OWL 2 Direct entails F(G₂) with respect to F(D), then G₁ OWL 2 RDF-Based entails G₂ with respect to D.

Let I be an OWL 2 RDF-Based interpretation w.r.t. an OWL 2 RDF-Based datatype map D of a vocabulary V_I that covers all the names (IRIs and literals) occurring in the RDF graphs G₁ and G₂, and let I OWL 2 RDF-Based satisfy G₁. It will be shown that I OWL 2 RDF-Based satisfies G₂.

As a first step, an OWL 2 Direct interpretation J w.r.t. the corresponding OWL 2 Direct datatype map F(D) will be constructed for a vocabulary V_J that covers all the names (IRIs and literals) occurring in the OWL 2 DL ontologies in Functional Syntax form F(G₁) and F(G₂). J will be defined in a way such that it closely corresponds to I on those parts of the vocabularies V_I and V_J that cover G₁ and G₂, and F(G₁) and F(G₂), respectively.

G₁ and G₂ are OWL 2 DL ontologies in RDF graph form that are mapped by the reverse RDF mapping to F(G₁) and F(G₂), respectively. This means that the same literals are used in both G₁ and F(G₁), and in both G₂ and F(G₂), respectively. Further, since the pair ⟨ G₁ , G₂ ⟩ is balanced, according to property (2) of the "Balanced"-definition there are entity declarations in F(G₁) and F(G₂) for all the entity types of every non-built-in IRI occurring in G₁ and G₂, respectively. For each entity declaration of the form Declaration(T(u)) in F(G₁) and F(G₂), where T is the entity type for some IRI u, a typing triple of the form u rdf:type t exists in G₁ or G₂, respectively, where t denotes the class representing the part of the universe that corresponds to T; and vice versa.

Since the pair ⟨ G₁ , G₂ ⟩ is balanced, all the entity declarations of F(G₂) are also contained in F(G₁), and therefore all the typing triples of G₂ that correspond to some entity declaration in F(G₂) are also contained in G₁. Since I OWL 2 RDF-Based satisfies G₁, all these "declaring" typing triples are OWL 2 RDF-Based satisfied by I, and thus all non-built-in IRIs in G₁ and G₂ are actually instances of their declared parts of the universe.

Based on these observations, the OWL 2 Direct interpretation J and its vocabulary V_J for the datatype map F(D) can now be defined.

The vocabulary V_J := ( V_C , V_OP , V_DP , V_I , V_DT , V_LT , V_FA ) is defined as follows.

• The set V_C of class names contains all IRIs that are declared as classes in F(G₁).
• The set V_OP of object property names contains all IRIs that are declared as object properties in F(G₁).
• The set V_DP of data property names contains all IRIs that are declared as data properties in F(G₁).
• The set V_I of individual names contains all IRIs that are declared as named individuals in F(G₁).

The sets V_DT of datatype names, V_LT of literals, and V_FA of facet-literal pairs are defined according to Section 2.1 of [OWL 2 Direct Semantics] w.r.t. the datatype map F(D). Specifically, V_DT includes all IRIs that are declared as datatypes in F(G₁).

The interpretation J := ( Δ_I , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT , ⋅ ^FA ) is defined as follows. The object and data domains of J are identified with the universe IR and the set of data values LV of I, respectively, i.e., Δ_I := IR and Δ_D := LV. The datatype interpretation function ⋅ ^DT, the literal interpretation function ⋅ ^LT, and the facet interpretation function ⋅ ^FA are defined according to Section 2.2 of [OWL 2 Direct Semantics]. Specifically, ⋅ ^DT interprets all IRIs that are declared as datatypes in F(G₁) according the following definition. For every non-built-in IRI u occurring in F(G₁):

• If u is declared as a named individual, then set u^I := I(u), since the graph contains the triple "u rdf:type owl:NamedIndividual", i.e., I(u) ∈ IR.
• If u is declared as a class, then set u^C := ICEXT(I(u)), since the graph contains the triple "u rdf:type owl:Class", i.e., I(u) ∈ IC.
• If u is declared as a datatype, then set u^DT := ICEXT(I(u)), since the graph contains the triple "u rdf:type rdfs:Datatype", i.e., I(u) ∈ IDC.
• If u is declared as an object property, then set u^OP := IEXT(I(u)), since the graph contains the triple "u rdf:type owl:ObjectProperty", i.e., I(u) ∈ IP.
• If u is declared as a data property, then set u^DP := IEXT(I(u)), since the graph contains the triple "u rdf:type owl:DatatypeProperty", i.e., I(u) ∈ IODP.

Note that G₁ may also contain declarations of annotation properties, but they will not be interpreted by the OWL 2 Direct Semantics and are therefore ignored here. This will not lead to problems, since the pair ⟨ G₁ , G₂ ⟩ is balanced, and therefore G₂ does not contain any annotations.

Further, note that the definition of J is compatible with the concept of a non-separated vocabulary in OWL 2 DL (also called "punning", see Section 5.9 of [OWL 2 Specification]). Since G₁ and G₂ are OWL 2 DL ontologies in RDF graph form, it is allowed that the same IRI u is declared to be all of an individual name, and a class name, and either an object property name or a data property name. According to I, the IRI u will always denote the same individual in the universe IR, where I(u) will be both a class and a property. Under J, however, the individual name u will denote an individual, the class name u will denote a subset of Δ_I, and the property name u will denote a subset of Δ_I × Δ_I.

Literals occurring in G₁ and G₂ are mapped by the OWL 2 RDF mapping to the same literals in the corresponding interpreted language constructs of F(G₁) and F(G₂), which comprise data enumerations, has-value restrictions with a data value, cardinality restrictions, datatype restrictions, data property assertions, and negative data property assertions. Also, the semantics of literals is strictly analog for both the OWL 2 RDF-Based Semantics and the OWL 2 Direct Semantics. Therefore, literals need no further treatment in this proof.

Based on the premise that I OWL 2 RDF-Based satisfies G₁, it has to be shown that J OWL 2 Direct satisfies F(G₁). For this to hold it will be sufficient to show that J OWL 2 Direct satisfies every axiom occurring in F(G₁). Let A be an axiom occurring in F(G₁), and let g_A be the subgraph of G₁ that is mapped to A by the reverse OWL 2 RDF mapping. It is possible to prove that J OWL 2 Direct satisfies A by showing that the meaning, which is given to A by the OWL 2 Direct Semantics, is compatible with the semantic relationship that, according to J, holds between the denotations of the names occurring in A. The basic idea is as follows:

Since I OWL 2 RDF-Based satisfies G₁, all the triples occurring in g_A are OWL 2 RDF-Based satisfied by I. Also, since I is an OWL 2 RDF-Based interpretation, all the OWL 2 RDF-Based semantic conditions are met by I. Hence, the left-to-right directions of all the semantic conditions that are "matched" by the triples in g_A will apply. This will reveal certain semantic relationships that, according to I, hold between the denotations of the names occurring in g_A. These semantic relationships are, roughly speaking, the semantic consequences of the axiom that is encoded by the triples in g_A.

Since the denotations w.r.t. J of all the names occurring in A have been defined in terms of the denotations and class and property extensions w.r.t. I of the same names occurring in g_A, and since the meaning of the axiom A w.r.t. the OWL 2 Direct Semantics turns out to be fully covered by the semantic consequences of the subgraph g_A w.r.t. the OWL 2 RDF-Based Semantics, one can eventually show that J OWL 2 Direct satisfies A.

A special note is necessary for anonymous individuals occurring in an assertion A. These have the form of the same blank node b both in A and in g_A. Both the OWL 2 RDF-Based Semantics and the OWL 2 Direct Semantics treat blank nodes as existential variables in an ontology. Since I satisfies g_A, b can be mapped to an individual x in IR such that g_A becomes true under I (see Section 1.5 in [RDF Semantics] for the precise definition on how blank nodes are treated in RDF based languages). The same mapping from b to x can also be used for J in order to OWL 2 Direct satisfy A.

This basic idea is now demonstrated in more detail for a single example axiom A in F(G₁), which can be taken as a hint on how a complete proof could be constructed in principle. A complete proof would need to take every language construct of OWL 2 into account, as well as additional aspects such as datatype maps and facets. As in the example below, such a proof can make use of the observation that the definitions of the OWL 2 Direct Semantics and the OWL 2 RDF-Based Semantics are actually closely aligned for all the different language constructs of OWL 2.

Since J OWL 2 Direct satisfies F(G₁), and since F(G₁) OWL 2 Direct entails F(G₂), it follows that J OWL 2 Direct satisfies F(G₂).

The next step will be to show that I OWL 2 RDF-Based satisfies G₂. For this to hold, I needs to OWL 2 RDF-Based satisfy all the triples occurring in G₂, taking into account the premise that an OWL 2 RDF-Based interpretation is required to meet all the OWL 2 RDF-Based semantic conditions.

Since the pair ⟨ G₁ , G₂ ⟩ is balanced, G₂ contains a single ontology header consisting of a single triple "b rdf:type owl:Ontology" with a blank node b, and it does neither contain annotations nor deprecation statements. Hence, F(G₂) only consists of entity declarations and axioms, and does not have any ontology IRI and no ontology version, annotations or import directives. Further, since G₂ is an OWL 2 DL ontology in RDF graph form, every triple occurring in G₂, which is not the ontology header triple, belongs to some subgraph of G₂ that is mapped by the reverse OWL 2 RDF mapping to one of the entity declarations or axioms contained in F(G₂).

For the ontology header triple "b rdf:type owl:Ontology" in G₂: Since G₁ is an OWL 2 DL ontology in RDF graph form, G₁ contains an ontology header containing a triple "x rdf:type owl:Ontology", where x is either an IRI or a blank node. Since I OWL 2 RDF-Based satisfies G₁, this particular triple is satisfied by I. From the semantic conditions of "Simple Entailment", as defined in [RDF Semantics], follows that the triple "b rdf:type owl:Ontology" with the existentially interpreted blank node b is satisfied by I, too.

For entity declarations, let A be an entity declaration in F(G₂), and let g_A be the corresponding subgraph of G₂. Since the pair ⟨ G₁ , G₂ ⟩ is balanced, A occurs in F(G₁), and hence g_A is a subgraph of G₁. Since I OWL 2 RDF-Based satisfies G₁, I in particular OWL 2 RDF-Based satisfies g_A.

For axioms, let A be an axiom in F(G₂), and let g_A be the corresponding subgraph of G₂. It is possible to prove that I OWL 2 RDF-Based satisfies g_A, by showing that all the premises for the right-to-left hand side of the particular semantic conditions, which are associated with the sort of axiom represented by g_A, are met. This will allow to apply the semantic condition, from which will follow that all the triples in g_A are OWL 2 RDF-Based satisfied by I. The premises of the semantic condition generally require that the denotations of all the non-built-in names in g_A are contained in the appropriate part of the universe, and that the semantic relationship that is expressed on the right hand side of the semantic condition actually holds between the denotations of all these names w.r.t. I. Special care has to be taken regarding the blank nodes occurring in g_A. The basic idea is as follows:

For every non-built-in IRI u occurring in g_A, u also occurs in A. Since the pair ⟨ G₁ , G₂ ⟩ is balanced, property (2) of the "Balanced"-definition provides that there are entity declarations in F(G₂) for all the entity types of u, each being of the form E := "Declaration(T(u))" for some entity type T. From the reverse RDF mapping follows that for each such declaration E a typing triple e exists in G₂, being of the form e := "u rdf:type t", where t is the name of a class representing the part of the universe corresponding to the entity type T. It has already been shown that for E being an entity declaration in F(G₂), and e being the corresponding subgraph in G₂, I OWL 2 RDF-Based satisfies e. Hence, I(u) is an individual contained in the appropriate part of the universe.

Further, since J OWL 2 Direct satisfies F(G₂), J OWL 2 Direct satisfies A. Therefore, the semantic relationship that is represented by A according to the OWL 2 Direct Semantics actually holds between the denotations of the names occurring in A w.r.t. J. Since the denotations of these names w.r.t. J have been defined in terms of the denotations and class and property extensions w.r.t. I of the same names in G₂, by applying the definition of J it will turn out that the analog relationship also holds between the denotations of the same names occurring in g_A.

Finally, for the blank nodes occurring in g_A, it becomes clear from the fact that G₂ is an OWL 2 DL ontology in RDF graph form that only certain kinds of subgraphs of g_A can occur having blank nodes.

• Case 1: A blank node corresponds to some anonymous individual in A (for A being one of a class assertion, object property assertion or data property assertion, according to Sections 5.6, 9.5 and 11.2 in [OWL 2 Specification]). The same blank node is used in A, and J interprets it as an existential variable. This renders the semantic relationship that is expressed by A into an existential assertion. After applying the definition of J, the analog existential assertion holds w.r.t. I, with the same blank node as the same existential variable in g_A.
• Case 2: A blank node is the "root" node of the multi-triple RDF encoding g_A of A (for g_A being an n-ary axiom from Section 5.11, or a negative property assertion from Section 5.15). The right-to-left direction of the semantic condition for this kind of axiom is of a form that the triples in g_A containing the blank node will be OWL 2 RDF-Based satisfied after all the premises of the semantic condition are met.
• Case 3: A blank node is the "root" node of the multi-triple RDF encoding g_E of an expression in A (for g_E being either a sequence, or one of a boolean connective from Section 5.4, an enumeration from Section 5.5, a property restriction from Section 5.6, or a datatype restriction from Section 5.7). Since the pair ⟨ G₁ , G₂ ⟩ is balanced, g_E also occurs in G₁. Since I OWL 2 RDF-Based satisfies G₁, g_E is OWL 2 RDF-Based satisfied, either, taking into account that blank nodes are existential variables. Hence, the left-to-right direction of the respective semantic condition for the particular sort of expression can be applied. This can be done for all the expressions occurring in g_A, and g_A can be seen as a directed acyclic graph with the triples encoding the actual axiom on top, and the different component expressions being connected via blank nodes. Eventually, one can see that all the premises of the right-to-left direction of the semantic condition for the axiom encoded by g_A hold.

This basic idea is now demonstrated in more detail for a single example axiom A in F(G₂), which can be taken as a hint on how a complete proof could be constructed in principle. A complete proof would need to take every language construct of OWL 2 into account, as well as additional aspects such as datatype maps and facets. As in the example below, such a proof can make use of the observation that the definitions of the OWL 2 Direct Semantics and the OWL 2 RDF-Based Semantics are actually closely aligned for all the different language constructs of OWL 2.

To conclude, for every OWL 2 RDF-Based interpretation I that OWL 2 RDF-Based satisfies G₁ it turns out that I also OWL 2 RDF-Based satisfies G₂. Hence, G₁ OWL 2 RDF-Based entails G₂.

Q.E.D.

The correspondence theorem in Section 7.2 shows that it is possible for the OWL 2 RDF-Based Semantics to reflect all the entailments of the OWL 2 Direct Semantics [OWL 2 Direct Semantics], provided that one allows for certain "harmless" syntactic transformations on the RDF graphs being considered. This makes numerous potentially desirable and useful entailments available that would otherwise be outside the scope of the OWL 2 RDF-Based Semantics, for the technical reasons discussed in Section 7.1. It seems natural to ask for similar entailments even when an entailment query does not formally consist of OWL 2 DL ontologies in RDF graph form. However, the correspondence theorem does not apply to such cases, and thus the OWL 2 Direct Semantics cannot be taken as a reference frame for "desirable" or "useful" entailments, or for what it means that a given transformation is "harmless" or not.

As discussed in Section 7.1, a core obstacle for the correspondence theorem to hold was RDF encodings of OWL 2 expressions, such as union class expressions, which appear on the right hand side of an entailment query. Under the OWL 2 RDF-Based Semantics, it is not generally ensured that an individual exists that represents the denotation of such an expression. The "comprehension principles" defined in this section are additional semantic conditions that provide for the necessary individuals for every possible list, class and property expression. By this, the combination of the normative semantic conditions of the OWL 2 RDF-Based Semantics (Section 5) and the comprehension conditions can be regarded to "simulate" the semantic expressivity of the OWL 2 Direct Semantics on OWL 2 DL entailment queries, while at the same time allowing for the interpretation of arbitrary entailment queries.

The combined semantics is, however, not primarily intended for use in actual implementations. The comprehension conditions add significantly to the complexity and expressivity of the basic semantics and, in fact, lead to formal inconsistency. But the combined semantics can still be seen as a generalized reference frame for "desirable" and "useful" entailments, and this can be used, for example, to evaluate methods that syntactically transform unrestricted entailment queries in order to receive additional entailments under the OWL 2 RDF-Based Semantics. Such a concrete method is, however, outside the scope of this specification.

Note: The conventions in the introduction of Section 5 ("Semantic Conditions") apply to the current section as well.

Table 8.1 lists the comprehension conditions for sequences, i.e. RDF lists. These comprehension conditions provide the existence of sequences built from any possible combination of individuals contained in the universe.

Table 8.2 lists the comprehension conditions for boolean connectives (see Section 5.4 for the corresponding semantic conditions). These comprehension conditions provide the existence of complement classes for any class, and of unions and intersections built from any possible set of classes contained in the universe.

Table 8.3 lists the comprehension conditions for enumerations (see Section 5.5 for the corresponding semantic conditions). These comprehension conditions provide the existence of enumeration classes built from any possible set of individuals contained in the universe.

Table 8.4 lists the comprehension conditions for property restrictions (see Section 5.6 for the corresponding semantic conditions). These comprehension conditions provide the existence of cardinality restriction classes on any property and for any non-negative integer, as well as value restriction classes on any property and on any class contained in the universe.