Lisez-moi S.V.P. 

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.


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 :

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 = <RI,PI,EXTI,SI,LI,LVI> une interprétation OWL DL de V qui satisfait à T(V'), avec LVI = LV. Soit CEXTI avec sa signification habituelle, et surchargeant comme toujours I pour relier une structure syntaxique à sa dénotation. Si :

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

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

Démonstration :

On réalise la démonstration du lemme par induction structurelle. Pour la démonstration, on a IOT = CEXTI(I(owl:Thing)), IOC = CEXTI(I(owl:Class)), IDC = CEXTI(I(rdfs:Datatype)), IOOP = CEXTI(I(owl:ObjectProperty)), IODP = - CEXTI(I(owl:DatatypeProperty)) et IL = CEXTI(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)>∈EXTI(I(rdfs:domain)) et <p,I(owl:Thing)>∈EXTI(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)∈CEXTI(I(owl:Class)). Comme I est une interprétation OWL DL, CEXTI(I(v))⊆IOT, de sorte que <I(v),I(owl:Thing)>∈EXTI(I(rdfs:subClassOf)). Donc I OWL DL satisfait à T(v). Puisque M(T(v)) est v, alors CEXTI(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)∈CEXTI(I(rdfs:Datatype)). Comme I est une interprétation OWL DL, CEXTI(I(v))⊆LVI, de sorte que <I(v),I(rdfs:Literal)>∈EXTI(I(rdfs:subClassOf)). Donc I compatible RDF satisfait à T(v). Puisque M(T(v)) est v, alors CEXTI(I(M(T(v))))=EC(v). D'où finalement I(v)∈IDC.
Hypothèse de base : d=oneOf(i1…in), où les ij sont des identificateurs d'individus
Comme ij∈VI pour 1 ≤ j ≤ n et que I satisfait à T(V), alors I(ij)∈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(i1),…,I(in) sur IOT. Pour tout l, qui est une suite I(i1),…,I(in) sur IOT, le principe de compréhension de owl:oneOf impose l'existence d'un y∈CEXTI(I(rdfs:Class)) tel que <y,l> ∈ EXTI(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), CEXTI(I+A(M(T(d)))) = {I(i1),…,I(in)} = EC(d). Finalement, I+A(M(T(d)))∈IOC.
Hypothèse de base : d=oneOf(v1…vn), où vi est un littéral de donnée
Puisque I(vj)∈LVI, le deuxième principe de compréhension des suites impose donc qu'il existe un l∈IL qui soit une suite I(v1),…,I(vn) sur LVI. Pour tout L, qui est une suite I(v1),…,I(vn) sur LVI, le principe de compréhension de owl:oneOf impose l'existence d'un y∈CEXTI(I(rdfs:Class)) tel que <y,l> ∈ EXTI(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), CEXTI(I+A(M(T(d)))) = {I(i1),…,I(in)} = 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), CEXTI(I+A(M(T(d)))) = {x∈IOT | <x,I(i)> ∈ EXTI(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>∈EXTI(I(owl:complementOf)), donc I satisfait à T(d). Pour tout I+A qui satisfait à T(d), CEXTI(I+A(M(T(d)))) = IOT-CEXTI(I+A(M(T(d)))) = R-EC(d') = EC(d). Finalement, I+A(M(T(d)))∈IOC.
Hypothèse inductive : d = unionOf(d1 … dn)
D'après l'hypothèse inductive, I satisfait à di, pour 1 ≤ i ≤ n, de sorte qu'il existe un Ai qui relie tous les nœuds blancs dans T(di) aux éléments du domaine tel que I+Ai satisfait T(di). Comme les nœuds blancs dans T(di) sont disjoints des nœuds blancs de T(dj), pour i≠j, I+A1+…+An et donc I satisfait à T(di)∪…∪T(dn). Chaque di est une description, donc, d'après l'hypothèse inductive, I+A1+…+An(M(T(di)))∈IOC. Le premier principe de compréhension des suites impose alors l'existence d'un l∈IL qui soit une suite I+A1+…+An(M(T(d1))),…,I+A1+…+An(M(T(dn))) sur IOC. Le principe de compréhension de owl:unionOf impose alors l'existence d'un y∈IOC tel que <y,l>∈EXTI(I(owl:unionOf)), ainsi I satisfait à T(d).
Pour tout I+A qui satisfait à T(d), I+A satisfait à T(di), donc CEXTI(I+A(di)) = EC(di)). Et ensuite CEXTI(I+A(M(T(d)))) = CEXTI(I+A(d1))∪…∪CEXTI(I+A(dn)) = EC(d1)∪…∪EC(dn) = EC(d). Finalement, I(M(T(d)))∈IOC.
Hypothèse inductive : d = intersectionOf(d1 … dn)
Similaire.
Hypothèse inductive : d = restriction(p x1 x2 … xn)
Puisque p∈VOP∪VDP, de précédemment I satisfait à T(p). D'après l'hypothèse inductive, I satisfait à restriction(p xi) pour 1 ≤ i ≤ n, de sorte qu'il existe un Ai reliant tous les nœuds blancs dans T(restriction(p xi)) aux éléments du domaine, tel que I+Ai satisfait à T(restriction(p xi)). Comme les nœuds blancs dans T(restriction(p xi)) sont disjoints de ceux de T(restriction(p xj)), pour i≠j, I+A1+…+An, et donc I satisfait à T(restriction(p x1 … xn)). Chaque restriction(p xi) étant une description, donc d'après l'hypothèse inductive M(T(restriction(p xi)))∈IOC. Le premier principe de compréhension des listes impose alors l'existence d'un l∈IL qui soit une suite I+A1+…+An(M(T(restriction(p xi)))),…,I+A1+…+An(M(T(restriction(p xi)))) sur IOC. Le principe de compréhension de owl:intersectionOf impose alors l'existence d'un y∈IOC tel que <y,l>∈EXTI(I(owl:intersectionOf)), et donc I satisfait à T(d).
Pour tout I+A qui satisfait à T(d), I+A satisfait à T(di), et donc CEXTI(I+A(di)) = EC(di)). Ensuite CEXTI(I+A(M(T(d)))) = CEXTI(I+A(restriction(p xi)))∩…∩ CEXTI(I+A(restriction(p xn))) = EC(restriction(p xi))cap;…∩EC(restriction(p xi)) = 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), CEXTI(I+A(M(T(d)))) = {x∈IOT | ∀ y∈IOT : <x,y>∈EXTI(p) implique que y∈CEXTI(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 RI, 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 RI 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 RI, 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 d1 … dn)

Soit d=intersectionOf(d1 … dn). 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), CEXTI(I+A(M(T(d)))) = EC(d). Ainsi, pour toute sous-description d' de d, CEXTI(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), CEXTI(I+A(M(T(d)))) = EC(d) et I+A(M(T(d)))∈IOC, et pour chaque sous-description d' de d, on a CEXTI(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 CEXTI(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXTI(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)))> ∈ EXTI(I(owl:equivalentClass)). En outre, à cause des conditions sémantiques sur I(owl:intersectionOf), on a <I(foo),I+A(M(T(SEQ d1 … dn)))> ∈ EXTI(I(owl:intersectionOf)).

