Difference between revisions of "Direct Semantics"

From OWL
Jump to: navigation, search
(Datatype Maps)
(Interpretations)
(4 intermediate revisions by one user not shown)
Line 86: Line 86:
 
* ''&sdot;&nbsp;<sup>C</sup>'' is the ''class interpretation'' function that assigns to each class ''C &isin; N<sub>C</sub>'' \ { ''owl:Thing'' , ''owl:Nothing'' } a subset ''C<sup>C</sup>'' &sube; ''&Delta;<sub>Int</sub>''.
 
* ''&sdot;&nbsp;<sup>C</sup>'' is the ''class interpretation'' function that assigns to each class ''C &isin; N<sub>C</sub>'' \ { ''owl:Thing'' , ''owl:Nothing'' } a subset ''C<sup>C</sup>'' &sube; ''&Delta;<sub>Int</sub>''.
  
* ''&sdot;&nbsp;<sup>OP</sup>'' is the ''object property interpretation'' function that assigns to each object property ''OP &isin; N<sub>OP</sub>'' a subset ''(OP)<sup>OP</sup>'' &sube; ''&Delta;<sub>Int</sub>'' &times; ''&Delta;<sub>Int</sub>''.
+
* ''&sdot;&nbsp;<sup>OP</sup>'' is the ''object property interpretation'' function that assigns to each object property ''OP &isin; N<sub>OP</sub>'' \ { ''owl:TopObjectProperty'' , ''owl:BottomObjectProperty'' } a subset ''(OP)<sup>OP</sup>'' &sube; ''&Delta;<sub>Int</sub>'' &times; ''&Delta;<sub>Int</sub>''.
  
* ''&sdot;&nbsp;<sup>DP</sup>'' is the ''data property interpretation'' function that assigns to each data property ''DP &isin; N<sub>DP</sub>'' a subset ''(DP)<sup>DP</sup>'' &sube; ''&Delta;<sub>Int</sub>'' &times; ''&Delta;<sub>D</sub>''.
+
* ''&sdot;&nbsp;<sup>DP</sup>'' is the ''data property interpretation'' function that assigns to each data property ''DP &isin; N<sub>DP</sub>'' \ { ''owl:TopDataProperty'' , ''owl:BottomDataProperty'' } a subset ''(DP)<sup>DP</sup>'' &sube; ''&Delta;<sub>Int</sub>'' &times; ''&Delta;<sub>D</sub>''.
  
 
* ''&sdot;&nbsp;<sup>I</sup>'' is the ''individual interpretation'' function that assigns to each individual ''a &isin; N<sub>I</sub>'' an element ''a<sup>I</sup>'' &isin; ''&Delta;<sub>Int</sub>''.
 
* ''&sdot;&nbsp;<sup>I</sup>'' is the ''individual interpretation'' function that assigns to each individual ''a &isin; N<sub>I</sub>'' an element ''a<sup>I</sup>'' &isin; ''&Delta;<sub>Int</sub>''.
Line 106: Line 106:
 
! Object Property Expression ''OPE''
 
! Object Property Expression ''OPE''
 
! Interpretation ''(OPE)<sup>OP</sup>''
 
! Interpretation ''(OPE)<sup>OP</sup>''
|-  
+
|-
 +
| class="name" | ''owl:TopObjectProperty''
 +
| ''&Delta;<sub>Int</sub>'' &times; ''&Delta;<sub>Int</sub>''
 +
|-
 +
| class="name" | ''owl:BottomObjectProperty''
 +
| &empty;
 +
|-
 
| class="name" | InverseOf( OP )
 
| class="name" | InverseOf( OP )
 
| { &lt; ''x'' , ''y'' &gt; <nowiki>|</nowiki> &lt; ''y'' , ''x'' &gt; &isin; ''(OP)<sup>OP</sup>'' }
 
| { &lt; ''x'' , ''y'' &gt; <nowiki>|</nowiki> &lt; ''y'' , ''x'' &gt; &isin; ''(OP)<sup>OP</sup>'' }
 +
