Direct Semantics

- This version:
- http://www.w3.org/TR/2008/WD-owl2-semantics-20081008/
- Latest version:
- http://www.w3.org/TR/owl2-semantics/
- Previous version:
- http://www.w3.org/TR/2008/WD-owl2-semantics-20080411/

- Editors:
- Boris Motik, Oxford University
- Peter F. Patel-Schneider, Bell Labs Research, Alcatel-Lucent
- Bernardo Cuenca Grau, Oxford University
- Contributors:
- Ian Horrocks, Oxford University
- Bijan Parsia, The University of Manchester
- Ulrike Sattler, The University of Manchester
*Note*: The complete list of contributors is being compiled and will be included in the next draft.

Copyright © 2008 W3C^{®} (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.

OWL 2 extends the W3C OWL Web Ontology Language
with a small but useful set of features that have been requested by
users, for which effective reasoning algorithms are now available,
and that OWL tool developers are willing to support. The new
features include extra syntactic sugar, additional property and
qualified cardinality constructors, extended datatype support,
simple metamodelling, and extended annotations.

This document provides the direct model-theoretic semantics for OWL 2, which is compatible with the description logic*SROIQ*.
Furthermore, this document defines the most common inference
problems for OWL 2.

This document provides the direct model-theoretic semantics for OWL 2, which is compatible with the description logic

*This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current W3C publications and the latest revision of this technical report can be found in the W3C technical reports index at http://www.w3.org/TR/.*

This document is being published as one of a set of 7 documents:

- Structural Specification and Functional-Style Syntax
- Direct Semantics (this document)
- RDF-Based Semantics
- Mapping to RDF Graphs
- XML Serialization
- Profiles
- Conformance and Test Cases

The OWL Working Group intends to make OWL 2 be a superset of OWL 1, except for a limited number of situations where we believe the impact will be minimal. This means that OWL 2 will be backward compatible, and creators of OWL 1 documents need only move to OWL 2 when they want to make use of OWL 2 features. More details and advice concerning migration from OWL 1 to OWL 2 will be in future drafts.

There are several major changes to this document since the version of 11 April 2008. A number of changes reflect the major revamping of the functional syntax to disallow punning between classes and datatypes and between object, data, and annotation properties. Semantics of Keys has been added. A set of inference problems has been defined. An extended discussion of datatypes has been added. Some minor changes were made to reflect changes in the Functional Syntax.

The OWL Working Group seeks public feedback on these Working Drafts. Please send your comments to public-owl-comments@w3.org (public archive). If possible, please offer specific changes to the text that would address your concern. You may also wish to check the Wiki Version of this document for internal-review comments and changes being drafted which may address your concerns.

*Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.*

*This document was produced by a group operating under the 5 February 2004 W3C Patent Policy. W3C maintains a public list of any patent disclosures made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) must disclose the information in accordance with section 6 of the W3C Patent Policy.*

## Contents |

This document defines the formal, model-theoretic semantics of
OWL 2. The semantics given here is strongly related to the
semantics of description logics [Description Logics]
and is compatible with the semantics of the description logic
*SROIQ* [SROIQ]. As the definition of *SROIQ* does not
provide for datatypes and punning, the semantics of OWL 2 is
defined directly on the constructs of the functional-style syntax
for OWL 2 [OWL 2
Specification] instead of by reference to the semantics
of SROIQ. For the constructs available in *SROIQ*, the
semantics of *SROIQ* trivially corresponds to the one defined
in this document.

Since OWL 2 is an extension of OWL DL, this document also provides a formal semantics for OWL Lite and OWL DL; this semantics is equivalent to the official semantics of OWL Lite and OWL DL [OWL Abstract Syntax and Semantics]. Furthermore, this document also provides the model-theoretic semantics for the OWL 2 profiles [OWL 2 Profiles].

