La sémantique et la syntaxe abstraite du langage d'ontologie Web OWL

Les démonstrations (informatif)

Rédacteur :: Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies

Veuillez consulter l'errata de ce document, lequel peut contenir des corrections normatives.

Cf. également d'éventuelles traductions.

Copyright © 2004 W3C^® (MIT, ERCIM, Keio), tous droits réservés. Les règles de responsabilité, de marque commerciale, d'utilisation des document et d'octroi de licences logicielles du W3C s'appliquent.

Table des matières

Annexe A. Les démonstrations (informatif)

Cette annexe contient les démonstrations des thérèmes trouvés dans le chapitre 5 du document.

Nomenclature : Dans toute cette annexe, D représentera une application de type de donnée (cf. le chapitre 3.1) contenant les types de données de tous les types de données OWL intégrés et rdf:XMLLiteral, T représentera l'application des ontologies OWL abstraites aux graphes RDF (cf. le chapitre 4.1) et VB représentera le vocabulaire OWL intégré. Également, les littéraux ordinaires dans un vocabulaire ne seront pas mentionnés.

Remarque : Dans toute cette annexe, les interprétations seront toutes par rapport à l'application de type de donnée D. Tous les résultats seront donc par rapport à D. Quelques détails évidents des constructions sont omis.

A.1 La correspondance entre la syntaxe abstraite et OWL DL

Ce chapitre montre que les deux sémantiques, à savoir le modèle théorique direct des ontologies OWL abstraites décrit dans le chapitre 3, appelé ici modèle théorique direct, et la sémantique OWL DL décrite dans le chapitre 5, appelée ici modèle théorique OWL DL, correspondent sur certaines ontologies OWL.

Définition : Soit D comme défini précédemment, on formalise en outre un vocabulaire OWL séparé (cf. le chapitre 4.2) dans un ensemble d'appels d'adresses URI V', disjoint du vocabulaire interdit (cf. le chapitre 4.2), avec une partition disjointe de V' écrite V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP, où VC est l'ensemble de classes OWL intégrées, où VD contient les appels d'adresses URI, tous les noms de types de données de D et rdfs:Literal, où VAP contient les propriétés d'annotation OWL intégrées et où VXP contient les propriétés d'ontologie OWL intégrées.

Définition : La traduction d'un vocabulaire OWL séparé V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP, notée T(V'), se compose de tous les triplets de la forme
v rdf:type owl:Ontology, où v ∈ VO,
v rdf:type owl:Class, où v ∈ VC,
v rdf:type rdfs:Datatype, où v ∈ VD,
v rdf:type owl:Thing, où v ∈ VI,
v rdf:type owl:ObjectProperty, où v ∈ VOP,
v rdf:type owl:DatatypeProperty, où v ∈ VDP,
v rdf:type owl:AnnotationProperty, où v ∈ VAP, et
v rdf:type owl:OntologyProperty, où v ∈ VXP.

Définition : Un ensemble d'ontologies, axiomes et faits OWL DL O dans la forme de la syntaxe abstraite (cf. le chapitre 2), avec un vocabulaire séparé, (cf. le chapitre 4) est encore formalisé ici dans la notion nouvelle de vocabulaire séparé V = VO + VC + VD + VI + VOP + VDP + VAP + VXP, comme suit :

Tous les appels d'adresse URI utilisés comme noms d'ontologies proviennent de VA, comme identificateurs de classes proviennent de VC, comme identificateurs de types de données de VD, comme identificateurs d'individus de VI, comme identificateurs de propriétés à valeur d'individu de VOP, comme identificateurs de propriétés à valeur de donnée de VDP, comme identificateurs de propriétés d'annotation de VAP et comme identificateurs de propriétés d'ontologie de VXP.
Tous les appels d'adresse URI utilisés comme identificateurs d'invidus reçoivent un type dans une ontologie dans O.
Les ontologies, axiomes et faits dans O utilisent uniquement le vocabulaire réservé aux classes pour les identificateurs de classes, uniquement le vocabulaire réservé aux types de données pour les identificateurs de types de données, uniquement le vocabulaire réservé aux propriétés pour les identificateurs de propriétés à valeur de donnée, les identificateurs de propriétés à valeur d'individu, les identificateurs de propriétés d'annotation ou les identificateurs de propriétés d'ontologie, et ne mentionnent pas de vocabulaire interdit.

Le théorème à démontrer est donc le suivant : soit O et O' des ensembles d'ontologies, axiomes et faits OWL DL dans la forme de la syntaxe abstraite, clos aux importations, tel que leur union ait un vocabulaire séparé, alors O infère directement O' si et seulement si T(O) infère dans OWL DL T(O').

A.1.1 La correspondance des descriptions

