Direct Semantics

From OWL

(Redirected from Semantics)

Jump to: navigation, search

[Hide Review Comments]

Document title:: OWL 2 Web Ontology Language
Direct Semantics

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.

Abstract: 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.
Status of this Document

1 Introduction
2 Model-Theoretic Semantics for OWL 2
3 Independence of the Semantics from the Datatype Map
4 References

1 Introduction

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.

2 Model-Theoretic Semantics for OWL 2

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

2.1 Vocabulary

Let D = ( N_DT , N_LT , N_FA , ⋅ ^DT , ⋅ ^LT , ⋅ ^FA ) be a datatype map as defined in Section 4 of the OWL 2 Specification [OWL 2 Specification], interpreting the built-in datatypes as defined in Sections 4.1 to 4.6. A vocabulary V = ( V_C , V_OP , V_DP , V_I , V_DT , V_LT , V_FA ) over D is a 7-tuple consisting of the following elements:

V_C is a set of classes as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the classes owl:Thing and owl:Nothing.
V_OP is a set of object properties as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the object properties owl:TopObjectProperty and owl:BottomObjectProperty.
V_DP is a set of data properties as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the data properties owl:TopDataProperty and owl:BottomDataProperty.
V_I is a set of individuals (named and anonymous) as defined in the OWL 2 Specification [OWL 2 Specification].
V_DT is the set of all datatypes of D extended with the datatype rdfs:Literal; that is, V_DT = N_DT ∪ { rdfs:Literal }.
V_LT is a function that assigns to each datatype DT ∈ V_DT a set of literals V_LT(DT), such that
- V_LT(DT) = N_LT(DT) for each datatype DT ∈ N_DT and
- V_LT(rdfs:Literal) = ∅.
V_FA is the function assigning to each datatype DT ∈ V_DT a set V_FA(DT) of pairs of the form ⟨ f lt ⟩, where f is a constraining facet and lt ∈ V_LT, such that
- V_FA(DT) = N_FA(DT) for each datatype DT ∈ N_DT and
- 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.

2.2 Interpretations

Given a datatype map D and a vocabulary V over D, an interpretation Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT , ⋅ ^FA ) for D and V is a 9-tuple with the following structure.

Δ_Int is a nonempty set called the object domain.
Δ_D is a nonempty set disjoint with Δ_Int called the data domain such that (DT)^DT ⊆ Δ_D for each datatype DT ∈ V_DT.
⋅ ^C is the class interpretation function that assigns to each class C ∈ V_C a subset (C)^C ⊆ Δ_Int such that
- (owl:Thing)^C = Δ_Int and
- (owl:Nothing)^C = ∅.
⋅ ^OP is the object property interpretation function that assigns to each object property OP ∈ V_OP a subset (OP)^OP ⊆ Δ_Int × Δ_Int such that
- (owl:TopObjectProperty)^OP = Δ_Int × Δ_Int and
- (owl:BottomObjectProperty)^OP = ∅.
⋅ ^DP is the data property interpretation function that assigns to each data property DP ∈ V_DP a subset (DP)^DP ⊆ Δ_Int × Δ_D such that
- (owl:TopDataProperty)^DP = Δ_Int × Δ_D and
- (owl:BottomDataProperty)^DP = ∅.
⋅ ^I is the individual interpretation function that assigns to each individual a ∈ V_I an element (a)^I ∈ Δ_Int.
⋅ ^DT, ⋅ ^LT, and ⋅ ^FA are the same as in D, and (rdfs:Literal)^DT = Δ_D.

The following sections define the extensions of ⋅ ^OP, ⋅ ^DT, and ⋅ ^C to object property expressions, data ranges, and class expressions.

2.2.1 Object Property Expressions

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

Table 1. Interpreting Object Property Expressions
Object Property Expression	Interpretation ⋅ ^OP
InverseOf( OP )	{ ⟨ x , y ⟩ \| ⟨ y , x ⟩ ∈ (OP)^OP }

2.2.2 Data Ranges

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 DT is interpreted as a unary relation (DT)^DT over Δ_D. Data ranges, however, can be n-ary—this allows implementations to provide built-in predicates such as comparisons or arithmetic as an extension. Hence, an n-ary data range DR is interpreted as an n-ary relation (DR)^DT over Δ_D.

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

Table 3. Interpreting Data Ranges
Data Range	Interpretation ⋅ ^DT
OneOf( lt₁ ... lt_n )	{ (lt₁)^LT , ... , (lt_n)^LT }
ComplementOf( DR )	(Δ_D)ⁿ \ (DR)^DT where n is the arity of DR
DatatypeRestriction( DT f₁ lt₁ ... f_n lt_n )	(DT)^DT ∩ (⟨ f₁ lt₁ ⟩)^FA ∩ ... ∩ (⟨ f_n lt_n ⟩)^FA