Si d est de la forme intersectionOf(d1), alors CEXTI(I+A(M(T(d1)))) = EC(d1) = EC(d) = EC(foo) et I+A(M(T(d1)))∈IOC. Ainsi, d'après les conditions sémantiques sur I(owl:equivalentClass), <I(foo),I+A(M(T(d1)))> ∈ EXTI(I(owl:equivalentClass)). Si d1 est de la forme complementOf(d'1), alors IOT - CEXTI(I+A(M(T(d'1)))) = CEXTI(I+A(M(T(d1)))) = EC(d1) = EC(d) = EC(foo) et I+A(M(T(d'1)))∈IOC. Ainsi, d'après les conditions sémantiques sur I(owl:complementOf), <I(foo),I+A(M(T(d'1)))> ∈ EXTI(I(owl:complementOf)). Si d1 est de la forme unionOf(d11 … d1m), alors CEXTI(I+A(M(T(d11)))) ∪ … ∪ CEXTI(I+A(M(T(d1m)))) = CEXTI(I+A(M(T(d1)))) = EC(d1) = EC(d) = EC(foo) et I+A(M(T(d1j)))∈IOC, pour 1 ≤ j ≤ m. Ainsi, d'après les conditions sémantiques sur I(owl:unionOf), <I(foo),I+A(M(T(SEQ d11 … d1m)))> ∈ EXTI(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(d1 … dn)). Comme précédemment, il existe donc une certaine application A tel que <I(foo),I+A(M(T(d)))> ∈ EXTI(I(owl:equivalentClass)). Ainsi EC(d) = CEXTI(I+A(M(T(d)))) = CEXTI(I(foo)) = EC(foo). Par conséquent I' satisfait à F.