The semantics is defined for a set of axioms, rather than for an ontology document in the functional-style syntax. Turning ontology documents into sets of axioms involves determining the axiom closure of an ontology (i.e., performing imports and renaming anonymous individuals apart) as described in the OWL 2 Specification [OWL 2 Specification]).

OWL 2 allows for annotations of ontologies, ontology entities (classes, properties, and individuals), anonymous individuals, axioms, and other annotations. Annotations of all these types, however, have no semantic meaning in OWL 2 and are ignored in this document. OWL 2 declarations are simply used to disambiguate class expressions from data ranges and object property from data property expressions in the functional-style syntax. Therefore, they are not mentioned explicitly in the tables in this document.

This section specifies the model-theoretic semantics of OWL 2 ontologies in the functional-style syntax.

Let *D* = ( *N _{DT}* ,

*V*is a set of_{C}*classes*as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the classes*owl:Thing*and*owl:Nothing*.*V*is a set of_{OP}*object properties*as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the object properties*owl:TopObjectProperty*and*owl:BottomObjectProperty*.*V*is a set of_{DP}*data properties*as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the data properties*owl:TopDataProperty*and*owl:BottomDataProperty*.*V*is a set of_{I}*individuals*(named and anonymous) as defined in the OWL 2 Specification [OWL 2 Specification].*V*is the set of all datatypes of_{DT}*D*extended with the datatype*rdfs:Literal*; that is,*V*=_{DT}*N*∪ {_{DT}*rdfs:Literal*}.*V*is a function that assigns to each datatype_{LT}*DT*∈*V*a set of literals_{DT}*V*, such that_{LT}(DT)*V*=_{LT}(DT)*N*for each datatype_{LT}(DT)*DT*∈*N*and_{DT}*V*= ∅._{LT}(rdfs:Literal)

*V*is the function assigning to each datatype_{FA}*DT*∈*V*a set_{DT}*V*of pairs of the form ⟨ f lt ⟩, where_{FA}(DT)*f*is a constraining facet and*lt*∈*V*, such that_{LT}*V*=_{FA}(DT)*N*for each datatype_{FA}(DT)*DT*∈*N*and_{DT}*V*= ∅._{FA}(rdfs:Literal)

Given a vocabulary *V*, the following conventions are used
in this document to denote different syntactic parts of OWL 2
ontologies:

- OP denotes an object property;
- OPE denotes an object property expression;
- DP denotes a data property;
- DPE denotes a data property expression;
- PE denotes an object property or a data property expression;
- C denotes a class;
- CE denotes a class expression;
- DT denotes a datatype;
- DR denotes a data range;
- a denotes an individual (named or anonymous);
- lt denotes a literal; and
- f denotes a constraining facet.

Given a datatype map *D* and a vocabulary *V* over
*D*, an *interpretation* *Int* = (
*Δ _{Int}* ,

*Δ*is a nonempty set called the_{Int}*object domain*.*Δ*is a nonempty set disjoint with_{D}*Δ*called the_{Int}*data domain*such that*(DT)*⊆^{DT}*Δ*for each datatype_{D}*DT*∈*V*._{DT}*⋅*is the^{C}*class interpretation*function that assigns to each class*C ∈ V*a subset_{C}*(C)*⊆^{C}*Δ*such that_{Int}*(owl:Thing)*=^{C}*Δ*and_{Int}*(owl:Nothing)*= ∅.^{C}

*⋅*is the^{OP}*object property interpretation*function that assigns to each object property*OP ∈ V*a subset_{OP}*(OP)*⊆^{OP}*Δ*×_{Int}*Δ*such that_{Int}*(owl:TopObjectProperty)*=^{OP}*Δ*×_{Int}*Δ*and_{Int}*(owl:BottomObjectProperty)*= ∅.^{OP}

*⋅*is the^{DP}*data property interpretation*function that assigns to each data property*DP ∈ V*a subset_{DP}*(DP)*⊆^{DP}*Δ*×_{Int}*Δ*such that_{D}*(owl:TopDataProperty)*=^{DP}*Δ*×_{Int}*Δ*and_{D}*(owl:BottomDataProperty)*= ∅.^{DP}

*⋅*is the^{I}*individual interpretation*function that assigns to each individual*a ∈ V*an element_{I}*(a)*∈^{I}*Δ*._{Int}*⋅*,^{DT}*⋅*, and^{LT}*⋅*are the same as in^{FA}*D*, and*(rdfs:Literal)*=^{DT}*Δ*._{D}

The following sections define the extensions of
*⋅ ^{OP}*,

The object property interpretation function
*⋅ ^{OP}* is extended to object property
expressions as shown in Table 1.

Object Property Expression | Interpretation ⋅ ^{OP} |
---|---|

InverseOf( OP ) | { ⟨ x , y ⟩ | ⟨ y , x ⟩ ∈
(OP) }^{OP} |

The datatype interpretation function *⋅ ^{DT}*
is extended to data ranges as shown in Table 3. Note that datatypes
in OWL 2 are all unary; thus, each datatype

Editor's Note:
OWL WG ISSUE-127 is
related to n-ary data ranges and might impact this section.

Data Range | Interpretation ⋅ ^{DT} |
---|---|

OneOf( lt_{1} ... lt_{n} ) |
{ (lt , ... ,
_{1})^{LT}(lt }_{n})^{LT} |

ComplementOf( DR ) | (Δ \ _{D})^{n}(DR)
where ^{DT}n is the arity of DR |

DatatypeRestriction( DT f_{1}
lt_{1} ... f_{n} lt_{n} ) |
(DT) ∩ ^{DT}(⟨ f ∩ ... ∩ _{1} lt_{1}
⟩)^{FA}(⟨ f_{n} lt_{n}
⟩)^{FA} |

The class interpretation function *⋅ ^{C}* is
extended to class expressions as shown in Table 4. For

Class Expression | Interpretation ⋅ ^{C} |
---|---|

IntersectionOf( CE_{1} ... CE_{n}
) |
(CE ∩ ... ∩
_{1})^{C}(CE_{n})^{C} |

UnionOf( CE_{1} ... CE_{n} ) |
(CE ∪ ... ∪
_{1})^{C}(CE_{n})^{C} |

ComplementOf( CE ) | Δ \ _{Int}(CE)^{C} |

OneOf( a_{1} ... a_{n} ) |
{ (a , ... ,
_{1})^{I}(a }_{n})^{I} |

SomeValuesFrom( OPE CE ) | { x | ∃ y : ⟨ x, y ⟩ ∈
(OPE) and ^{OP}y ∈ (CE)
}^{C} |

AllValuesFrom( OPE CE ) | { x | ∀ y : ⟨ x, y ⟩ ∈
(OPE) implies ^{OP}y ∈
(CE) }^{C} |

HasValue( OPE a ) | { x | ⟨ x , (a) ⟩ ∈
^{I}(OPE) }^{OP} |

ExistsSelf( OPE ) | { x | ⟨ x , x ⟩ ∈
(OPE) }^{OP} |

MinCardinality( n OPE ) | { x | #{ y | ⟨ x , y ⟩ ∈
(OPE) } ≥ n }^{OP} |

MaxCardinality( n OPE ) | { x | #{ y | ⟨ x , y ⟩ ∈
(OPE) } ≤ n }^{OP} |