2.2.3 Class Expressions

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.

Table 4. Interpreting Class Expressions
Class Expression	Interpretation ⋅ ^C
IntersectionOf( CE₁ ... CE_n )	(CE₁)^C ∩ ... ∩ (CE_n)^C
UnionOf( CE₁ ... CE_n )	(CE₁)^C ∪ ... ∪ (CE_n)^C
ComplementOf( CE )	Δ_Int \ (CE)^C
OneOf( a₁ ... a_n )	{ (a₁)^I , ... , (a_n)^I }
SomeValuesFrom( OPE CE )	{ x \| ∃ y : ⟨ x, y ⟩ ∈ (OPE)^OP and y ∈ (CE)^C }
AllValuesFrom( OPE CE )	{ x \| ∀ y : ⟨ x, y ⟩ ∈ (OPE)^OP implies 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)^OP } ≥ n }
MaxCardinality( n OPE )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (OPE)^OP } ≤ n }
ExactCardinality( n OPE )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (OPE)^OP } = n }
MinCardinality( n OPE CE )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (OPE)^OP and y ∈ (CE)^C } ≥ n }
MaxCardinality( n OPE CE )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (OPE)^OP and y ∈ (CE)^C } ≤ n }
ExactCardinality( n OPE CE )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (OPE)^OP and y ∈ (CE)^C } = n }
SomeValuesFrom( DPE₁ ... DPE_n DR )	{ x \| ∃ y₁, ... , y_n : ⟨ x , y_k ⟩ ∈ (DPE_k)^DP for each 1 ≤ k ≤ n and ⟨ y₁ , ... , y_n ⟩ ∈ (DR)^DT }
AllValuesFrom( DPE₁ ... DPE_n DR )	{ x \| ∀ y₁, ... , y_n : ⟨ x , y_k ⟩ ∈ (DPE_k)^DP for each 1 ≤ k ≤ n imply ⟨ y₁ , ... , y_n ⟩ ∈ (DR)^DT }
HasValue( DPE lt )	{ x \| ⟨ x , (lt)^LT ⟩ ∈ (DPE)^DP }
MinCardinality( n DPE )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (DPE)^DP} ≥ n }
MaxCardinality( n DPE )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (DPE)^DP } ≤ n }
ExactCardinality( n DPE )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (DPE)^DP } = n }
MinCardinality( n DPE DR )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (DPE)^DP and y ∈ (DR)^DT } ≥ n }
MaxCardinality( n DPE DR )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (DPE)^DP and y ∈ (DR)^DT } ≤ n }
ExactCardinality( n DPE DR )	{ x \| #{ y \| ⟨ x , y ⟩ ∈ (DPE)^DP and y ∈ (DR)^DT } = n }

2.3 Satisfaction in an Interpretation

An interpretation Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT , ⋅ ^FA ) satisfies an axiom w.r.t. an ontology O if the axiom satisfies appropriate conditions listed in the following sections. Satisfaction of axioms in Int is defined w.r.t. O because satisfaction of key axioms uses the function ISNAMED_O defined as follows, where the axiom closure of O is defined in Section 3.4 of the OWL 2 Specification [OWL 2 Specification]:

ISNAMED_O(x) = true for x ∈ Δ_Int if and only if (a)^I = x for some named individual a occurring in the axiom closure of O.

2.3.1 Class Expression Axioms

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

Table 5. Satisfaction of Class Expression Axioms in an Interpretation
Axiom	Condition
SubClassOf( CE₁ CE₂ )	(CE₁)^C ⊆ (CE₂)^C
EquivalentClasses( CE₁ ... CE_n )	(CE_j)^C = (CE_k)^C for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n
DisjointClasses( CE₁ ... 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₁ ... CE_n )	(C)^C = (CE₁)^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

2.3.2 Object Property Expression Axioms

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