Lemme 1 : Soit V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP un vocabulaire OWL séparé. Soit V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VB. Soit I' = <R,EC,ER,L,S,LV> une interprétation directe de V'. Soit I = <R_I,P_I,EXT_I,S_I,L_I,LV_I> une interprétation OWL DL de V qui satisfait à T(V'), avec LV_I = LV. Soit CEXT_I avec sa signification habituelle, et surchargeant comme toujours I pour relier une structure syntaxique à sa dénotation. Si :

R = R_I
EC(v) = CEXT_I(S_I(v)), pour v∈ VC∪VD
ER(v) = EXT_I(S_I(v)), pour v∈ VOP ∪ VDP ∪ VAP ∪ VXP
< x, S(owl:DeprecatedClass) > ∈ ER(rdf:type) si et seulement si < x, S_I(owl:DeprecatedClass) > EXT_I(S_I(rdf:type)), pour x∈R
< x, S(owl:DeprecatedProperty) > ∈ ER(rdf:type) si et seulement si < x, S_I(owl:DeprecatedProperty) > EXT_I(S_I(rdf:type)), pour x∈R
L(d) = L_I(d), pour d un littéral de donnée quelconque
S(v) = S_I(v) pour v∈ VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VO

Alors pour d, une description OWL abstraite ou une gamme de données sur V' :

I satisfait directement à T(d), et
Pour toute application A reliant tous les nœuds blancs de T(d) dans R_I, où I + A OWL DL satisfait à T(d) :
1. CEXT_I(I+A(M(T(d)))) = EC(d),
2. si d est une description, alors I+A(M(T(d)))∈CEXT_I(S_I(owl:Class)), et
3. si d est une gamme de données, alors I+A(M(T(d)))∈CEXT_I(S_I(rdfs:Datatype)).

Démonstration :

On réalise la démonstration du lemme par induction structurelle. Pour la démonstration, on a IOT = CEXT_I(I(owl:Thing)), IOC = CEXT_I(I(owl:Class)), IDC = CEXT_I(I(rdfs:Datatype)), IOOP = CEXT_I(I(owl:ObjectProperty)), IODP = - CEXT_I(I(owl:DatatypeProperty)) et IL = CEXT_I(I(rdf:List)).

Pour que l'induction fonctionne, il faut montrer que pour tout d, une description ou une gamme de données avec des sous-structures, T(d) contient des triplets pour chaque sous-structure ne partageant pas de nœuds blancs avec les triplets d'autres sous-structures. On peut aisément le vérifier à partir des règles de T.

Si p∈VOP alors I satisfait à p∈IOOP. Ensuite comme I est une interprétation OWL DL, I satisfait à <p,I(owl:Thing)>∈EXT_I(I(rdfs:domain)) et <p,I(owl:Thing)>∈EXT_I(I(rdfs:range)). Donc I satisfait à T(p). De même pour p∈VDP.

Hypothèse de base : v ∈ VC, y compris owl:Thing et owl:Nothing: Puisque v∈VC et I satisfont à T(V), alors I(v)∈CEXT_I(I(owl:Class)). Comme I est une interprétation OWL DL, CEXT_I(I(v))⊆IOT, de sorte que <I(v),I(owl:Thing)>∈EXT_I(I(rdfs:subClassOf)). Donc I OWL DL satisfait à T(v). Puisque M(T(v)) est v, alors CEXT_I(I(M(T(v))))=EC(v). D'où finalement I(v)∈IOC.
Hypothèse de base : v ∈ VD, y compris rdfs:Literal: Puisque v∈VD et I satisfont à T(V), I(v)∈CEXT_I(I(rdfs:Datatype)). Comme I est une interprétation OWL DL, CEXT_I(I(v))⊆LV_I, de sorte que <I(v),I(rdfs:Literal)>∈EXT_I(I(rdfs:subClassOf)). Donc I compatible RDF satisfait à T(v). Puisque M(T(v)) est v, alors CEXT_I(I(M(T(v))))=EC(v). D'où finalement I(v)∈IDC.
Hypothèse de base : d=oneOf(i₁…i_n), où les i_j sont des identificateurs d'individus: Comme i_j∈VI pour 1 ≤ j ≤ n et que I satisfait à T(V), alors I(i_j)∈IOT. Le deuxième principe de compréhension des suites impose qu'il existe un élément l∈IL qui soit une suite de I(i₁),…,I(i_n) sur IOT. Pour tout l, qui est une suite I(i₁),…,I(i_n) sur IOT, le principe de compréhension de owl:oneOf impose l'existence d'un y∈CEXT_I(I(rdfs:Class)) tel que <y,l> ∈ EXT_I(IS(owl:oneOf)). De la troisième caractérisation de owl:oneOf, y∈IOC. Par conséquent, I satisfait à T(d). Pour tout I+A qui satisfait à T(d), CEXT_I(I+A(M(T(d)))) = {I(i₁),…,I(i_n)} = EC(d). Finalement, I+A(M(T(d)))∈IOC.
Hypothèse de base : d=oneOf(v₁…v_n), où v_i est un littéral de donnée: Puisque I(v_j)∈LV_I, le deuxième principe de compréhension des suites impose donc qu'il existe un l∈IL qui soit une suite I(v₁),…,I(v_n) sur LV_I. Pour tout L, qui est une suite I(v₁),…,I(v_n) sur LV_I, le principe de compréhension de owl:oneOf impose l'existence d'un y∈CEXT_I(I(rdfs:Class)) tel que <y,l> ∈ EXT_I(IS(owl:oneOf)). De la deuxième caractérisaiton de owl:oneOf, y∈IOC. Par conséquent, I satisfait à T(d). Pour tout I+A qui satisfait à T(d), CEXT_I(I+A(M(T(d)))) = {I(i₁),…,I(i_n)} = EC(d). Finalement, I+A(M(T(d)))∈IDC.
Hypothèse de base : d=restriction(p value(i)), avec p∈VOP∪VDP et i un identificateur d'individu: Comme p∈VOP∪VDP, de précédemment I satisfait à T(p). Comme I satisfait à T(V'), I(p)∈IOOP∪IODP. Comme i∈VI et I satisfont à T(V'), I(i)∈IOT. D'après un principe de compréhension de restriction, I satisfait à T(d). Pour toute application A, tel que I+A satisfait à T(d), CEXT_I(I+A(M(T(d)))) = {x∈IOT | <x,I(i)> ∈ EXT_I(p)} = {x∈R | <x,S(i)> ∈ ER(p)} = EC(d). Finalement, I+A(M(T(d)))∈IOC.
Hypothèse de base : d=restriction(p value(i)), avec p∈VOP∪VDP et i une valeur de donnée typée.: Similaire.
Hypothèse de base : d=restriction(p minCardinality(n)), avec p∈VOP∪VDP et n un entier non négatif: Similaire.
Hypothèse de base : d=restriction(p maxCardinality(n)), avec p∈VOP∪VDP et n un entier non négatif: Similaire.
Hypothèse de base : d=restriction(p Cardinality(n)), avec p∈VOP∪VDP et n un entier non négatif: Similaire.
Hypothèse inductive : d=complementOf(d'): D'après l'hypothèse inductive, I satisfait à T(d'). Comme d' est une description, d'après l'hypothèse inductive, il existe une application A qui relie tous les nœuds blancs dans T(d') aux éléments du domaine, tel que I+A satisfait à T(d') et I+A(M(T(d'))) = EC(d') et I+A(M(T(d')))∈IOC. Le principe de compréhension de owl:complementOf impose alors que s'il existe un y∈IOC tel que I+A satisfait à <y,e>∈EXT_I(I(owl:complementOf)), donc I satisfait à T(d). Pour tout I+A qui satisfait à T(d), CEXT_I(I+A(M(T(d)))) = IOT-CEXT_I(I+A(M(T(d)))) = R-EC(d') = EC(d). Finalement, I+A(M(T(d)))∈IOC.
Hypothèse inductive : d = unionOf(d₁ … d_n): D'après l'hypothèse inductive, I satisfait à d_i, pour 1 ≤ i ≤ n, de sorte qu'il existe un A_i qui relie tous les nœuds blancs dans T(d_i) aux éléments du domaine tel que I+A_i satisfait T(d_i). Comme les nœuds blancs dans T(d_i) sont disjoints des nœuds blancs de T(d_j), pour i≠j, I+A₁+…+A_n et donc I satisfait à T(d_i)∪…∪T(d_n). Chaque d_i est une description, donc, d'après l'hypothèse inductive, I+A₁+…+A_n(M(T(d_i)))∈IOC. Le premier principe de compréhension des suites impose alors l'existence d'un l∈IL qui soit une suite I+A₁+…+A_n(M(T(d₁))),…,I+A₁+…+A_n(M(T(d_n))) sur IOC. Le principe de compréhension de owl:unionOf impose alors l'existence d'un y∈IOC tel que <y,l>∈EXT_I(I(owl:unionOf)), ainsi I satisfait à T(d).
Pour tout I+A qui satisfait à T(d), I+A satisfait à T(d_i), donc CEXT_I(I+A(d_i)) = EC(d_i)). Et ensuite CEXT_I(I+A(M(T(d)))) = CEXT_I(I+A(d₁))∪…∪CEXT_I(I+A(d_n)) = EC(d₁)∪…∪EC(d_n) = EC(d). Finalement, I(M(T(d)))∈IOC.
Hypothèse inductive : d = intersectionOf(d₁ … d_n): Similaire.
Hypothèse inductive : d = restriction(p x₁ x₂ … x_n): Puisque p∈VOP∪VDP, de précédemment I satisfait à T(p). D'après l'hypothèse inductive, I satisfait à restriction(p x_i) pour 1 ≤ i ≤ n, de sorte qu'il existe un A_i reliant tous les nœuds blancs dans T(restriction(p x_i)) aux éléments du domaine, tel que I+A_i satisfait à T(restriction(p x_i)). Comme les nœuds blancs dans T(restriction(p x_i)) sont disjoints de ceux de T(restriction(p x_j)), pour i≠j, I+A₁+…+A_n, et donc I satisfait à T(restriction(p x₁ … x_n)). Chaque restriction(p x_i) étant une description, donc d'après l'hypothèse inductive M(T(restriction(p x_i)))∈IOC. Le premier principe de compréhension des listes impose alors l'existence d'un l∈IL qui soit une suite I+A₁+…+A_n(M(T(restriction(p x_i)))),…,I+A₁+…+A_n(M(T(restriction(p x_i)))) sur IOC. Le principe de compréhension de owl:intersectionOf impose alors l'existence d'un y∈IOC tel que <y,l>∈EXT_I(I(owl:intersectionOf)), et donc I satisfait à T(d).
Pour tout I+A qui satisfait à T(d), I+A satisfait à T(d_i), et donc CEXT_I(I+A(d_i)) = EC(d_i)). Ensuite CEXT_I(I+A(M(T(d)))) = CEXT_I(I+A(restriction(p x_i)))∩…∩ CEXT_I(I+A(restriction(p x_n))) = EC(restriction(p x_i))cap;…∩EC(restriction(p x_i)) = EC(d). Finalement, I(M(T(d)))∈IOC.
Hypothèse inductive : d = restriction(p allValuesFrom(d')), avec p∈VOP∪VDP et d' une description: Puisque p∈VOP∪VDP, de précédemment I satisfait à T(p). D'après l'hypothèse inductive, I satisfait à T(d'). Comme d' est une description, d'après l'hypothèse inductive, toute application A qui relie tous les nœuds blancs dans T(d') aux éléments du domaine tel que I+A satisfait à T(d'), aura I+A(M(T(d'))) = EC(d') et I+A(M(T(d')))∈IOC. Puisque p∈VOP∪VDP et I satisfait à T(V'), on a I(p)∈IOOP∪IODP. Le principe de compréhension de restriction owl:allValuesFrom impose alors que I satisfait aux triplets dans T(d) non dans T(d') ou dans T(p), d'une sorte que I satisfait à T(d).
Pour tout I+A qui satisfait à T(d), CEXT_I(I+A(M(T(d)))) = {x∈IOT | ∀ y∈IOT : <x,y>∈EXT_I(p) implique que y∈CEXT_I(M(T(d')))} = {x∈R | ∀ y∈R : <x,y>∈ER(p) implique y∈EC(d')} = EC(d). Finalement, I+A(M(T(d)))∈IOC.
Hypothèse inductive : d = restriction(p someValuesFrom(d)), avec p∈VOP∪VDP et d' une description: Similaire.
Hypothèse inductive : d = restriction(p allValuesFrom(d)), avec p∈VOP∪VDP et d' un éventail de données: Similaire.
Hypothèse inductive : d = restriction(p someValuesFrom(d)), avec p∈VOP∪VDP et d' un éventail de données: Similaire.

Lemme 1.1 : Soit V', V, I' et I comme dans le lemme 1. Soit d une structure individuelle OWL abstraite sur V' (de la forme Individual(…)). Alors, pour toute application A reliant les nœuds blancs de T(d) dans R_I, où I+A OWL DL satisfait T(d), I+A(M(T(d))) ∈ EC(d). Également, pour tout r∈EC(d), il existe une application A qui relie tous les nœuds blancs de T(d) dans R_I tel que I+A(M(T(d))) = r.

Démonstration :

Un argument inductif simple montre que I+A(M(T(d))) doit satisfaire à toutes les conditions de EC(d). Un autre argument inductif, s'appuyant sur le non-partage des nœuds blancs dans les sous-structures, montre que pour chaque r∈EC(d) il existe une application A tel que I+A(M(T(d))) = r.

A.1.2 La correspondance des directives

Lemme 1.9 : Soit V', V, I' et I comme dans le lemme 1. Soit F une directive OWL sur V' avec une annotation de la forme annotation(p x). Si F est un axiome de classe ou de propriété, n est le nom de la classe ou de la propriété. Si F est un axiome d'individu, n est le nœud principal de T(F). Alors pour toute application A reliant tous les nœuds blancs de T(F) dans R_I, I+A OWL DL satisfait aux triplets résultant de l'annotation, si et seulement si I' satisfait directement aux conditions résultant de l'annotation.

Démonstration :

Pour les annotations sur des appels d'adresses URI, on peut aisément établir le lemme en inspectant la condition sémantique et les triplets de traduction. Pour les annotations sur Individual(…), il faut également utiliser le lemme 1.1.

Lemme 2 : Soit V', V, I' et I comme dans le lemme 1. Soit F une directive OWL sur V'. Alors I satisfait à T(F) si et seulement si I' satisfait à F.

Démonstration :

La partie principale de la démonstration consiste en une induction structurelle sur les directives. Les annotations apparaissent dans beaucoup de directives et fonctionnent exactement pareil, il faut juste utiliser le lemme 1.9 Le reste de la démonstration ignorera donc les annotations. Les contre-indications seront interprétées de la même façon, et ignorées également dans la suite de la démonstration.

Hypothèse : F = Class(foo complete d₁ … d_n)

Soit d=intersectionOf(d₁ … d_n). Puisque d est une description sur V', alors I satisfait à T(d) et, pour toute application A reliant les nœuds blancs de T(d) tel que I+A satisfait à T(d), CEXT_I(I+A(M(T(d)))) = EC(d). Ainsi, pour toute sous-description d' de d, CEXT_I(I+A(M(T(d')))) = EC(d') et I+A(M(T(d')))∈IOC. Alors pour une application A reliant les nœuds blancs de T(d) tel que I+A satisfait à T(d), CEXT_I(I+A(M(T(d)))) = EC(d) et I+A(M(T(d)))∈IOC, et pour chaque sous-description d' de d, on a CEXT_I(I+A(M(T(d')))) = EC(d') et I+A(M(T(d')))∈IOC.

Si I' satisfait à F, alors EC(foo) = EC(d). De précédemment, s'il existe une applicaton A tel que CEXT_I(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXT_I(I(foo)) et I+A(M(T(d)))∈IOC. Puisque I satisfait à T(V), I(foo)∈IOC, alors <I(foo),I+A(M(T(d)))> ∈ EXT_I(I(owl:equivalentClass)). En outre, à cause des conditions sémantiques sur I(owl:intersectionOf), on a <I(foo),I+A(M(T(SEQ d₁ … d_n)))> ∈ EXT_I(I(owl:intersectionOf)).

Si d est de la forme intersectionOf(d₁), alors CEXT_I(I+A(M(T(d₁)))) = EC(d₁) = EC(d) = EC(foo) et I+A(M(T(d₁)))∈IOC. Ainsi, d'après les conditions sémantiques sur I(owl:equivalentClass), <I(foo),I+A(M(T(d₁)))> ∈ EXT_I(I(owl:equivalentClass)). Si d₁ est de la forme complementOf(d'₁), alors IOT - CEXT_I(I+A(M(T(d'₁)))) = CEXT_I(I+A(M(T(d₁)))) = EC(d₁) = EC(d) = EC(foo) et I+A(M(T(d'₁)))∈IOC. Ainsi, d'après les conditions sémantiques sur I(owl:complementOf), <I(foo),I+A(M(T(d'₁)))> ∈ EXT_I(I(owl:complementOf)). Si d₁ est de la forme unionOf(d₁₁ … d_1m), alors CEXT_I(I+A(M(T(d₁₁)))) ∪ … ∪ CEXT_I(I+A(M(T(d_1m)))) = CEXT_I(I+A(M(T(d₁)))) = EC(d₁) = EC(d) = EC(foo) et I+A(M(T(d_1j)))∈IOC, pour 1 ≤ j ≤ m. Ainsi, d'après les conditions sémantiques sur I(owl:unionOf), <I(foo),I+A(M(T(SEQ d₁₁ … d_1m)))> ∈ EXT_I(I(owl:unionOf)).

Par conséquent, I satisfait à T(F), pour chaque T(F) potentiel.

Si I satisfait à T(F), alors I satisfait à T(intersectionOf(d₁ … d_n)). Comme précédemment, il existe donc une certaine application A tel que <I(foo),I+A(M(T(d)))> ∈ EXT_I(I(owl:equivalentClass)). Ainsi EC(d) = CEXT_I(I+A(M(T(d)))) = CEXT_I(I(foo)) = EC(foo). Par conséquent I' satisfait à F.

Hypothèse : F = Class(foo partial d₁ … d_n)

Soit d=intersectionOf(d₁ … d_n). Puisque d est une description sur V', alors I satisfait à T(d) et, pour toute application A reliant les nœuds blancs de T(d) tel que I+A satisfait à T(d), on a CEXT_I(I+A(M(T(d)))) = EC(d). Ainsi, CEXT_I(I+A(M(T(d_i)))) = EC(d_i), pour 1 ≤ i ≤ n. Alors, pour une application A reliant les nœuds blancs de T(d) tel que I+A satisfait à T(d), on a CEXT_I(I+A(M(T(d_i)))) = EC(d_i) et I+A(M(T(d_i))∈IOC, pour 1 ≤ i ≤ n.

Si I' satisfait à F, alors EC(foo) ⊆ EC(d_i), pour 1 ≤ i ≤ n. De précédemment, il existe une application A tel que CEXT_I(I+A(M(T(d_i)))) = EC(d_i) ⊇ EC(foo) = CEXT_I(I(foo)) et I+A(M(T(d_i))∈IOC. Comme I satisfait à T(V), I(foo)∈IOC, alors <I(foo),I+A(M(T(d_i)))> ∈ EXT_I(I(rdfs:subClassOf)), pour 1 ≤ i ≤ n. Par conséquent I satisfait à T(F).

Si I satisfait à T(F), alors I satisfait à T(d_i), pour 1 ≤ i≤ n. Ainsi, il existe une application A, comme précédemment, tel que <I(foo),I+A(M(T(d_i)))> ∈ EXT_I(I(rdfs:subClassOf)), pour 1 ≤ i ≤ n. Ainsi, EC(d) = CEXT_I(I+A(M(T(d_i)))) ⊇ CEXT_I(I(foo)) = EC(foo), pour 1 ≤ i ≤ n. Par conséquent, I' satisfait à F.

Hypothèse : F = EnumeratedClass(foo i₁ … i_n)

Soit d=oneOf(i₁ … i_n). Puisque d est une description sur V', alors I satisfait à T(d) et, pour une application A reliant les nœuds blancs de T(d) tel que I+A satisfasse à T(d), on a EC(d) = CEXT_I(I+A(M(T(d)))) = {S_I(M(T(i₁)), … S_I(M(T(i_n))}. On a également S_I(M(T(i_j)) ∈ IOT, pour 1 ≤ j ≤ n.

Si I' satisfait à F, alors EC(foo) = EC(d). De précédemment, il existe une application A tel que CEXT_I(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXT_I(I(foo)) et I+A(M(T(d))∈IOC. Soit e, I+A(M(T(SEQ i₁ … i_n))). Alors, d'après les conditions sémantiques sur I(owl:oneOf), on a <I(foo),e> ∈ EXT_I(I(owl:oneOf)). Par conséquent, I satisfait à T(F).

Si I satisfait à T(F), alors I satisfait à T(SEQ i₁ … i_n). Ainsi, il existe une application A, comme précédemment, tel que <I(foo),I+A(M(T(SEQ i₁ … i_n)))> ∈ EXT_I(I(owl:oneOf)). Ainsi, {S_I(M(T(i₁)), …, S_I(M(T(i_n))} = CEXT_I(I(foo)) = EC(foo). Par conséquent I' satisfait à F.

Hypothèse : F = Datatype(foo)

La seule chose à montrer ici est le typage de foo, qui est similaire à celui des classes.

Hypothèse : F= DisjointClasses(d₁ … d_n)

Puisque d_i est une description sur V', alors I satisfait à T(d_i), et pour toute application A reliant les nœuds blancs de T(d_i) tel que I+A satisfait à T(d_i), CEXT_I(I+A(M(T(d_i)))) = EC(d_i).

Si I satisfait à T(F), alors, pour 1 ≤ i ≤ n, il existe une application A_i tel que I satisfait à <I+A_i(M(T(d_i))),I+A_j(M(T(d_j)))> ∈ EXT_I(I(owl:disjointWith)), pour chaque 1 ≤ i < j ≤ n. Ainsi, on a EC(d_i)∩EC(d_j) = {}, pour i ≠ j. Par conséquent, I' satisfait à F.

Si I' satisfait à F, alors EC(d_i)∩EC(d_j) = {}, pour i ≠ j. Pour toute application A_i et A_j, comme précédemment, on a <I+A_i+A_j(M(T(d_i))),I+A_i+A_j(M(T(d_j)))> ∈ EXT_I(I(owl:disjointWith)), pour i ≠ j. Comme il existe au moins une application A_i pour chaque i et que les nœuds blancs de T(d_j) sont tous disjoints, alors I+A₁+…+A_n satisfait à T(DisjointClasses(d₁ … d_n)). Par conséquent, I satisfait à T(F).

Hypothèse : F = EquivalentClasses(d₁ … d_n)

Similaire.

Hypothèse : F = SubClassOf(d₁ d2)

Similaire dans une certaine mesure.

Hypothèse : F = ObjectProperty(p super(s₁) … super(sn) domain(d₁) … domain(d_m) range(r₁) … range(r_k) [inverse(i)] [Symmetric] [Functional] [InverseFunctional] [OneToOne] [Transitive])

Puisque d_i, pour 1 ≤ i ≤ m est une description sur V', alors I satisfait à T(d_i) et, pour toute application A reliant les nœuds blancs de T(d_i) tel que I+A satisfait à T(d_i), on a CEXT_I(I+A(M(T(d_i)))) = EC(d_i). De même pour r_i, pour 1 ≤ i ≤ k.

Si I' satisfait à F, alors, comme p∈VOP, I satisfait à I(p)∈IOOP. Ensuite, comme I est une interprétation OWL DL, alors I satisfait à <I(p),I(owl:Thing)>∈EXT_I(I(rdfs:domain)) et à <I(p),I(owl:Thing)>∈EXT_I(I(rdfs:range)). Également, ER(p)⊆ER(s_i), pour 1 ≤ i ≤ n, de sorte que EXT_I(I(p))=ER(p) ⊆ ER(s_i)=EXT_I(I(s_i)) et que I satisfait à <I(p),I(s_i)>∈EXT_I(I(rdfs:subPropertyOf)). Alors, ER(p)⊆EC(d_i)×R, pour 1 ≤ i ≤ m, de sorte que <z,w>∈ER(p) implique z∈EC(d_i) et que, pour toute application A tel que I+A satisfait à T(d_i), <z,w>∈EXT_I(p) implique z∈CEXT_I(I+A(M(T(d_i)))), et donc <I(p),I+A(M(T(d_i)))>∈EXT_I(I(rdfs:domain)). De même pour r_i, pour 1 ≤ i ≤ k.

Si I' satisfait à F et inverse(i) est dans F, alors ER(p) et ER(i) sont réciproques. Ainsi, on a <u,v>∈ER(p) si et seulement si <v,u>∈ER(i) de sorte que <u,v>∈EXT_I(p) si et seulement si <v,u>∈EXT_I(i) et I satisfait à <I(p),I(i)>∈EXT_I(I(owl:inverseOf)). Si I' satisfait à F et Symmetric est dans F, alors ER(p) est symétrique. De cette façon, si <x,y>∈ ER(p), alors <y,x>∈ER(p), de sorte que si <x,y> ∈ EXT_I(p), alors <y, x>∈EXT_I(p). Et donc I satisfait à p∈CEXT_I(I(owl:Symmetric)). De même pour Functional, InverseFunctional et Transitive. Par conséquent, si I' satisfait à F, alors I satisfait à T(F).

Si I satisfait à T(F), alors, pour 1 ≤ i ≤ n, <I(p),I(s_i)>∈EXT_I(I(rdfs:subPropertyOf)), de sorte que ER(p)=EXT_I(I(p)) ⊆ EXT_I(I(s_i))=ER(s_i). Également, pour 1 ≤ i ≤ m, pour une application A tel que I+A satisfait à T(d_i), <I(p),I+A(M(T(d_i)))>∈EXT_I(I(rdfs:domain)), de sorte que <z,w>∈EXT_I(p) implique z∈CEXT_I(I+A(M(T(d_i)))). Par conséquent, <z,w>∈ER(p) implique z∈EC(d_i) et ER(p)⊆EC(d_i)×R. De même pour r_i, pour 1 ≤ i ≤ k.

Si I satisfait à T(F) et inverse(i) est dans F, alors I satisfait à <I(p),I(i)>∈EXT_I(I(owl:inverseOf)). Ainsi, on a <u,v>∈EXT_I(p) si et seulement si <v,u>∈EXT_I(i), de sorte que <u,v>∈ER(p) si et seulement si <v,u>∈ER(i) et si ER(p) et ER(i) sont réciproques. Si I satisfait à F et si Symmetric est dans F, alors I satisfait à p∈CEXT_I(I(owl:Symmetric)), de sorte que si <x,y> ∈ EXT_I(p), alors <y, x>∈EXT_I(p). Par conséquent, si <x,y>∈ ER(p) alors <y,x>∈ER(p) et ER(p) est symétrique. De même pour Functional, InverseFunctional et Transitive. Donc, si I satisfait à T(F), alors I' satisfait à F.

Hypothèse : F = DatatypeProperty(p super(s₁) … super(sn) domain(d₁) … domain(d_m) range(r₁) … range(r_l) [Functional])

Similaire, mais plus simple.

Hypothèse : F = AnnotationProperty(p domain(d₁) … domain(d_m))

Similaire, mais encore plus simple.

Hypothèse : F = OntologyProperty(p domain(d₁) … domain(d_m))

Similaire, mais encore plus simple.

Hypothèse : F = EquivalentProperties(p₁ … p_n), pour p_i∈VOP

Puisque p_i∈VOP et I satisfait à T(V'), alors I(p_i)∈IOOP. Si I satisfait à T(F), alors <I(p_i),I(p_j)> ∈ EXT_I(I(owl:equivalentProperty)), pour chaque 1 ≤ i < j ≤ n. Par conséquent, EXT_I(p_i) = EXT_I(p_j), pour chaque 1 ≤ i < j ≤ n ; ER(p_i) = ER(p_j), pour chaque 1 ≤ i < j ≤ n ; et I' satisfait à F.

Si I' satisfait à F, alors ER(p_i) = ER(p_j), pour chaque 1 ≤ i < j ≤ n. Par conséquent, EXT_I(p_i) = EXT_I(p_j), pour chaque 1 ≤ i < j ≤ n. D'après la définition OWL DL de owl:equivalentProperty, on a <I(p_i),I(p_j)> ∈ EXT_I(I(owl:equivalentProperty)), pour chaque 1 ≤ i < j ≤ n. De sorte que I satisfait à T(F).

Hypothèse : F = SubPropertyOf(p₁ p₂)

Un peu similaire, mais plus simple.

Hypothèse : F = SameIndividual(i₁ … i_n)

Similaire à SamePropertyAs.

Hypothèse : F = DifferentIndividuals(i₁ … i_n)

Similaire à SamePropertyAs.

Hypothèse : F = Individual([i] type(t₁) … type(t_n) value(p₁ v₁) … value(p_n v_n))

Si I satisfait à T(F), alors il existe une application A qui relie chaque nœud blanc dans T(F) tel que I+A satisfait à T(F). Un simple examen de T(F) montre que les applications A plus celles des identificateurs d'individu dans F sont toutes dans IOT, et donc que I' satisfait à F.

Si I' satisfait à F, alors pour chaque structure Individual dans F, il doit exister un élément de R qui fait la relation de type et la vérifie dans F. Les triplets dans T(F) tombent alors dans trois catégories : (1) Les relations de type aux structures owl:Thing, qui sont vérifiées dans I parce que les éléments décrits précédemment appartiennent à R ; (2) Les relations de type aux descriptions OWL, qui sont vérifiées dans I parce qu'elles le sont dans I' d'après le lemme 1 ; (3) Les relations des propriétés OWL, qui sont vérifiées dans I' parce qu'elles le sont dans I. Par conséquent I satisfait à T(F).

A.1.3 De la sémantique RDF à la sémantique directe

Lemme 3 : Soit V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP, un vocabulaire OWL séparé. Soit V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VB. Alors pour chaque interprétation OWL DL I = <R_I,P_I,EXT_I,S_I,L_I,LV_I> de V qui satisfait à T(V'), il existe une interprétation directe I' de V' tel que pour tout ensemble d'ontologies abstraites, axiomes et faits OWL O de vocabulaire V', tel que O est clos aux importations, I' satisfait directement à O si et seulement si I OWL DL satisfait à T(O).

Démonstration :

Soit CEXT_I défini normalement d'après I. L'interprétation directe obligatoire sera I' = < R_I, EC, ER, L, S, LV_I >, où :

EC(v) = CEXT_I(S_I(v)), pour v∈VC∪VD
ER(v) = EXT_I(S_I(v)), pour v∈VOP∪VDP∪VAP∪VXP
< x, S(owl:DeprecatedClass) > ∈ ER(rdf:type) si et seulement si < x, S_I(owl:DeprecatedClass) > EXT_I(S_I(rdf:type)), pour x ∈ R
< x, S(owl:DeprecatedProperty) > ∈ ER(rdf:type) si et seulement si < x, S_I(owl:DeprecatedProperty) > EXT_I(S_I(rdf:type)), pour x ∈ R
L(d) = L_I(d), pour d un littéral typé
S(v) = S_I(v), pour n∈VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VO

V', V, I' et I remplissent les conditions du lemme 2, donc pour toute directive D sur V', I satisfait à T(D) si et seulement si I' satisfait à D.

Puisque O est clos aux importations, alors O inclut toutes les ontologies importées dans T(O), de sorte que la partie importation des directives d'importation sera traitée pareil. Satisfaire à une ontologie abstraite revient simplement à satisfaire à ses directives, et satisfaire à la traduction d'un ontologie abstraite revient à satisfaire à tous les triplets, donc I OWL DL satisfait à T(K) si et seulement si I' satisfait directement K.

A.1.4 De la sémantique directe à la sémantique RDF

Lemme 4 : Soit V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP un vocabulaire OWL séparé. Soit V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VB. Alors pour chaque interprétation directe I' = < U, EC, ER, L, S, LV > de V', il existe une interprétation OWL DL I de V qui satisfait à T(V') tel que, pour tout ensemble d'ontologies abstraites, axiomes et faits OWL O de vocabulaire V', tel que O est clos aux importations, I' satisfait directement à O si et seulement si I OWL DL satisfait à T(O).

Démonstration :

Construire I = < R_I, P_I, EXT_I, S_I, L, LV_I > comme suit :

Soit IOC l'ensemble de toutes les descriptions OWL sur V', plus le vocabulaire réservé aux classes.
Soit IDC l'ensemble de toutes les gammes de données OWL sur V'.
Soit IOP = VOP ∪ VDP ∪ VAP ∪ VXP, plus le vocabulaire réservé aux propriétés.
Soit IX = VO.
Soit IL, rdf:nil plus les suites finies sur U, sur IOC et sur LV.
Soit IAD, rdf:nil plus les suites finies sur U.
Soit IV, le vocabulaire interdit moins rdf:nil.
Soit R_I, l'union disjointe de U, IOC, IDC, IOP, IX, IL, IAD et IV.
Soit P_I, IOP ∪ IV
Soit LV_I = LV.
Soit S_I(n) = S(n) pour n∈VI.
Soit S_I(n) = n pour n∈V-VI.
CEXT_I(c)=EC(c), pour c∈IOC, sinon c'est {}.
Pour d∈IDC, CEXT_I(d)=EC(d).
Pour x∈U∪IL∪IAD∪IOP∪IX, CEXT_I(x)={}.
CEXT_I(S_I(rdf:type)) = {}
CEXT_I(S_I(rdf:Property)) = P_I
CEXT_I(S_I(rdf:List)) = IL
CEXT_I(S_I(rdf:XMLLiteral)) représente les valeurs littérales XML RDF
CEXT_I(S_I(rdf:first)) = CEXT_I(S_I(rdf:rest)) = CEXT_I(S_I(rdfs:domain)) = CEXT_I(S_I(rdfs:range)) = {}
CEXT_I(S_I(rdfs:Resource)) = R_I
CEXT_I(S_I(rdfs:Literal)) = LV_I
CEXT_I(S_I(rdfs:Datatype)) = D
CEXT_I(S_I(rdfs:Class)) = IOC ∪ IV
CEXT_I(S_I(rdfs:subClassOf)) = CEXT_I(S_I(rdfs:subPropertyOf)) = CEXT_I(S_I(rdfs:member)) = {}
CEXT_I(S_I(rdfs:Container)) = CEXT_I(S_I(rdf:Seq)) ∪ CEXT_I(S_I(rdf:Bag)) ∪ CEXT_I(S_I(rdf:Alt))
CEXT_I(S_I(rdfs:ContainerMembershipProperty)) représente les propriétés de membre de conteneur RDF
Pour r∈IOP, EXT_I(r)=ER(r) si défini, sinon {}
EXT_I(S_I(rdf:type)) est déterminé par CEXT_I.
EXT_I(S_I(rdf:Property)) = EXT_I(S_I(rdf:List)) = EXT_I(S_I(rdf:XMLLiteral)) = {}
<x,y> ∈ EXT_I(rdf:first) si et seulement si x∈IL et si y est son premier élément.
<x,y> ∈ EXT_I(rdf:rest) si et seulement si x∈IL et si y est le dernier élément.
EXT_I(S_I(rdfs:domain)) = { <x,y> : x∈IOP y∈IOC ∧ ∀ w, <w,z> ∈ EXT_I(x) implique w ∈ CEXT_I(y) }
EXT_I(S_I(rdfs:range)) = { <x,y> : x∈OP y∈IOC ∧ ∀ z, <w,z> ∈ EXT_I(x) implique z ∈ CEXT_I(y) }
EXT_I(S_I(rdfs:Resource)) = EXT_I(S_I(rdfs:Literal)) = EXT_I(S_I(rdfs:Datatype)) = EXT_I(S_I(rdfs:Class)) = {}
EXT_I(S_I(rdfs:subClassOf)) = { <x,y> : x,y∈IOC ∧ CEXT_I(x) ⊆ CEXT_I(y) }
EXT_I(S_I(rdfs:subPropertyOf)) = { <x,y> : x,y∈OP ∧ EXT_I(x) ⊆ EXT_I(y) }
EXT_I(S_I(rdfs:member)) est l'union des extensions de propriétés de membre de conteneur
EXT_I(S_I(rdfs:Container)) = EXT_I(S_I(rdfs:ContainerMembershipProperty)) = {}
Les extensions de owl:allValuesFrom, owl:cardinality, owl:hasValue, owl:maxCardinality, owl:minCardinality, owl:onProperty et owl:someValuesFrom apparaissent au besoin afin de relier les éléments de IOC et de IDC à leurs parties. Leurs extensions de classe sont toutes vides.
Les extensions de owl:complementOf, owl:intersectionOf, owl:oneOf et owl:unionOf apparaissent au besoin afin que leurs conditions sémantiques fonctionnent correctement. Leurs extensions de classe sont toutes vides. On peut aisément le faire ici parce que la modification de ces extensions n'induit pas de boucles dans le processus.
CEXT_I(S_I(owl:AnnotationProperty)) = VAP
CEXT_I(S_I(owl:OntologyProperty)) = VXP
CEXT_I(S_I(owl:Class)) = IOC
CEXT_I(S_I(owl:DatatypeProperty)) = VDP
CEXT_I(S_I(owl:FunctionalProperty)) représente ces éléments de VOP∪VDP dont l'extension est fonctionnelle partielle.
CEXT_I(S_I(owl:InverseFunctionalProperty)) représente ces éléments de VOP dont l'extension est fonctionnelle partielle symétrique.
CEXT_I(S_I(owl:ObjectProperty)) = VOP
CEXT_I(S_I(owl:Ontology)) = VO
CEXT_I(S_I(owl:Restriction)) représente ces éléments de IOC qui sont des restrictions OWL.
CEXT_I(S_I(owl:SymmetricProperty)) représente ces éléments de VOP dont l'extension est symétrique.
CEXT_I(S_I(owl:TransitiveProperty)) représente ces éléments de VOP dont l'extension est transitive.
EXT_I(S_I(owl:AnnotationProperty)) = EXT_I(S_I(owl:OntologyProperty)) = EXT_I(S_I(owl:Class)) = EXT_I(S_I(owl:DatatypeProperty)) = EXT_I(S_I(owl:FunctionalProperty)) = EXT_I(S_I(owl:InverseFunctionalProperty)) = EXT_I(S_I(owl:ObjectProperty)) = EXT_I(S_I(owl:Ontology)) = EXT_I(S_I(owl:Restriction)) = EXT_I(S_I(owl:SymmetricProperty)) = EXT_I(S_I(owl:TransitiveProperty)) = {}
CEXT_I(S_I(owl:AllDifferent)) se compose des éléments de IAD ayant une propriété owl:distinctMembers.
EXT_I(S_I(owl:differentFrom)) est la relation d'inéquation sur U.
EXT_I(S_I(owl:disjointWith)) relie les membres de IOC qui ont des extensions de classe disjointes
EXT_I(S_I(owl:distinctMembers)) relie les éléments de IAD à leur copie dans IL, mais seulement pour les suites d'individus distincts.
EXT_I(S_I(owl:equivalentClass)) relie les membres de IOC qui ont la même extension de classe.
EXT_I(S_I(owl:equivalentProperty)) relie les membres de IOP∪IDP qui ont la même extension.
EXT_I(S_I(owl:inverseOf)) relie les membres de IOP dont les extensions sont symétriques l'une par rapport à l'autre.
EXT_I(S_I(owl:sameAs)) est la relation d'égalité sur U.
EXT_I(S_I(owl:AllDifferent)) = CEXT_I(S_I(owl:differentFrom)) = CEXT_I(S_I(owl:disjointWith)) = CEXT_I(S_I(owl:distinctMembers)) = CEXT_I(S_I(owl:equivalentClass)) = CEXT_I(S_I(owl:equivalentProperty)) = CEXT_I(S_I(owl:inverseOf)) = CEXT_I(S_I(owl:sameAs)) = {}
CEXT_I(S_I(owl:DeprecatedClass)) = { x ∈ IOC∪IDC : <x,S(owl:DeprecatedClass)>∈ER(rdf:type) }
CEXT_I(S_I(owl:DeprecatedProperty)) = { x ∈ IOOP∪IODP : <x,S(owl:DeprecatedProperty)>∈ER(rdf:type) }
EXT_I(S_I(owl:DeprecatedClass)) = EXT_I(S_I(owl:DeprecatedProperty)) = {}

Donc I est une interprétation OWL DL parce que les conditions des extensions de classes dans OWL DL correspondent aux conditions des structures pareilles à des classes de la syntaxe abstraite OWL.

V', V, I' et I satisfont aux conditions du lemme 2, donc pour toute directive D sur V', i satisfait à T(D) si et seulement si I' satisfait à D.

Puisque O est clos aux importations, O inclut toutes les ontologies importées dans T(O) et la partie importation des directives d'importation sera traitée pareil. Satisfaire à une ontologie abstraite revient simplement à satisfaire à ses directives, et satisfaire à la traduction d'une ontologie abstraite revient à satisfaire à tous les triplets, donc I OWL DL satisfait à T(K) si et seulement si I' satisfait directement à K.

A.1.5 Le théorème de correspondance

Théorème 1 : Soit O et O' des ensembles d'ontologies, axiomes et faits OWL dans la forme de la syntaxe abstraite, clos aux importations, tel que leur union ait un vocabulaire séparé V' et tel que chaque appel d'adresse URI dans V' soit utilisé dans O. Alors O infère O' si et seulement si T(O) infère dans OWL DL T(O').

Donc I satisfait à T(V'), parce que chaque appel d'adresse URI dans V' est utilisé sur O.

Démonstration : Supposons que O infère O'. Soit I, une interprétation OWL DL qui satisfait à T(O). Alors, d'après le lemme 3, il existe une interprétation directe I' tel que, pour toute ontologie abstraite OWL, ou tout axiome OWL, ou tout fait OWL X sur V', I satisfait à T(X) si et seulement si I' satisfait à X. Donc I' satisfait à chaque ontologie dans O. Comme O infère O', alors I' satisfait à O', et donc I satisfait à T(O'). Donc T(K),T(V') infère dans OWL DL T(Q).

Supposons que T(O) infère dans OWL DL T(O'). Soit I', une interprétation directe qui satisfait à K. Alors, d'après le lemme 4, il existe une interprétation OWL DL I tel que, pour toute ontologie OWL abstraite X sur V', I satisfait à T(X) si et seulement si I' satisfait à X. Donc I satisfait à T(O). Comme T(O) infère dans OWL DL T(O'), alors I satisfait à T(O'), et donc I' satisfait à O'. Donc O infère O'.

A.2 La correspondance entre OWL DL et OWL Full

Ce chapitre contient une ébauche de démonstration concernant la relation entre OWL DL et OWL Full. Cette démonstration est incomplète, sa mise au point demandera peut-être beaucoup d'effort et certains détails de cette relation pourront changer.

Soit K un graphe RDF. Une interprétation OWL de K est une interprétation OWL (d'après le chapitre 5.2), c'est-à-dire une interprétation directe de K.

Lemme 5 : Soit V un vocabulaire séparé. Alors, pour chaque interprétation OWL I, il existe une interprétation OWL DL I' (d'après le chapitre 5.3) tel que, pour K une ontologie OWL dans la syntaxe abstraite avec un vocabulaire séparé V, I est une interprétation OWL de T(K) si et seulement si I' est une interprétation OWL DL de T(K).

Ébauche de démonstration : Comme toutes les interprétations OWL DL sont des interprétations OWL, la réciproque est évidente.

Soit I = < R_I, EXT_I, S_I, L_I > une interprétation OWL qui satisfait à T(K). Soit I' = < R_I', EXT_I', S_I', L_I' > une interprétation OWL qui satisfait à T(K). Soit R_I' = CEXT_I(I(owl:Thing)) + CEXT_I(I(owl:ObjectProperty)) + CEXT_I(I(owl:ObjectProperty)) + CEXT_I(I(owl:Class)) + CEXT_I(I(rdf:List)) + R_I, où + symbolise une union disjointe. Définissons EXT_I' afin de distinguer les divers rôles des copies. Définissons S_I' afin de relier un vocabulaire à la copie appropriée. Cette hypothèse se vérifie parce que K a un vocabulaire séparé, donc I peut être découpé selon les rôles, et il n'y a pas de relation erronnée dans EXT_I. Essentiellement, le premier composant de R_I' correspond aux individus OWL, le deuxième composant de R_I' aux propriétés de type de donnée OWL, le troisième composant aux propriétés à valeur d'individu OWL, le quatrième composant aux classes OWL, le cinquième composant aux listes RDF et le sixième composant à tout le reste.

Théorème 2 : Soit O et O' des ensembles d'ontologies, axiomes et faits OWL DL dans la forme de la syntaxe abstraite, clos aux importations, tel que leur union a un vocabulaire séparé (cf. le chapitre 4.2). Alors la traduction de O infère dans OWL Full la traduction de O', si la traduction de O infère dans OWL DL la traduction de O'.

Démonstration : D'après le lemme précédent et parce que toutes les interprétations OWL Full sont des interprétations OWL.

Remarque : La condition seulement si n'est pas vérifiée.