|-
 +
|}
 +
</div>
 +
 +
==== Data Property Expressions ====
 +
 +
The data property interpretation function ''&sdot;&nbsp;<sup>DP</sup>'' is extended to data property expressions as shown in Table 2.
 +
 +
<div class="center">
 +
{| border="2" cellpadding="5"
 +
|+ <span class="caption">Table 2.</span> Interpreting Data Property Expressions
 +
|-
 +
! Data Property Expression ''DPE''
 +
! Interpretation ''(DPE)<sup>DP</sup>''
 +
|-
 +
| class="name" | ''owl:TopDataProperty''
 +
| ''&Delta;<sub>Int</sub>'' &times; ''&Delta;<sub>D</sub>''
 +
|-
 +
| class="name" | ''owl:BottomDataProperty''
 +
| &empty;
 +
|-
 
|}
 
|}
 
</div>
 
</div>
Line 114: Line 141:
 
==== Data Range Expressions ====
 
==== Data Range Expressions ====
  
The datatype interpretation function ''&sdot;&nbsp;<sup>DT</sup>'' is extended to data ranges as shown in Table 2.
+
The datatype interpretation function ''&sdot;&nbsp;<sup>DT</sup>'' is extended to data ranges as shown in Table 3.
  
 
<div class="center">
 
<div class="center">
 