Table 6. Satisfaction of Object Property Expression Axioms in an Interpretation
Axiom	Condition
SubPropertyOf( OPE₁ OPE₂ )	(OPE₁)^OP ⊆ (OPE₂)^OP
SubPropertyOf( PropertyChain( OPE₁ ... OPE_n ) OPE )	∀ y₀ , ... , y_n : ⟨ y₀ , y₁ ⟩ ∈ (OPE₁)^OP and ... and ⟨ y_n-1 , y_n ⟩ ∈ (OPE_n)^OP imply ⟨ y₀ , y_n ⟩ ∈ (OPE)^OP
EquivalentProperties( OPE₁ ... OPE_n )	(OPE_j)^OP = (OPE_k)^OP for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n
DisjointProperties( OPE₁ ... OPE_n )	(OPE_j)^OP ∩ (OPE_k)^OP = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k
PropertyDomain( OPE CE )	∀ x , y : ⟨ x , y ⟩ ∈ (OPE)^OP implies x ∈ (CE)^C
PropertyRange( OPE CE )	∀ x , y : ⟨ x , y ⟩ ∈ (OPE)^OP implies y ∈ (CE)^C
InverseProperties( OPE₁ OPE₂ )	(OPE₁)^OP = { ⟨ x , y ⟩ \| ⟨ y , x ⟩ ∈ (OPE₂)^OP }
FunctionalProperty( OPE )	∀ x , y₁ , y₂ : ⟨ x , y₁ ⟩ ∈ (OPE)^OP and ⟨ x , y₂ ⟩ ∈ (OPE)^OP imply y₁ = y₂
InverseFunctionalProperty( OPE )	∀ x₁ , x₂ , y : ⟨ x₁ , y ⟩ ∈ (OPE)^OP and ⟨ x₂ , y ⟩ ∈ (OPE)^OP imply x₁ = x₂
ReflexiveProperty( OPE )	∀ x : x ∈ Δ_Int implies ⟨ x , x ⟩ ∈ (OPE)^OP
IrreflexiveProperty( OPE )	∀ x : x ∈ Δ_Int implies ⟨ x , x ⟩ ∉ (OPE)^OP
SymmetricProperty( OPE )	∀ x , y : ⟨ x , y ⟩ ∈ (OPE)^OP implies ⟨ y , x ⟩ ∈ (OPE)^OP
AsymmetricProperty( OPE )	∀ x , y : ⟨ x , y ⟩ ∈ (OPE)^OP implies ⟨ y , x ⟩ ∉ (OPE)^OP
TransitiveProperty( OPE )	∀ x , y , z : ⟨ x , y ⟩ ∈ (OPE)^OP and ⟨ y , z ⟩ ∈ (OPE)^OP imply ⟨ x , z ⟩ ∈ (OPE)^OP

2.3.3 Data Property Expression Axioms

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

Table 7. Satisfaction of Data Property Expression Axioms in an Interpretation
Axiom	Condition
SubPropertyOf( DPE₁ DPE₂ )	(DPE₁)^DP ⊆ (DPE₂)^DP
EquivalentProperties( DPE₁ ... DPE_n )	(DPE_j)^DP = (DPE_k)^DP for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n
DisjointProperties( DPE₁ ... DPE_n )	(DPE_j)^DP ∩ (DPE_k)^DP = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k
PropertyDomain( DPE CE )	∀ x , y : ⟨ x , y ⟩ ∈ (DPE)^DP implies x ∈ (CE)^C
PropertyRange( DPE DR )	∀ x , y : ⟨ x , y ⟩ ∈ (DPE)^DP implies y ∈ (DR)^DT
FunctionalProperty( DPE )	∀ x , y₁ , y₂ : ⟨ x , y₁ ⟩ ∈ (DPE)^DP and ⟨ x , y₂ ⟩ ∈ (DPE)^DP imply y₁ = y₂

2.3.4 Keys

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

Table 8. Satisfaction of Keys in an Interpretation
Axiom	Condition
HasKey( CE PE₁ ... PE_n )	∀ x , y , z₁ , ... , z_n : if ISNAMED_O(x) and ISNAMED_O(y) and ISNAMED_O(z₁) and ... and ISNAMED_O(z_n) and x ∈ (CE)^C and y ∈ (CE)^C and for each 1 ≤ i ≤ n, if PE_i is an object property, then ⟨ x , z_i ⟩ ∈ (PE_i)^OP and ⟨ y , z_i ⟩ ∈ (PE_i)^OP, and if PE_i is a data property, then ⟨ x , z_i ⟩ ∈ (PE_i)^DP and ⟨ y , z_i ⟩ ∈ (PE_i)^DP then x = y

2.3.5 Assertions

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