ExactCardinality( n OPE ) | { x | #{ y | ⟨ x , y ⟩ ∈
(OPE) } = n }^{OP} |

MinCardinality( n OPE CE ) | { x | #{ y | ⟨ x , y ⟩ ∈
(OPE) and ^{OP}y ∈ (CE) }
≥ n }^{C} |

MaxCardinality( n OPE CE ) | { x | #{ y | ⟨ x , y ⟩ ∈
(OPE) and ^{OP}y ∈ (CE) }
≤ n }^{C} |

ExactCardinality( n OPE CE ) | { x | #{ y | ⟨ x , y ⟩ ∈
(OPE) and ^{OP}y ∈ (CE) }
= n }^{C} |

SomeValuesFrom( DPE_{1} ...
DPE_{n} DR ) |
{ x | ∃ y, ... ,
_{1}y : ⟨ _{n}x , y ⟩ ∈
_{k}(DPE for each 1 ≤ _{k})^{DP}k ≤
n and ⟨ y , ... , _{1}y ⟩
∈ _{n}(DR) }^{DT} |

AllValuesFrom( DPE_{1} ... DPE_{n}
DR ) |
{ x | ∀ y, ... ,
_{1}y : ⟨ _{n}x , y ⟩ ∈
_{k}(DPE for each 1 ≤ _{k})^{DP}k ≤
n imply ⟨ y , ... , _{1}y
⟩ ∈ _{n}(DR) }^{DT} |