{| border="2" cellpadding="5"
 
{| border="2" cellpadding="5"
|+ <span class="caption">Table 2.</span> Interpreting Data Ranges
+
|+ <span class="caption">Table 3.</span> Interpreting Data Ranges
 
|-
 
|-
 
! Data Range ''DR''
 
! Data Range ''DR''
Line 142: Line 169:
 
==== Class Expressions ====
 
==== Class Expressions ====
  
The class interpretation function ''&sdot;&nbsp;<sup>C</sup>'' is extended to class expressions as shown in Table 3. For ''S'' a set, ''<nowiki>#S</nowiki>'' denotes the number of elements in ''S''.
+
The class interpretation function ''&sdot;&nbsp;<sup>C</sup>'' is extended to class expressions as shown in Table 4. For ''S'' a set, ''<nowiki>#S</nowiki>'' denotes the number of elements in ''S''.
  
 
<div class="center">
 
<div class="center">
 
{| border="2" cellpadding="5"
 
{| border="2" cellpadding="5"
|+ <span class="caption">Table 3.</span> Interpreting Class Expressions
+
|+ <span class="caption">Table 4.</span> Interpreting Class Expressions
 
|-
 
|-
 
! Class Expression ''CE''
 
! Class Expression ''CE''
Line 234: Line 261:
 
==== Class Expression Axioms ====
 
==== Class Expression Axioms ====
  
Satisfaction of OWL 2 class expression axioms in ''Int'' is defined as shown in Table 4.
+
Satisfaction of OWL 2 class expression axioms in ''Int'' is defined as shown in Table 5.
  
 
<div class="center">
 
<div class="center">
 
{| border="2" cellpadding="5"
 
{| border="2" cellpadding="5"
|+ <span class="caption">Table 4.</span> Satisfaction of Class Expression Axioms in ''Int''
+
|+ <span class="caption">Table 5.</span> Satisfaction of Class Expression Axioms in ''Int''
 
|-
 
|-
 
! Axiom
 
! Axiom
Line 260: Line 287:
 
==== Object Property Expression Axioms ====
 
==== Object Property Expression Axioms ====
  
Satisfaction of OWL 2 object property expression axioms in ''Int'' is defined as shown in Table 5.
+
Satisfaction of OWL 2 object property expression axioms in ''Int'' is defined as shown in Table 6.
  
 
<div class="center">
 
<div class="center">
 
{| border="2" cellpadding="5"
 
{| border="2" cellpadding="5"
|+ <span class="caption">Table 5.</span> Satisfaction of Object Property Expression Axioms in ''Int''
+
|+ <span class="caption">Table 6.</span> Satisfaction of Object Property Expression Axioms in ''Int''
 
|-
 
|-
 
! Axiom
 
! Axiom
Line 316: Line 343:
 
==== Data Property Expression Axioms ====
 
==== Data Property Expression Axioms ====
  
Satisfaction of OWL 2 data property expression axioms in ''Int'' is defined as shown in Table 6.
+
Satisfaction of OWL 2 data property expression axioms in ''Int'' is defined as shown in Table 7.
  
 
<div class="center">
 
<div class="center">
 
{| border="2" cellpadding="5"
 
{| border="2" cellpadding="5"
|+ <span class="caption">Table 6.</span> Satisfaction of Data Property Expression Axioms in an Interpretation
+
|+ <span class="caption">Table 7.</span> Satisfaction of Data Property Expression Axioms in an Interpretation
 
|-
 
|-
 
! Axiom
 
! Axiom
Line 348: Line 375:
 
==== Assertions ====
 
==== Assertions ====
  
Satisfaction of OWL 2 assertions in ''Int'' is defined as shown in Table 7.
+
Satisfaction of OWL 2 assertions in ''Int'' is defined as shown in Table 8.
  
 
<div class="center">
 
<div class="center">
 
{| border="2" cellpadding="5"
 
{| border="2" cellpadding="5"
|+ <span class="caption">Table 7.</span> Satisfaction of Assertions in ''Int''
+
|+ <span class="caption">Table 8.</span> Satisfaction of Assertions in ''Int''
 
|-
 
|-
 
! Axiom
 
! Axiom

Revision as of 16:19, 16 June 2008

__NUMBEREDHEADINGS__

[Hide Review Comments]

Document title:
OWL 2 Web Ontology Language
Model-Theoretic Semantics (Second Edition)
Authors
Bernardo Cuenca Grau, Oxford University
Boris Motik, Oxford University
Contributors
Ian Horrocks, Oxford University
Bijan Parsia, The University of Manchester
Peter F. Patel-Schneider, Bell Labs Research, Alcatel-Lucent
Ulrike Sattler, The University of Manchester
Abstract
The OWL 2 Web Ontology Language, informally OWL 2, is an ontology language for the Semantic Web with formally defined meaning. OWL 2 ontologies provide classes, properties, individuals, and data values and are stored as Semantic Web documents. OWL 2 ontologies can be used along with information written in RDF, and OWL 2 ontologies themselves are primarily exchanged as RDF documents. The OWL 2 Document Overview describes the overall state of OWL 2, and should be read before other OWL 2 documents.
This document provides a model-theoretic semantics for OWL 2.
Status of this Document
This document is an evolution of the OWL 1.1 Web Ontology Language: Model-Theoretic Semantics document that forms part of the OWL 1.1 Web Ontology Language W3C Member Submission.

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

1 Introduction

Editor's Note: See Issue-72 (Annotation Semantics).
Editor's Note: See Issue 69 (punning).

This document defines the formal semantics of OWL 2. The semantics given here follows the principles for defining the semantics of description logics [Description Logics] and is compatible with the description logic SROIQ [SROIQ]. Unfortunately, the definition of SROIQ does not provide for datatypes and punning. Therefore, the semantics of OWL 2 is defined in a direct model-theoretic way, by interpreting the constructs of the functional-style syntax from [OWL 2 Specification]. 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 and is equivalent to the official definition [OWL Abstract Syntax and Semantics].

OWL 2 allows for annotations of ontologies and ontology entities (classes, properties, and individuals) and ontology axioms. Annotations, however, have no semantic meaning in OWL 2 and are ignored in this document.

OWL 2 declarations are not interpreted directly; they 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 Datatype Maps

A datatype map is a 4-tuple D = ( NDT , NCT , ⋅ DT , ⋅ CT ) that defines the set of supported datatypes and their interpretation.

  • NDT is a set of datatypes as defined in the OWL 2 Specification [OWL 2 Specification], each associated with a positive integer arity, containing at least the unary datatype rdfs:Literal.
  • NCT is a function that assigns to each datatype DTNDT a set of constants NCT(DT); this set is sometimes also called a lexical space of DT; furthermore, NCT(rdfs:Literal) = ∅. The set of all constants for all datatypes is given as the set NCT (whether NCT is used as a function or as a set of all constants is expected to be clear from the context).
  • For each n-ary datatype DTNDT \ { rdfs:Literal }, the function ⋅ DT assigns to DT an n-ary relation (DT)DT called a value space.
  • For each unary datatype DTNDT \ { rdfs:Literal } and each constant ct ∈ NCT(DT), the function ⋅ CT assigns to ct a data value (ct)CT(DT)DT.

The value spaces of the XML Schema Datatypes and the mappings of their constants to data values is defined as in XML Schema Datatypes [XML Schema Datatypes]. The value space for owl:internationalizedString consists of all pairs <"text",languageTag>, where "text" is a string and languageTag is a language tag.

2.2 Vocabulary

Given a datatype map D = ( NDT , NCT , ⋅ DT , ⋅ CT ), a vocabulary (or signature) V = ( NC , NOP , NDP , NI , NDT , NCT ) over D is a 6-tuple consisting of the following elements:

  • NC is a set of classes as defined in OWL 2 Specification [OWL 2 Specification], containing at least the classes owl:Thing and owl:Nothing.
  • NOP is a set of object properties as defined in OWL 2 Specification [OWL 2 Specification].
  • NDP is a set of data properties as defined in OWL 2 Specification [OWL 2 Specification].
  • NI is a set of individuals as defined in OWL 2 Specification [OWL 2 Specification].
  • NDT is the set of all datatypes of D.
  • NCT is a set of all constants of D.

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;
  • C denotes a class;
  • CE denotes a class expression;
  • DT denotes a data type;
  • DR denotes a data range;
  • a denotes an individual; and
  • ct denotes a constant.

2.3 Interpretations

Given a datatype map D and a vocabulary V over D, an interpretation Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ CT ) is a 8-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, for each datatype DTNDT and each tuple < α1 , ... , αk > ∈ (DT)DT, it is the case that αiΔD for each 1 ≤ i ≤ k.
  • ⋅ C is the class interpretation function that assigns to each class C ∈ NC \ { owl:Thing , owl:Nothing } a subset CCΔInt.
  • ⋅ OP is the object property interpretation function that assigns to each object property OP ∈ NOP \ { owl:TopObjectProperty , owl:BottomObjectProperty } a subset (OP)OPΔInt × ΔInt.
  • ⋅ DP is the data property interpretation function that assigns to each data property DP ∈ NDP \ { owl:TopDataProperty , owl:BottomDataProperty } a subset (DP)DPΔInt × ΔD.
  • ⋅ I is the individual interpretation function that assigns to each individual a ∈ NI an element aIΔInt.
  • ⋅ DT and ⋅ CT are the same as in D.

The following sections define the extensions of ⋅ OP , ⋅ DT , and ⋅ C to object property expressions, data ranges, and class expressions. Since data property expressions are currently restricted to data properties, it is not necessary to define an extension of ⋅ DP to data property expressions.

2.3.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 OPE Interpretation (OPE)OP
owl:TopObjectProperty ΔInt × ΔInt
owl:BottomObjectProperty
InverseOf( OP ) { < x , y > | < y , x > ∈ (OP)OP }

2.3.2 Data Property Expressions

The data property interpretation function ⋅ DP is extended to data property expressions as shown in Table 2.

Table 2. Interpreting Data Property Expressions
Data Property Expression DPE Interpretation (DPE)DP
owl:TopDataProperty ΔInt × ΔD
owl:BottomDataProperty

2.3.3 Data Range Expressions

The datatype interpretation function ⋅ DT is extended to data ranges as shown in Table 3.

Table 3. Interpreting Data Ranges
Data Range DR Interpretation (DR)DT
rdfs:Literal ΔD
OneOf( ct1 ... ctn ) { (ct1)CT , ... , (ctn)CT }
ComplementOf( DR ) D)n \ (DR)DT where n is the arity of DR
DatatypeRestriction( DT f1 v1 ... fn vn )

the subset of (DT)DT obtained by applying to it
the facets f1 to fn with values v1 to vn, respectively,
as specified by the definition of facets in XML Schema Datatypes [XML Schema Datatypes]

2.3.4 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 CE Interpretation (CE)C
owl:Thing ΔInt
owl:Nothing
ComplementOf( CE ) ΔInt \ (CE)C
IntersectionOf( CE1 ... CEn ) (CE1)C ∩ ... ∩ (CEn)C
UnionOf( CE1 ... CEn ) (CE1)C ∪ ... ∪ (CEn)C
OneOf( a1 ... an ) { (a1)I , ... , (an)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 , aI > ∈ (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( DPE1 ... DPEn DR ) { x | ∃ y1, ... , yn : < x , yk > ∈ (DPEk)DP for each 1 ≤ kn and < y1 , ... , yn > ∈ (DR)DT }
AllValuesFrom( DPE1 ... DPEn DR ) { x | ∀ y1, ... , yn : < x , yk > ∈ (DPEk)DP for each 1 ≤ kn imply < y1 , ... , yn > ∈ (DR)DT }
HasValue( DPE ct ) { x | < x , (ct)CT > ∈ (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.4 Models

An interpretation Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ CT ) is called a model of an axiom (resp. ontology) if the axiom (resp. ontology) is satisfied in Int according to the following definitions.

2.4.1 Class Expression Axioms

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

Table 5. Satisfaction of Class Expression Axioms in Int
Axiom Condition
SubClassOf( CE1 CE2 ) (CE1)C(CE2)C
EquivalentClasses( CE1 ... CEn ) (CEj)C = (CEk)C for each 1 ≤ jn and each 1 ≤ kn
DisjointClasses( CE1 ... CEn ) (CEj)C(CEk)C = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
DisjointUnion( C CE1 ... CEn ) CC = (CE1)C ∪ ... ∪ (CEn)C and
(CEj)C(CEk)C = ∅ for each 1 ≤ jn and each 1 ≤ kn such that j

2.4.2 Object Property Expression Axioms

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

Table 6. Satisfaction of Object Property Expression Axioms in Int
Axiom Condition
SubPropertyOf( OPE1 OPE2 ) (OPE1)OP(OPE2)OP
SubPropertyOf( PropertyChain( OPE1 ... OPEn ) OPE ) y0 , ... , yn : < y0 , y1 > ∈ (OPE1)OP and ... and < yn-1 , yn > ∈ (OPEn)OP imply < y0 , yn > ∈ (OPE)OP
EquivalentProperties( OPE1 ... OPEn ) (OPEj)OP = (OPEk)OP for each 1 ≤ jn and each 1 ≤ kn
DisjointProperties( OPE1 ... OPEn ) (OPEj)OP(OPEk)OP = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
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( OPE1 OPE2 ) (OPE1)OP = { < x , y > | < y , x > ∈ (OPE2)OP }
FunctionalProperty( OPE ) x , y1 , y2 : < x , y1 > ∈ (OPE)OP and < x , y2 > ∈ (OPE)OP imply y1 = y2
InverseFunctionalProperty( OPE ) x1 , x2 , y : < x1 , y > ∈ (OPE)OP and < x2 , y > ∈ (OPE)OP imply x1 = x2
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.4.3 Data Property Expression Axioms

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

Table 7. Satisfaction of Data Property Expression Axioms in an Interpretation
Axiom Condition
SubPropertyOf( DPE1 DPE2 ) (DPE1)DP(DPE2)DP
EquivalentProperties( DPE1 ... DPEn ) (DPEj)DP = (DPEk)DP for each 1 ≤ jn and each 1 ≤ kn
DisjointProperties( DPE1 ... DPEn ) (DPEj)DP(DPEk)DP = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
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 , y1 , y2 : < x , y1 > ∈ (DPE)DP and < x , y2 > ∈ (DPE)DP imply y1 = y2

2.4.4 Assertions

Satisfaction of OWL 2 assertions in Int is defined as shown in Table 8.

Table 8. Satisfaction of Assertions in Int
Axiom Condition
SameIndividual( a1 ... an ) (aj)I = (ak)I for each 1 ≤ jn and each 1 ≤ kn
DifferentIndividuals( a1 ... an ) (aj)I(ak)I for each 1 ≤ jn and each 1 ≤ kn such that jk
ClassAssertion( CE a ) aI(CE)C
PropertyAssertion( OPE a1 a2 ) < (a1)I , (a2)I > ∈ (OPE)OP
NegativePropertyAssertion( OPE a1 a2 ) < (a1)I , (a2)I > ∉ (OPE)OP
PropertyAssertion( DPE a ct ) < aI , (ct)CT > ∈ (DPE)DP
NegativePropertyAssertion( DPE a ct ) < aI , (ct)CT > ∉ (DPE)DP

2.4.5 Ontologies

Int is a model of an OWL 2 ontology O if it is a model of all the axioms in the axiom closure of O. (Note that anonymous individuals must be properly renamed apart, as described in Section 4.6.2 of the OWL 2 Specification [OWL 2 Specification].)

2.5 Inference Problems

Let O and O' be OWL 2 ontologies, CE, CE1, and CE2 class expressions, and a a named individual.

  • O is satisfiable (or consistent) if a model of O exists.
  • O entails O' if every model of O is also a model of O'.
  • O and O' are equivalent if O entails O' and O' entails O.
  • O and O' are equisatisfiable if O is satisfiable if and only if O' is satisfiable.
  • CE is satisfiable w.r.t. O if a model Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ CT ) of O exists such that (CE)C ≠ ∅.
  • CE1 is a subclass of CE2 w.r.t. O if (CE1)C(CE2)C for each model Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ CT ) of O.
  • a is an instance of CE w.r.t. O if aICCE for each model Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ CT ) of O.

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 is made precise by the following theorem.

Theorem 1. Let O1 and O2 be OWL 2 ontologies, D = ( NDT , NCT , ⋅ DT , ⋅ CT ) a datatype map such that each datatype mentioned in O1 and O2 occurs in NDT, and D' = ( NDT' , NCT' , ⋅ DT' , ⋅ CT' ) a datatype map such that NDTNDT', NCTNCT', and ⋅ DT' and ⋅ CT' are extensions of ⋅ DT and ⋅ CT. Then, O1 entails O2 w.r.t. D if an only if O1 entails O2 w.r.t. D'.

Proof. The theorem is proved by showing the contrapositive: an interpretation Int w.r.t. D exists such that O1 is and O2 is not satisfied in Int if and only if an interpretation Int' w.r.t. D' exists such that O1 is and O2 is not satisfied in Int'. The (⇐) direction is trivial since each interpretation Int w.r.t. D' is also an interpretation w.r.t. D. For the (⇒) direction, assume that an interpretation Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ CT ) w.r.t. D exists such that O1 is and O2 is not satisfied in Int. Let Int' = ( ΔInt , ΔD' , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ CT ) be an interpretation where all the components are the same as in Int apart from ΔD', which is defined obtained by extending ΔD with the value space of all datatypes in NDT' \ NDT. Clearly, ComplementOf( DT )DTComplementOf( DT )DT' for each datatype DTNDT. The interpretation of data properties is the same in ΔInt and ΔInt', so (CE)CE = (CE)CE' for each class expression CE occurring in O1 and O2. Therefore, O1 is and O2 is not satisfied in Int'. QED

This theorem allows OWL 2 implementations to interpret each OWL 2 ontology O by considering only the datatypes explicitly occurring in O. Furthermore, it shows that tools can support datatypes not explicitly mentioned in this specification without fear that this will change the semantics of OWL 2 ontologies that do not use these datatypes.

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 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.
[XML Schema Datatypes]
XML Schema Part 2: Datatypes Second Edition. Paul V. Biron and Ashok Malhotra, eds. W3C Recommendation 28 October 2004.
[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).