Table 9. Satisfaction of Assertions in an Interpretation
Axiom	Condition
SameIndividual( a₁ ... a_n )	(a_j)^I = (a_k)^I for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n
DifferentIndividuals( a₁ ... 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
PropertyAssertion( OPE a₁ a₂ )	⟨ (a₁)^I , (a₂)^I ⟩ ∈ (OPE)^OP
NegativePropertyAssertion( OPE a₁ a₂ )	⟨ (a₁)^I , (a₂)^I ⟩ ∉ (OPE)^OP
PropertyAssertion( DPE a lt )	⟨ (a)^I , (lt)^LT ⟩ ∈ (DPE)^DP
NegativePropertyAssertion( DPE a lt )	⟨ (a)^I , (lt)^LT ⟩ ∉ (DPE)^DP

2.3.6 Ontologies

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.

2.4 Models

An interpretation Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT , ⋅ ^FA ) is a model of an OWL 2 ontology O if an interpretation Int' = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I' , ⋅ ^DT , ⋅ ^LT , ⋅ ^FA ) exists such that ⋅ ^I' coincides with ⋅ ^I on all named individuals and Int' satisfies O.

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.

2.5 Inference Problems

Let D be a datatype map and V a vocabulary over D. Furthermore, let O and O' be OWL 2 ontologies, CE, CE₁, and CE₂ class expressions, and a a named individual, such that all of them refer only to the vocabulary elements in V. A Boolean conjunctive query Q is a closed formula of the form [ ∃ x₁ , ... , x_n , y₁ , ... , y_m : A₁ ∧ ... ∧ 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' 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 , Δ_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₁ is subsumed by a class expression CE₂ w.r.t. O and D if (CE₁)^C ⊆ (CE₂)^C for each model Int = ( Δ_Int , Δ_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 Int = ( Δ_Int , Δ_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.

3 Independence of the Semantics from the Datatype Map

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₁ and O₂ be OWL 2 ontologies over a vocabulary V and D = ( N_DT , N_LT , N_FA , ⋅ ^DT , ⋅ ^LT , ⋅ ^FA ) a datatype map such that each datatype mentioned in O₁ and O₂ is either rdfs:Literal or it occurs in N_DT. Furthermore, let D' = ( N_DT' , N_LT' , N_FA' , ⋅ ^DT ' , ⋅ ^LT ' , ⋅ ^FA ' ) be a datatype map such that N_DT ⊆ N_DT', N_LT(DT) = N_LT'(DT) and N_FA(DT) = N_FA'(DT) for each DT ∈ N_DT, and ⋅ ^DT ', ⋅ ^LT ', and ⋅ ^FA ' are extensions of ⋅ ^DT, ⋅ ^LT, and ⋅ ^FA, respectively. Then, O₁ entails O₂ w.r.t. D if and only if O₁ entails O₂ w.r.t. D'.

Proof. Without loss of generality, one can assume O₁ and O₂ to be in negation-normal form [Description Logics]. The claim of the theorem is equivalent to the following statement: an interpretation Int w.r.t. D and and V exists such that O₁ is and O₂ is not satisfied in Int if and only if an interpretation Int' w.r.t. D' and V exists such that O₁ is and O₂ is not satisfied in Int'. The (⇐) direction is trivial since each interpretation Int w.r.t. D' and V is also an interpretation w.r.t. D and V. For the (⇒) direction, assume that an interpretation Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT , ⋅ ^FA ) w.r.t. D and V exists such that O₁ is and O₂ is not satisfied in Int. Let Int' = ( Δ_Int , Δ_D' , ⋅ ^C ' , ⋅ ^OP , ⋅ ^DP ' , ⋅ ^I , ⋅ ^DT ' , ⋅ ^LT ' , ⋅ ^FA ' ) be an interpretation such that

Δ_D' is obtained by extending Δ_D with the value space of all datatypes in N_DT' \ N_DT,
⋅ ^C ' coincides with ⋅ ^C on all classes, and
⋅ ^DP ' coincides with ⋅ ^DP on all data properties apart from owl:TopDataProperty.

Clearly, ComplementOf( DR )^DT ⊆ ComplementOf( DR )^DT ' for each data range DR that is is either a datatype, a datatype restriction, or an enumerated data range. The interpretation of data properties is the same in Int and Int', so (CE)^C = (CE)^C ' for each class expression CE occurring in O₁ and O₂. Therefore, O₁ is and O₂ is not satisfied in Int'. QED

4 References

[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. Peter F. Patel-Schneider, Ian Horrocks, and Boris Motik, eds., 2006.
[OWL 2 Profiles]: OWL 2 Web Ontology Language: Profiles. Bernardo Cuenca Grau, Boris Motik, Zhe Wu, Achille Fokoue, Carsten Lutz, eds., 2006.
[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).

Retrieved from "http://www.w3.org/2007/OWL/wiki/Direct_Semantics"