This document is also available in these non-normative formats: PDF version.
Copyright © 2009 W3C^{®} (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.
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 Last Call Working Draft has a few changes since the previous version of 02 December 2008.
The Working Group believes it has completed its design work for the technologies specified this document, so this is a "Last Call" draft. The design is not expected to change significantly, going forward, and now is the key time for external review, before the implementation phase. (This is the second Last Call draft of this document. The public response to the previous Last Call prompted the Working Group to make material changes to the design.)
The OWL Working Group seeks public feedback on this Working Draft. 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 and see if the relevant text has already been updated.
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.
Table of Contents |
This document defines the direct model-theoretic semantics of OWL 2. The semantics given here is strongly related to the semantics of description logics [Description Logics] and it extends 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 structural specification of OWL 2 [OWL 2 Specification] instead of by reference to SROIQ. For the constructs available in SROIQ, the semantics of SROIQ trivially corresponds to the one defined in this document.
Since each OWL 1 DL ontology is an OWL 2 ontology, this document also provides a direct semantics for OWL 1 Lite and OWL 1 DL ontologies; this semantics is equivalent to the direct model-theoretic semantics of OWL 1 Lite and OWL 1 DL [OWL Abstract Syntax and Semantics]. Furthermore, this document also provides the direct model-theoretic semantics for the OWL 2 profiles [OWL 2 Profiles].
The semantics is defined for OWL 2 axioms and ontologies, which should be understood as instances of the structural specification [OWL 2 Specification]. Parts of the structural specification are written in this document using the functional-style syntax.
OWL 2 allows ontologies, anonymous individuals, and axioms to be annotated; furthermore, annotations themselves can contain additional annotations. All these types of annotations, however, have no semantic meaning in OWL 2 and are ignored in this document. OWL 2 declarations are used only 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 this document.
This section specifies the direct model-theoretic semantics of OWL 2 ontologies.
A datatype map, formalizing datatype maps from the OWL 2 Specification [OWL 2 Specification], is a 6-tuple D = ( N_{DT} , N_{LS} , N_{FS} , ⋅ ^{DT} , ⋅ ^{LS} , ⋅ ^{FS} ) with the following components:
A vocabulary V = ( V_{C} , V_{OP} , V_{DP} , V_{I} , V_{DT} , V_{LT} , V_{FA} ) over a datatype map D is a 7-tuple consisting of the following elements:
Given a vocabulary V, the following conventions are used in this document to denote different syntactic parts of OWL 2 ontologies:
Given a datatype map D and a vocabulary V over D, an interpretation I = ( Δ_{I} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{I} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) for D and V is a 9-tuple with the following structure:
The following sections define the extensions of ⋅ ^{OP}, ⋅ ^{DT}, and ⋅ ^{C} to object property expressions, data ranges, and class expressions.
The object property interpretation function ⋅ ^{OP} is extended to object property expressions as shown in Table 1.
Object Property Expression | Interpretation ⋅ ^{OP} |
---|---|
ObjectInverseOf( OP ) | { ⟨ x , y ⟩ | ⟨ y , x ⟩ ∈ (OP)^{OP} } |
The datatype interpretation function ⋅ ^{DT} is extended to data ranges as shown in Table 3. All datatypes in OWL 2 are unary, so each datatype DT is interpreted as a unary relation over Δ_{D} — that is, as a set (DT)^{DT} ⊆ Δ_{D}. OWL 2 currently does not define data ranges of arity more than one; however, by allowing for n-ary data ranges, the syntax of OWL 2 provides a "hook" allowing implementations to introduce extensions such as comparisons and arithmetic. An n-ary data range DR is interpreted as an n-ary relation (DR)^{DT} over Δ_{D} — that is, as a set (DT)^{DT} ⊆ (Δ_{D})^{n}
Data Range | Interpretation ⋅ ^{DT} |
---|---|
DataIntersectionOf( DR_{1} ... DR_{n} ) | (DR_{1})^{DT} ∩ ... ∩ (DR_{n})^{DT} |
DataUnionOf( DR_{1} ... DR_{n} ) | (DR_{1})^{DT} ∪ ... ∪ (DR_{n})^{DT} |
DataComplementOf( DR ) | (Δ_{D})^{n} \ (DR)^{DT} where n is the arity of DR |
DataOneOf( lt_{1} ... lt_{n} ) | { (lt_{1})^{LT} , ... , (lt_{n})^{LT} } |
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 S a set, #S denotes the number of elements in S.
Class Expression | Interpretation ⋅ ^{C} |
---|---|
ObjectIntersectionOf( CE_{1} ... CE_{n} ) | (CE_{1})^{C} ∩ ... ∩ (CE_{n})^{C} |
ObjectUnionOf( CE_{1} ... CE_{n} ) | (CE_{1})^{C} ∪ ... ∪ (CE_{n})^{C} |
ObjectComplementOf( CE ) | Δ_{I} \ (CE)^{C} |
ObjectOneOf( a_{1} ... a_{n} ) | { (a_{1})^{I} , ... , (a_{n})^{I} } |
ObjectSomeValuesFrom( OPE CE ) | { x | ∃ y : ⟨ x, y ⟩ ∈ (OPE)^{OP} and y ∈ (CE)^{C} } |
ObjectAllValuesFrom( OPE CE ) | { x | ∀ y : ⟨ x, y ⟩ ∈ (OPE)^{OP} implies y ∈ (CE)^{C} } |
ObjectHasValue( OPE a ) | { x | ⟨ x , (a)^{I} ⟩ ∈ (OPE)^{OP} } |
ObjectHasSelf( OPE ) | { x | ⟨ x , x ⟩ ∈ (OPE)^{OP} } |
ObjectMinCardinality( n OPE ) | { x | #{ y | ⟨ x , y ⟩ ∈ (OPE)^{OP} } ≥ n } |
ObjectMaxCardinality( n OPE ) | { x | #{ y | ⟨ x , y ⟩ ∈ (OPE)^{OP} } ≤ n } |
ObjectExactCardinality( n OPE ) | { x | #{ y | ⟨ x , y ⟩ ∈ (OPE)^{OP} } = n } |
ObjectMinCardinality( n OPE CE ) | { x | #{ y | ⟨ x , y ⟩ ∈ (OPE)^{OP} and y ∈ (CE)^{C} } ≥ n } |
ObjectMaxCardinality( n OPE CE ) | { x | #{ y | ⟨ x , y ⟩ ∈ (OPE)^{OP} and y ∈ (CE)^{C} } ≤ n } |
ObjectExactCardinality( n OPE CE ) | { x | #{ y | ⟨ x , y ⟩ ∈ (OPE)^{OP} and y ∈ (CE)^{C} } = n } |
DataSomeValuesFrom( DPE_{1} ... DPE_{n} DR ) | { x | ∃ y_{1}, ... , y_{n} : ⟨ x , y_{k} ⟩ ∈ (DPE_{k})^{DP} for each 1 ≤ k ≤ n and ⟨ y_{1} , ... , y_{n} ⟩ ∈ (DR)^{DT} } |
DataAllValuesFrom( DPE_{1} ... DPE_{n} DR ) | { x | ∀ y_{1}, ... , y_{n} : ⟨ x , y_{k} ⟩ ∈ (DPE_{k})^{DP} for each 1 ≤ k ≤ n imply ⟨ y_{1} , ... , y_{n} ⟩ ∈ (DR)^{DT} } |
DataHasValue( DPE lt ) | { x | ⟨ x , (lt)^{LT} ⟩ ∈ (DPE)^{DP} } |
DataMinCardinality( n DPE ) | { x | #{ y | ⟨ x , y ⟩ ∈ (DPE)^{DP}} ≥ n } |
DataMaxCardinality( n DPE ) | { x | #{ y | ⟨ x , y ⟩ ∈ (DPE)^{DP} } ≤ n } |
DataExactCardinality( n DPE ) | { x | #{ y | ⟨ x , y ⟩ ∈ (DPE)^{DP} } = n } |
DataMinCardinality( n DPE DR ) | { x | #{ y | ⟨ x , y ⟩ ∈ (DPE)^{DP} and y ∈ (DR)^{DT} } ≥ n } |
DataMaxCardinality( n DPE DR ) | { x | #{ y | ⟨ x , y ⟩ ∈ (DPE)^{DP} and y ∈ (DR)^{DT} } ≤ n } |
DataExactCardinality( n DPE DR ) | { x | #{ y | ⟨ x , y ⟩ ∈ (DPE)^{DP} and y ∈ (DR)^{DT} } = n } |
An interpretation I = ( Δ_{I} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{I} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) satisfies an axiom w.r.t. an ontology O if the axiom satisfies the relevant condition from the following sections. Satisfaction of axioms in I is defined w.r.t. O because satisfaction of key axioms uses the following function:
ISNAMED_{O}(x) = true for x ∈ Δ_{I} if and only if (a)^{I} = x for some named individual a occurring in the axiom closure of O
Satisfaction of OWL 2 class expression axioms in I 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_{k})^{C} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointClasses( CE_{1} ... CE_{n} ) | (CE_{j})^{C} ∩ (CE_{k})^{C} = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
DisjointUnion( C CE_{1} ... CE_{n} ) | (C)^{C} = (CE_{1})^{C} ∪ ... ∪ (CE_{n})^{C} and (CE_{j})^{C} ∩ (CE_{k})^{C} = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
Satisfaction of OWL 2 object property expression axioms in I w.r.t. O is defined as shown in Table 6.
Axiom | Condition |
---|---|
SubObjectPropertyOf( OPE_{1} OPE_{2} ) | (OPE_{1})^{OP} ⊆ (OPE_{2})^{OP} |
SubObjectPropertyOf( ObjectPropertyChain( OPE_{1} ... OPE_{n} ) OPE ) | ∀ y_{0} , ... , y_{n} : ⟨ y_{0} , y_{1} ⟩ ∈ (OPE_{1})^{OP} and ... and ⟨ y_{n-1} , y_{n} ⟩ ∈ (OPE_{n})^{OP} imply ⟨ y_{0} , y_{n} ⟩ ∈ (OPE)^{OP} |
EquivalentObjectProperties( OPE_{1} ... OPE_{n} ) | (OPE_{j})^{OP} = (OPE_{k})^{OP} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointObjectProperties( OPE_{1} ... OPE_{n} ) | (OPE_{j})^{OP} ∩ (OPE_{k})^{OP} = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
ObjectPropertyDomain( OPE CE ) | ∀ x , y : ⟨ x , y ⟩ ∈ (OPE)^{OP} implies x ∈ (CE)^{C} |
ObjectPropertyRange( OPE CE ) | ∀ x , y : ⟨ x , y ⟩ ∈ (OPE)^{OP} implies y ∈ (CE)^{C} |
InverseObjectProperties( OPE_{1} OPE_{2} ) | (OPE_{1})^{OP} = { ⟨ x , y ⟩ | ⟨ y , x ⟩ ∈ (OPE_{2})^{OP} } |
FunctionalObjectProperty( OPE ) | ∀ x , y_{1} , y_{2} : ⟨ x , y_{1} ⟩ ∈ (OPE)^{OP} and ⟨ x , y_{2} ⟩ ∈ (OPE)^{OP} imply y_{1} = y_{2} |
InverseFunctionalObjectProperty( OPE ) | ∀ x_{1} , x_{2} , y : ⟨ x_{1} , y ⟩ ∈ (OPE)^{OP} and ⟨ x_{2} , y ⟩ ∈ (OPE)^{OP} imply x_{1} = x_{2} |
ReflexiveObjectProperty( OPE ) | ∀ x : x ∈ Δ_{I} implies ⟨ x , x ⟩ ∈ (OPE)^{OP} |
IrreflexiveObjectProperty( OPE ) | ∀ x : x ∈ Δ_{I} implies ⟨ x , x ⟩ ∉ (OPE)^{OP} |
SymmetricObjectProperty( OPE ) | ∀ x , y : ⟨ x , y ⟩ ∈ (OPE)^{OP} implies ⟨ y , x ⟩ ∈ (OPE)^{OP} |
AsymmetricObjectProperty( OPE ) | ∀ x , y : ⟨ x , y ⟩ ∈ (OPE)^{OP} implies ⟨ y , x ⟩ ∉ (OPE)^{OP} |
TransitiveObjectProperty( OPE ) | ∀ x , y , z : ⟨ x , y ⟩ ∈ (OPE)^{OP} and ⟨ y , z ⟩ ∈ (OPE)^{OP} imply ⟨ x , z ⟩ ∈ (OPE)^{OP} |
Satisfaction of OWL 2 data property expression axioms in I w.r.t. O is defined as shown in Table 7.
Axiom | Condition |
---|---|
SubDataPropertyOf( DPE_{1} DPE_{2} ) | (DPE_{1})^{DP} ⊆ (DPE_{2})^{DP} |
EquivalentDataProperties( DPE_{1} ... DPE_{n} ) | (DPE_{j})^{DP} = (DPE_{k})^{DP} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointDataProperties( DPE_{1} ... DPE_{n} ) | (DPE_{j})^{DP} ∩ (DPE_{k})^{DP} = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
DataPropertyDomain( DPE CE ) | ∀ x , y : ⟨ x , y ⟩ ∈ (DPE)^{DP} implies x ∈ (CE)^{C} |
DataPropertyRange( DPE DR ) | ∀ x , y : ⟨ x , y ⟩ ∈ (DPE)^{DP} implies y ∈ (DR)^{DT} |
FunctionalDataProperty( DPE ) | ∀ x , y_{1} , y_{2} : ⟨ x , y_{1} ⟩ ∈ (DPE)^{DP} and ⟨ x , y_{2} ⟩ ∈ (DPE)^{DP} imply y_{1} = y_{2} |
Satisfaction of datatype definitions in I w.r.t. O is defined as shown in Table 8.
Axiom | Condition |
---|---|
DatatypeDefinition( DT DR ) | (DT)^{DT} = (DR)^{DT} |
Satisfaction of keys in I w.r.t. O is defined as shown in Table 9.
Axiom | Condition |
---|---|
HasKey( CE ( OPE_{1} ... OPE_{m} ) ( DPE_{1} ... DPE_{n} ) ) | ∀ x , y , z_{1} , ... , z_{m} , w_{1} , ... , w_{n} : if x ∈ (CE)^{C} and ISNAMED_{O}(x) and y ∈ (CE)^{C} and ISNAMED_{O}(y) and ⟨ x , z_{i} ⟩ ∈ (OPE_{i})^{OP} and ⟨ y , z_{i} ⟩ ∈ (OPE_{i})^{OP} and ISNAMED_{O}(z_{i}) for each 1 ≤ i ≤ m and ⟨ x , w_{j} ⟩ ∈ (DPE_{j})^{DP} and ⟨ y , w_{j} ⟩ ∈ (DPE_{j})^{DP} for each 1 ≤ j ≤ n then x = y |
Satisfaction of OWL 2 assertions in I w.r.t. O is defined as shown in Table 10.
Axiom | Condition |
---|---|
SameIndividual( a_{1} ... a_{n} ) | (a_{j})^{I} = (a_{k})^{I} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DifferentIndividuals( a_{1} ... a_{n} ) | (a_{j})^{I} ≠ (a_{k})^{I} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
ClassAssertion( CE a ) | (a)^{I} ∈ (CE)^{C} |
ObjectPropertyAssertion( OPE a_{1} a_{2} ) | ⟨ (a_{1})^{I} , (a_{2})^{I} ⟩ ∈ (OPE)^{OP} |
NegativeObjectPropertyAssertion( OPE a_{1} a_{2} ) | ⟨ (a_{1})^{I} , (a_{2})^{I} ⟩ ∉ (OPE)^{OP} |
DataPropertyAssertion( DPE a lt ) | ⟨ (a)^{I} , (lt)^{LT} ⟩ ∈ (DPE)^{DP} |
NegativeDataPropertyAssertion( DPE a lt ) | ⟨ (a)^{I} , (lt)^{LT} ⟩ ∉ (DPE)^{DP} |
An interpretation I satisfies an OWL 2 ontology O if all axioms in the axiom closure of O (with anonymous individuals standardized apart as described in Section 5.6.2 of the OWL 2 Specification [OWL 2 Specification]) are satisfied in I w.r.t. O.
Given a datatype map D, an interpretation I = ( Δ_{I} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{I} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) for D is a model of an OWL 2 ontology O w.r.t. D if an interpretation J = ( Δ_{I} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{J} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) for D exists such that ⋅ ^{J} coincides with ⋅ ^{I} on all named individuals and J satisfies O.
Thus, an interpretation I satisfying O is also a model of O. In contrast, a model I of O may not satisfy O directly; however, by modifying the interpretation of anonymous individuals, I can always be coerced into an interpretation J that satisfies O.
Let D be a datatype map and V a vocabulary over D. Furthermore, let O and O_{1} be OWL 2 ontologies, CE, CE_{1}, and CE_{2} class expressions, and a a named individual, such that all of them refer only to the vocabulary elements in V. Furthermore, variables are symbols that are not contained in V. Finally, a Boolean conjunctive query Q is a closed formula of the form
∃ x_{1} , ... , x_{n} , y_{1} , ... , y_{m} : [ A_{1} ∧ ... ∧ A_{k} ]
where each A_{i} is an atom of the form C(s), OP(s,t), or DP(s,u) with C a class, OP an object property, DP a data property, s and t individuals or some variable x_{j}, and u a literal or some variable y_{j}.
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_{1} w.r.t. D if every model of O w.r.t. D and V is also a model of O_{1} w.r.t. D and V.
Ontology Equivalence: O and O_{1} are equivalent w.r.t. D if O entails O_{1} w.r.t. D and O_{1} entails O w.r.t. D.
Ontology Equisatisfiability: O and O_{1} are equisatisfiable w.r.t. D if O is satisfiable w.r.t. D if and only if O_{1} is satisfiable w.r.t D.
Class Expression Satisfiability: CE is satisfiable w.r.t. O and D if a model I = ( Δ_{I} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{I} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) of O w.r.t. D and V exists such that (CE)^{C} ≠ ∅.
Class Expression Subsumption: CE_{1} is subsumed by a class expression CE_{2} w.r.t. O and D if (CE_{1})^{C} ⊆ (CE_{2})^{C} for each model I = ( Δ_{I} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{I} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) of O w.r.t. D and V.
Instance Checking: a is an instance of CE w.r.t. O and D if (a)^{I} ∈ (CE)^{C} for each model I = ( Δ_{I} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{I} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) of O w.r.t. D and V.
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 according to the standard definitions of first-order logic.
In order to ensure that ontology entailment, class expression satisfiability, class expression subsumption, and instance checking are decidable, the following restriction w.r.t. O needs to be satisfied:
Each class expression of type MinObjectCardinality, MaxObjectCardinality, ExactObjectCardinality, and ObjectHasSelf that occurs in O_{1}, CE, CE_{1}, and CE_{2} can contain only object property expressions that are simple in the axiom closure Ax of O.
For ontology equivalence to be decidable, O_{1} needs to satisfy this restriction w.r.t. O and vice versa. These restrictions are analogous to the first condition from Section 11.2 of the OWL 2 Specification [OWL 2 Specification].
OWL 2 DL has been defined so that the consequences of an OWL 2 DL ontology O do 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, and it has several useful consequences:
Theorem DS1. Let O_{1} and O_{2} be OWL 2 DL ontologies over a vocabulary V and D = ( N_{DT} , N_{LS} , N_{FS} , ⋅ ^{DT} , ⋅ ^{LS} , ⋅ ^{FS} ) a datatype map such that each datatype mentioned in O_{1} and O_{2} is rdfs:Literal, a datatype defined in the respective ontology, or it occurs in N_{DT}. Furthermore, let D' = ( N_{DT}' , N_{LS}' , N_{FS}' , ⋅ ^{DT '} , ⋅ ^{LS '} , ⋅ ^{FS '} ) be a datatype map such that N_{DT} ⊆ N_{DT}', N_{LS}(DT) = N_{LS}'(DT), and N_{FS}(DT) = N_{FS}'(DT) for each DT ∈ N_{DT}, and ⋅ ^{DT '}, ⋅ ^{LS '}, and ⋅ ^{FS '} are extensions of ⋅ ^{DT}, ⋅ ^{LS}, and ⋅ ^{FS}, respectively. Then, O_{1} entails O_{2} w.r.t. D if and only if O_{1} entails O_{2} w.r.t. D'.
Proof. Without loss of generality, one can assume O_{1} and O_{2} to be in negation-normal form [Description Logics]. Furthermore, since datatype definitions in O_{1} and O_{2} are acyclic, one can assume that each defined datatype has been recursively replaced with its definition; thus, all datatypes in O_{1} and O_{2} are from N_{DT} ∪ { rdfs:Literal }. The claim of the theorem is equivalent to the following statement: an interpretation I w.r.t. D and V exists such that O_{1} is and O_{2} is not satisfied in I if and only if an interpretation I' w.r.t. D' and V exists such that O_{1} is and O_{2} is not satisfied in I'. The (⇐) direction is trivial since each interpretation I w.r.t. D' and V is also an interpretation w.r.t. D and V. For the (⇒) direction, assume that an interpretation I = ( Δ_{I} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{I} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) w.r.t. D and V exists such that O_{1} is and O_{2} is not satisfied in I. Let I' = ( Δ_{I} , Δ_{D}' , ⋅ ^{C '} , ⋅ ^{OP} , ⋅ ^{DP '} , ⋅ ^{I} , ⋅ ^{DT '} , ⋅ ^{LT '} , ⋅ ^{FA '} ) be an interpretation such that
Clearly, DataComplementOf( DR )^{DT} ⊆ DataComplementOf( DR )^{DT '} for each data range DR that is either a datatype, a datatype restriction, or an enumerated data range. The owl:topDataProperty property can occur in O_{1} and O_{2} only in tautologies. The interpretation of all other data properties is the same in I and I', so (CE)^{C} = (CE)^{C '} for each class expression CE occurring in O_{1} and O_{2}. Therefore, O_{1} is and O_{2} is not satisfied in I'. QED
The starting point for the development of OWL 2 was the OWL1.1 member submission, itself a result of user and developer feedback, and in particular of information gathered during the OWL Experiences and Directions (OWLED) Workshop series. The working group also considered postponed issues from the WebOnt Working Group.
This document has been produced by the OWL Working Group (see below), and its contents reflect extensive discussions within the Working Group as a whole. The editors extend special thanks to Markus Krötzsch (FZI), Michael Schneider (FZI) and Thomas Schneider (University of Manchester) for their thorough reviews.
The regular attendees at meetings of the OWL Working Group at the time of publication of this document were: Jie Bao (RPI), Diego Calvanese (Free University of Bozen-Bolzano), Bernardo Cuenca Grau (Oxford University), Martin Dzbor (Open University), Achille Fokoue (IBM Corporation), Christine Golbreich (Université de Versailles St-Quentin and LIRMM), Sandro Hawke (W3C/MIT), Ivan Herman (W3C/ERCIM), Rinke Hoekstra (University of Amsterdam), Ian Horrocks (Oxford University), Elisa Kendall (Sandpiper Software), Markus Krötzsch (FZI), Carsten Lutz (Universität Bremen), Deborah L. McGuinness (RPI), Boris Motik (Oxford University), Jeff Pan (University of Aberdeen), Bijan Parsia (University of Manchester), Peter F. Patel-Schneider (Bell Labs Research, Alcatel-Lucent), Alan Ruttenberg (Science Commons), Uli Sattler (University of Manchester), Michael Schneider (FZI), Mike Smith (Clark & Parsia), Evan Wallace (NIST), and Zhe Wu (Oracle Corporation). We would also like to thank past members of the working group: Jeremy Carroll, Jim Hendler, Vipul Kashyap.