HasValue( DPE lt ) | { x | ⟨ x , (lt) ⟩ ∈
^{LT}(DPE) }^{DP} |

MinCardinality( n DPE ) | { x | #{ y | ⟨ x , y ⟩ ∈
(DPE)} ≥ n }^{DP} |

MaxCardinality( n DPE ) | { x | #{ y | ⟨ x , y ⟩ ∈
(DPE) } ≤ n }^{DP} |

ExactCardinality( n DPE ) | { x | #{ y | ⟨ x , y ⟩ ∈
(DPE) } = n }^{DP} |

MinCardinality( n DPE DR ) | { x | #{ y | ⟨ x , y ⟩ ∈
(DPE) and ^{DP}y ∈ (DR) }
≥ n }^{DT} |

MaxCardinality( n DPE DR ) | { x | #{ y | ⟨ x , y ⟩ ∈
(DPE) and ^{DP}y ∈ (DR) }
≤ n }^{DT} |

ExactCardinality( n DPE DR ) | { x | #{ y | ⟨ x , y ⟩ ∈
(DPE) and ^{DP}y ∈ (DR) }
= n }^{DT} |

An interpretation *Int* = ( *Δ _{Int}* ,

*ISNAMED _{O}(x)* =

Satisfaction of OWL 2 class expression axioms in *Int*
w.r.t. *O* is defined as shown in Table 5.

Axiom | Condition |
---|---|

SubClassOf( CE_{1} CE_{2} ) |
(CE ⊆
_{1})^{C}(CE_{2})^{C} |

EquivalentClasses( CE_{1} ...
CE_{n} ) |
(CE =
_{j})^{C}(CE for each 1 ≤ _{k})^{C}j ≤
n and each 1 ≤ k ≤ n |

DisjointClasses( CE_{1} ... CE_{n}
) |
(CE ∩
_{j})^{C}(CE = ∅ for each 1 ≤ _{k})^{C}j ≤
n and each 1 ≤ k ≤ n such that j ≠
k |

DisjointUnion( C CE_{1} ... CE_{n}
) |
(C) = ^{C}(CE ∪
... ∪ _{1})^{C}(CE and_{n})^{C}(CE ∩
_{j})^{C}(CE = ∅ for each 1 ≤ _{k})^{C}j ≤
n and each 1 ≤ k ≤ n such that j ≠
k |

Satisfaction of OWL 2 object property expression axioms in
*Int* w.r.t. *O* is defined as shown in Table 6.

Axiom | Condition |
---|---|

SubPropertyOf( OPE_{1} OPE_{2}
) |
(OPE ⊆
_{1})^{OP}(OPE_{2})^{OP} |

SubPropertyOf( PropertyChain( OPE_{1} ...
OPE_{n} ) OPE ) |
∀ y , ... , _{0}y : ⟨
_{n}y , _{0}y ⟩ ∈
_{1}(OPE and ... and ⟨
_{1})^{OP}y , _{n-1}y ⟩ ∈
_{n}(OPE imply ⟨ _{n})^{OP}y
, _{0}y ⟩ ∈ _{n}(OPE)^{OP} |

EquivalentProperties( OPE_{1} ...
OPE_{n} ) |
(OPE =
_{j})^{OP}(OPE for each 1 ≤ _{k})^{OP}j ≤
n and each 1 ≤ k ≤ n |

DisjointProperties( OPE_{1} ...
OPE_{n} ) |
(OPE ∩
_{j})^{OP}(OPE = ∅ for each 1 ≤ _{k})^{OP}j ≤
n and each 1 ≤ k ≤ n such that j ≠
k |

PropertyDomain( OPE CE ) | ∀ x , y : ⟨ x , y ⟩ ∈
(OPE) implies ^{OP}x ∈
(CE)^{C} |

PropertyRange( OPE CE ) | ∀ x , y : ⟨ x , y ⟩ ∈
(OPE) implies ^{OP}y ∈
(CE)^{C} |

InverseProperties( OPE_{1} OPE_{2}
) |
(OPE = { ⟨ _{1})^{OP}x , y
⟩ | ⟨ y , x ⟩ ∈ (OPE
}_{2})^{OP} |

FunctionalProperty( OPE ) | ∀ x , y , _{1}y :
⟨ _{2}x , y ⟩ ∈ _{1}(OPE) and
⟨ ^{OP}x , y ⟩ ∈ _{2}(OPE)
imply ^{OP}y = _{1}y_{2} |

InverseFunctionalProperty( OPE ) | ∀ x , _{1}x , _{2}y :
⟨ x , _{1}y ⟩ ∈ (OPE) and
⟨ ^{OP}x , _{2}y ⟩ ∈ (OPE)
imply ^{OP}x = _{1}x_{2} |

ReflexiveProperty( OPE ) | ∀ x : x ∈ Δ implies ⟨
_{Int}x , x ⟩ ∈ (OPE)^{OP} |

IrreflexiveProperty( OPE ) | ∀ x : x ∈ Δ implies ⟨
_{Int}x , x ⟩ ∉ (OPE)^{OP} |

SymmetricProperty( OPE ) | ∀ x , y : ⟨ x , y ⟩ ∈
(OPE) implies ⟨ ^{OP}y , x ⟩ ∈
(OPE)^{OP} |

AsymmetricProperty( OPE ) | ∀ x , y : ⟨ x , y ⟩ ∈
(OPE) implies ⟨ ^{OP}y , x ⟩ ∉
(OPE)^{OP} |

TransitiveProperty( OPE ) | ∀ x , y , z : ⟨ x , y ⟩
∈ (OPE) and ⟨ ^{OP}y , z ⟩ ∈
(OPE) imply ⟨ ^{OP}x , z ⟩ ∈
(OPE)^{OP} |

Satisfaction of OWL 2 data property expression axioms in
*Int* w.r.t. *O* is defined as shown in Table 7.

Axiom | Condition |
---|---|

SubPropertyOf( DPE_{1} DPE_{2}
) |
(DPE ⊆
_{1})^{DP}(DPE_{2})^{DP} |

EquivalentProperties( DPE_{1} ...
DPE_{n} ) |
(DPE =
_{j})^{DP}(DPE for each 1 ≤ _{k})^{DP}j ≤
n and each 1 ≤ k ≤ n |

DisjointProperties( DPE_{1} ...
DPE_{n} ) |
(DPE ∩
_{j})^{DP}(DPE = ∅ for each 1 ≤ _{k})^{DP}j ≤
n and each 1 ≤ k ≤ n such that j ≠
k |

PropertyDomain( DPE CE ) | ∀ x , y : ⟨ x , y ⟩ ∈
(DPE) implies ^{DP}x ∈
(CE)^{C} |

PropertyRange( DPE DR ) | ∀ x , y : ⟨ x , y ⟩ ∈
(DPE) implies ^{DP}y ∈
(DR)^{DT} |

FunctionalProperty( DPE ) | ∀ x , y , _{1}y :
⟨ _{2}x , y ⟩ ∈ _{1}(DPE) and
⟨ ^{DP}x , y ⟩ ∈ _{2}(DPE)
imply ^{DP}y = _{1}y_{2} |

Satisfaction of keys in *Int* w.r.t. *O* is defined as
shown in Table 8.

Axiom | Condition |
---|---|

HasKey( CE PE_{1} ... PE_{n}
) |
∀ x , y ,
z , ... , _{1}z :_{n}if ISNAMED and
_{O}(x)ISNAMED and
_{O}(y)ISNAMED and ... and
_{O}(z_{1})ISNAMED and _{O}(z_{n})x ∈
(CE) and ^{C}y ∈ (CE)
and^{C}for each 1 ≤ i ≤
n,if PE is an object property, then ⟨ _{i}x ,
z ⟩ ∈ _{i}(PE and ⟨
_{i})^{OP}y , z ⟩ ∈
_{i}(PE, and_{i})^{OP}if PE is a data property, then ⟨ _{i}x ,
z ⟩ ∈ _{i}(PE and ⟨
_{i})^{DP}y , z ⟩ ∈
_{i}(PE_{i})^{DP}then x = y |

Satisfaction of OWL 2 assertions in *Int* w.r.t. *O*
is defined as shown in Table 9.

Axiom | Condition |
---|---|

SameIndividual( a_{1} ... a_{n}
) |
(a =
_{j})^{I}(a for each 1 ≤ _{k})^{I}j ≤ n
and each 1 ≤ k ≤ n |

DifferentIndividuals( a_{1} ...
a_{n} ) |
(a ≠
_{j})^{I}(a for each 1 ≤ _{k})^{I}j ≤ n
and each 1 ≤ k ≤ n such that j ≠ k |

ClassAssertion( CE a ) | (a) ∈ ^{I}(CE)^{C} |

PropertyAssertion( OPE a_{1} a_{2}
) |
⟨ (a ,
_{1})^{I}(a ⟩ ∈
_{2})^{I}(OPE)^{OP} |

NegativePropertyAssertion( OPE a_{1}
a_{2} ) |
⟨ (a ,
_{1})^{I}(a ⟩ ∉
_{2})^{I}(OPE)^{OP} |

PropertyAssertion( DPE a lt ) | ⟨ (a) , ^{I}(lt) ⟩ ∈
^{LT}(DPE)^{DP} |

NegativePropertyAssertion( DPE a lt ) | ⟨ (a) , ^{I}(lt) ⟩ ∉
^{LT}(DPE)^{DP} |

*Int* *satisfies* an OWL 2 ontology *O* if all
axioms in the axiom closure of *O* (with anonymous individuals
renamed apart as described in Section 5.6.2 of the OWL 2
Specification [OWL 2 Specification]) are satisfied in *Int*
w.r.t. *O*.

An interpretation *Int* = ( *Δ _{Int}* ,

Thus, an interpretation *Int* satisfying *O* is also a
model of *O*. In contrast, a model *Int* of *O* may
not satisfy *O* directly; however, by modifying the
interpretation of anonymous individuals, *Int* can always be
coerced into an interpretation *Int'* that satisfies
*O*.

Let *D* be a datatype map and *V* a vocabulary over
*D*. Furthermore, let *O* and *O'* be OWL 2
ontologies, *CE*, *CE _{1}*, and

The following inference problems are often considered in practice.

**Ontology Consistency**: *O* is *consistent* (or
*satisfiable') w.r.t.* D *if a model of* O *w.r.t.*
D *and* V *exists.*

**Ontology Entailment**: *O* *entails* *O'*
w.r.t. *D* if every model of *O* w.r.t. *D* and
*V* is also a model of *O'* w.r.t. *D* and
*V*.

**Ontology Equivalence**: *O* and *O'* are
*equivalent* w.r.t. *D* if *O* entails *O'*
w.r.t. *D* and *O'* entails *O* w.r.t. *D*.

**Ontology Equisatisfiability**: *O* and *O'* are
*equisatisfiable* w.r.t. *D* if *O* is satisfiable
w.r.t. *D* if and only if *O'* is satisfiable w.r.t
*D*.

**Class Expression Satisfiability**: *CE* is satisfiable
w.r.t. *O* and *D* if a model *Int* = (
*Δ _{Int}* ,

**Class Expression Subsumption**: *CE _{1}* is

**Instance Checking**: *a* is an *instance* of
*CE* w.r.t. *O* and *D* if *(a) ^{I}* ∈

**Boolean Conjunctive Query Answering**: *Q* is an
*answer* w.r.t. *O* and *D* if *Q* is true in
each model of *O* w.r.t. *D* and *V*.

The semantics of OWL 2 has been defined in such a way that the
semantics of an OWL 2 ontology *O* does not depend on the
choice of a datatype map, as long as the datatype map chosen
contains all the datatypes occurring in *O*. This statement is
made precise by the following theorem, which has several useful
consequences:

- One can interpret an OWL 2 ontology
*O*by considering only the datatypes explicitly occurring in*O*. - When referring to various reasoning problems, the datatype map
*D*need not be given explicitly, as it is sufficient to consider the datatype map implicitly defined by the ontology in question. - OWL 2 reasoners can provide datatypes not explicitly mentioned in this specification without fear that this will change the semantics of OWL 2 ontologies not using these datatypes.

**Theorem 1.** Let *O _{1}* and

*Proof.* Without loss of generality, one can assume
*O _{1}* and

*Δ*is obtained by extending_{D}'*Δ*with the value space of all datatypes in_{D}*N*\_{DT}'*N*,_{DT}*⋅*coincides with^{C '}*⋅*on all classes, and^{C}*⋅*coincides with^{DP '}*⋅*on all data properties apart from^{DP}*owl:TopDataProperty*.

Clearly, *ComplementOf( DR
) ^{DT}* ⊆

- [Description Logics]
- The Description Logic Handbook. Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, Peter Patel-Schneider, Editors. Cambridge University Press, 2003; and Description Logics Home Page.
- [OWL 2 Specification]
- OWL 2 Web Ontology Language:Structural Specification and Functional-Style Syntax Boris Motik, Peter F. Patel-Schneider, Bijan Parsia, eds. W3C Working Draft, 08 October 2008, http://www.w3.org/TR/2008/WD-owl2-syntax-20081008/. Latest version available at http://www.w3.org/TR/owl2-syntax/.
- [OWL 2 Profiles]
- OWL 2 Web Ontology Language:Structural Specification and Functional-Style Syntax Boris Motik, Peter F. Patel-Schneider, Bijan Parsia, eds. W3C Working Draft, 08 October 2008, http://www.w3.org/TR/2008/WD-owl2-syntax-20081008/. Latest version available at http://www.w3.org/TR/owl2-syntax/.
- [OWL Abstract Syntax and Semantics]
- OWL Web Ontology Language: Semantics and Abstract Syntax. Peter F. Patel-Schneider, Pat Hayes, and Ian Horrocks, Editors, W3C Recommendation, 10 February 2004.
- [SROIQ]
- The Even More Irresistible SROIQ. Ian Horrocks, Oliver Kutz, and Uli Sattler. In Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2006). AAAI Press, 2006.
- [RFC-4646]
- RFC 4646 - Tags for Identifying Languages. M. Phillips and A. Davis. IETF, September 2006, http://www.ietf.org/rfc/rfc4646.txt. Latest version is available as BCP 47, (details).