Hypothèse : F = Class(foo partial d1 … dn)

Soit d=intersectionOf(d1 … dn). 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 CEXTI(I+A(M(T(d)))) = EC(d). Ainsi, CEXTI(I+A(M(T(di)))) = EC(di), 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 CEXTI(I+A(M(T(di)))) = EC(di) et I+A(M(T(di))∈IOC, pour 1 ≤ i ≤ n.

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

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

Hypothèse : F = EnumeratedClass(foo i1 … in)

Soit d=oneOf(i1 … in). 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) = CEXTI(I+A(M(T(d)))) = {SI(M(T(i1)), … SI(M(T(in))}. On a également SI(M(T(ij)) ∈ 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 CEXTI(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXTI(I(foo)) et I+A(M(T(d))∈IOC. Soit e, I+A(M(T(SEQ i1 … in))). Alors, d'après les conditions sémantiques sur I(owl:oneOf), on a <I(foo),e> ∈ EXTI(I(owl:oneOf)). Par conséquent, I satisfait à T(F).

Si I satisfait à T(F), alors I satisfait à T(SEQ i1 … in). Ainsi, il existe une application A, comme précédemment, tel que <I(foo),I+A(M(T(SEQ i1 … in)))> ∈ EXTI(I(owl:oneOf)). Ainsi, {SI(M(T(i1)), …, SI(M(T(in))} = CEXTI(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(d1 … dn)

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

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

Si I' satisfait à F, alors EC(di)∩EC(dj) = {}, pour i ≠ j. Pour toute application Ai et Aj, comme précédemment, on a <I+Ai+Aj(M(T(di))),I+Ai+Aj(M(T(dj)))> ∈ EXTI(I(owl:disjointWith)), pour i ≠ j. Comme il existe au moins une application Ai pour chaque i et que les nœuds blancs de T(dj) sont tous disjoints, alors I+A1+…+An satisfait à T(DisjointClasses(d1 … dn)). Par conséquent, I satisfait à T(F).

Hypothèse : F = EquivalentClasses(d1 … dn)
Similaire.
Hypothèse : F = SubClassOf(d1 d2)
Similaire dans une certaine mesure.
Hypothèse : F = ObjectProperty(p super(s1) … super(sn) domain(d1) … domain(dm) range(r1) … range(rk) [inverse(i)] [Symmetric] [Functional] [InverseFunctional] [OneToOne] [Transitive])

Puisque di, pour 1 ≤ i ≤ m est une description sur V', alors I satisfait à T(di) et, pour toute application A reliant les nœuds blancs de T(di) tel que I+A satisfait à T(di), on a CEXTI(I+A(M(T(di)))) = EC(di). De même pour ri, 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)>∈EXTI(I(rdfs:domain)) et à <I(p),I(owl:Thing)>∈EXTI(I(rdfs:range)). Également, ER(p)⊆ER(si), pour 1 ≤ i ≤ n, de sorte que EXTI(I(p))=ER(p) ⊆ ER(si)=EXTI(I(si)) et que I satisfait à <I(p),I(si)>∈EXTI(I(rdfs:subPropertyOf)). Alors, ER(p)⊆EC(di)×R, pour 1 ≤ i ≤ m, de sorte que <z,w>∈ER(p) implique z∈EC(di) et que, pour toute application A tel que I+A satisfait à T(di), <z,w>∈EXTI(p) implique z∈CEXTI(I+A(M(T(di)))), et donc <I(p),I+A(M(T(di)))>∈EXTI(I(rdfs:domain)). De même pour ri, 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>∈EXTI(p) si et seulement si <v,u>∈EXTI(i) et I satisfait à <I(p),I(i)>∈EXTI(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> ∈ EXTI(p), alors <y, x>∈EXTI(p). Et donc I satisfait à p∈CEXTI(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(si)>∈EXTI(I(rdfs:subPropertyOf)), de sorte que ER(p)=EXTI(I(p)) ⊆ EXTI(I(si))=ER(si). Également, pour 1 ≤ i ≤ m, pour une application A tel que I+A satisfait à T(di), <I(p),I+A(M(T(di)))>∈EXTI(I(rdfs:domain)), de sorte que <z,w>∈EXTI(p) implique z∈CEXTI(I+A(M(T(di)))). Par conséquent, <z,w>∈ER(p) implique z∈EC(di) et ER(p)⊆EC(di)×R. De même pour ri, pour 1 ≤ i ≤ k.

Si I satisfait à T(F) et inverse(i) est dans F, alors I satisfait à <I(p),I(i)>∈EXTI(I(owl:inverseOf)). Ainsi, on a <u,v>∈EXTI(p) si et seulement si <v,u>∈EXTI(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∈CEXTI(I(owl:Symmetric)), de sorte que si <x,y> ∈ EXTI(p), alors <y, x>∈EXTI(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(s1) … super(sn) domain(d1) … domain(dm) range(r1) … range(rl) [Functional])
Similaire, mais plus simple.
Hypothèse : F = AnnotationProperty(p domain(d1) … domain(dm))
Similaire, mais encore plus simple.
Hypothèse : F = OntologyProperty(p domain(d1) … domain(dm))
Similaire, mais encore plus simple.
Hypothèse : F = EquivalentProperties(p1 … pn), pour pi∈VOP

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

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

Hypothèse : F = SubPropertyOf(p1 p2)
Un peu similaire, mais plus simple.
Hypothèse : F = SameIndividual(i1 … in)
Similaire à SamePropertyAs.
Hypothèse : F = DifferentIndividuals(i1 … in)
Similaire à SamePropertyAs.
Hypothèse : F = Individual([i] type(t1) … type(tn) value(p1 v1) … value(pn vn))

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 = <RI,PI,EXTI,SI,LI,LVI> 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 CEXTI défini normalement d'après I. L'interprétation directe obligatoire sera I' = < RI, EC, ER, L, S, LVI >, où :

  1. EC(v) = CEXTI(SI(v)), pour v∈VC∪VD
  2. ER(v) = EXTI(SI(v)), pour v∈VOP∪VDP∪VAP∪VXP
  3. < x, S(owl:DeprecatedClass) > ∈ ER(rdf:type) si et seulement si < x, SI(owl:DeprecatedClass) > EXTI(SI(rdf:type)), pour x ∈ R
  4. < x, S(owl:DeprecatedProperty) > ∈ ER(rdf:type) si et seulement si < x, SI(owl:DeprecatedProperty) > EXTI(SI(rdf:type)), pour x ∈ R
  5. L(d) = LI(d), pour d un littéral typé
  6. S(v) = SI(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 = < RI, PI, EXTI, SI, L, LVI > comme suit :

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 = < RI, EXTI, SI, LI > une interprétation OWL qui satisfait à T(K). Soit I' = < RI', EXTI', SI', LI' > une interprétation OWL qui satisfait à T(K). Soit RI' = CEXTI(I(owl:Thing)) + CEXTI(I(owl:ObjectProperty)) + CEXTI(I(owl:ObjectProperty)) + CEXTI(I(owl:Class)) + CEXTI(I(rdf:List)) + RI, où + symbolise une union disjointe. Définissons EXTI' afin de distinguer les divers rôles des copies. Définissons SI' 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 EXTI. Essentiellement, le premier composant de RI' correspond aux individus OWL, le deuxième composant de RI' 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.