Difference between revisions of "Direct Semantics"
(→Datatype Maps) |
(→Interpretations) |
||
(4 intermediate revisions by one user not shown) | |||
Line 86: | Line 86: | ||
* ''⋅ <sup>C</sup>'' is the ''class interpretation'' function that assigns to each class ''C ∈ N<sub>C</sub>'' \ { ''owl:Thing'' , ''owl:Nothing'' } a subset ''C<sup>C</sup>'' ⊆ ''Δ<sub>Int</sub>''. | * ''⋅ <sup>C</sup>'' is the ''class interpretation'' function that assigns to each class ''C ∈ N<sub>C</sub>'' \ { ''owl:Thing'' , ''owl:Nothing'' } a subset ''C<sup>C</sup>'' ⊆ ''Δ<sub>Int</sub>''. | ||
− | * ''⋅ <sup>OP</sup>'' is the ''object property interpretation'' function that assigns to each object property ''OP ∈ N<sub>OP</sub>'' a subset ''(OP)<sup>OP</sup>'' ⊆ ''Δ<sub>Int</sub>'' × ''Δ<sub>Int</sub>''. | + | * ''⋅ <sup>OP</sup>'' is the ''object property interpretation'' function that assigns to each object property ''OP ∈ N<sub>OP</sub>'' \ { ''owl:TopObjectProperty'' , ''owl:BottomObjectProperty'' } a subset ''(OP)<sup>OP</sup>'' ⊆ ''Δ<sub>Int</sub>'' × ''Δ<sub>Int</sub>''. |
− | * ''⋅ <sup>DP</sup>'' is the ''data property interpretation'' function that assigns to each data property ''DP ∈ N<sub>DP</sub>'' a subset ''(DP)<sup>DP</sup>'' ⊆ ''Δ<sub>Int</sub>'' × ''Δ<sub>D</sub>''. | + | * ''⋅ <sup>DP</sup>'' is the ''data property interpretation'' function that assigns to each data property ''DP ∈ N<sub>DP</sub>'' \ { ''owl:TopDataProperty'' , ''owl:BottomDataProperty'' } a subset ''(DP)<sup>DP</sup>'' ⊆ ''Δ<sub>Int</sub>'' × ''Δ<sub>D</sub>''. |
* ''⋅ <sup>I</sup>'' is the ''individual interpretation'' function that assigns to each individual ''a ∈ N<sub>I</sub>'' an element ''a<sup>I</sup>'' ∈ ''Δ<sub>Int</sub>''. | * ''⋅ <sup>I</sup>'' is the ''individual interpretation'' function that assigns to each individual ''a ∈ N<sub>I</sub>'' an element ''a<sup>I</sup>'' ∈ ''Δ<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'' | ||
+ | | ''Δ<sub>Int</sub>'' × ''Δ<sub>Int</sub>'' | ||
+ | |- | ||
+ | | class="name" | ''owl:BottomObjectProperty'' | ||
+ | | ∅ | ||
+ | |- | ||
| class="name" | InverseOf( OP ) | | class="name" | InverseOf( OP ) | ||
| { < ''x'' , ''y'' > <nowiki>|</nowiki> < ''y'' , ''x'' > ∈ ''(OP)<sup>OP</sup>'' } | | { < ''x'' , ''y'' > <nowiki>|</nowiki> < ''y'' , ''x'' > ∈ ''(OP)<sup>OP</sup>'' } | ||
+ | |- | ||
+ | |} | ||
+ | </div> | ||
+ | |||
+ | ==== Data Property Expressions ==== | ||
+ | |||
+ | The data property interpretation function ''⋅ <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'' | ||
+ | | ''Δ<sub>Int</sub>'' × ''Δ<sub>D</sub>'' | ||
+ | |- | ||
+ | | class="name" | ''owl:BottomDataProperty'' | ||
+ | | ∅ | ||
+ | |- | ||
|} | |} | ||
</div> | </div> | ||
Line 114: | Line 141: | ||
==== Data Range Expressions ==== | ==== Data Range Expressions ==== | ||
− | The datatype interpretation function ''⋅ <sup>DT</sup>'' is extended to data ranges as shown in Table | + | The datatype interpretation function ''⋅ <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 | + | |+ <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 ''⋅ <sup>C</sup>'' is extended to class expressions as shown in Table | + | The class interpretation function ''⋅ <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 | + | |+ <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 | + | 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 | + | |+ <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 | + | 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 | + | |+ <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 | + | 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 | + | |+ <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 | + | 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 | + | |+ <span class="caption">Table 8.</span> Satisfaction of Assertions in ''Int'' |
|- | |- | ||
! Axiom | ! Axiom |
Revision as of 16:19, 16 June 2008
__NUMBEREDHEADINGS__
- 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.
Contents
1 Introduction
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 = ( N_{DT} , N_{CT} , ⋅ ^{DT} , ⋅ ^{CT} ) that defines the set of supported datatypes and their interpretation.
- N_{DT} 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.
- N_{CT} is a function that assigns to each datatype DT ∈ N_{DT} a set of constants N_{CT}(DT); this set is sometimes also called a lexical space of DT; furthermore, N_{CT}(rdfs:Literal) = ∅. The set of all constants for all datatypes is given as the set N_{CT} (whether N_{CT} 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 DT ∈ N_{DT} \ { rdfs:Literal }, the function ⋅ ^{DT} assigns to DT an n-ary relation (DT)^{DT} called a value space.
- For each unary datatype DT ∈ N_{DT} \ { rdfs:Literal } and each constant ct ∈ N_{CT}(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 = ( N_{DT} , N_{CT} , ⋅ ^{DT} , ⋅ ^{CT} ), a vocabulary (or signature) V = ( N_{C} , N_{OP} , N_{DP} , N_{I} , N_{DT} , N_{CT} ) over D is a 6-tuple consisting of the following elements:
- N_{C} is a set of classes as defined in OWL 2 Specification [OWL 2 Specification], containing at least the classes owl:Thing and owl:Nothing.
- N_{OP} is a set of object properties as defined in OWL 2 Specification [OWL 2 Specification].
- N_{DP} is a set of data properties as defined in OWL 2 Specification [OWL 2 Specification].
- N_{I} is a set of individuals as defined in OWL 2 Specification [OWL 2 Specification].
- N_{DT} is the set of all datatypes of D.
- N_{CT} 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 DT ∈ N_{DT} 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 ∈ N_{C} \ { owl:Thing , owl:Nothing } a subset C^{C} ⊆ Δ_{Int}.
- ⋅ ^{OP} is the object property interpretation function that assigns to each object property OP ∈ N_{OP} \ { owl:TopObjectProperty , owl:BottomObjectProperty } a subset (OP)^{OP} ⊆ Δ_{Int} × Δ_{Int}.
- ⋅ ^{DP} is the data property interpretation function that assigns to each data property DP ∈ N_{DP} \ { owl:TopDataProperty , owl:BottomDataProperty } a subset (DP)^{DP} ⊆ Δ_{Int} × Δ_{D}.
- ⋅ ^{I} is the individual interpretation function that assigns to each individual a ∈ N_{I} an element a^{I} ∈ Δ_{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.
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.
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.
Data Range DR | Interpretation (DR)^{DT} |
---|---|
rdfs:Literal | Δ_{D} |
OneOf( ct_{1} ... ct_{n} ) | { (ct_{1})^{CT} , ... , (ct_{n})^{CT} } |
ComplementOf( DR ) | (Δ_{D})^{n} \ (DR)^{DT} where n is the arity of DR |
DatatypeRestriction( DT f_{1} v_{1} ... f_{n} v_{n} ) |
the subset of (DT)^{DT} obtained by applying to it |
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.
Class Expression CE | Interpretation (CE)^{C} |
---|---|
owl:Thing | Δ_{Int} |
owl:Nothing | ∅ |
ComplementOf( CE ) | Δ_{Int} \ (CE)^{C} |
IntersectionOf( CE_{1} ... CE_{n} ) | (CE_{1})^{C} ∩ ... ∩ (CE_{n})^{C} |
UnionOf( CE_{1} ... CE_{n} ) | (CE_{1})^{C} ∪ ... ∪ (CE_{n})^{C} |
OneOf( a_{1} ... a_{n} ) | { (a_{1})^{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_{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} } |
AllValuesFrom( 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} } |
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.
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 ≠ |
2.4.2 Object Property Expression Axioms
Satisfaction of OWL 2 object property expression axioms in Int 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_{1})^{OP} and ... and < y_{n-1} , y_{n} > ∈ (OPE_{n})^{OP} imply < y_{0} , y_{n} > ∈ (OPE)^{OP} |
EquivalentProperties( OPE_{1} ... OPE_{n} ) | (OPE_{j})^{OP} = (OPE_{k})^{OP} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointProperties( OPE_{1} ... 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_{1} OPE_{2} ) | (OPE_{1})^{OP} = { < x , y > | < y , x > ∈ (OPE_{2})^{OP} } |
FunctionalProperty( OPE ) | ∀ x , y_{1} , y_{2} : < x , y_{1} > ∈ (OPE)^{OP} and < x , y_{2} > ∈ (OPE)^{OP} imply y_{1} = y_{2} |
InverseFunctionalProperty( OPE ) | ∀ x_{1} , x_{2} , y : < x_{1} , y > ∈ (OPE)^{OP} and < x_{2} , y > ∈ (OPE)^{OP} imply x_{1} = x_{2} |
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.
Axiom | Condition |
---|---|
SubPropertyOf( DPE_{1} DPE_{2} ) | (DPE_{1})^{DP} ⊆ (DPE_{2})^{DP} |
EquivalentProperties( DPE_{1} ... DPE_{n} ) | (DPE_{j})^{DP} = (DPE_{k})^{DP} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointProperties( DPE_{1} ... 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_{1} , y_{2} : < x , y_{1} > ∈ (DPE)^{DP} and < x , y_{2} > ∈ (DPE)^{DP} imply y_{1} = y_{2} |
2.4.4 Assertions
Satisfaction of OWL 2 assertions in Int is defined as shown in Table 8.
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} |
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 ct ) | < a^{I} , (ct)^{CT} > ∈ (DPE)^{DP} |
NegativePropertyAssertion( DPE a ct ) | < a^{I} , (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, CE_{1}, and CE_{2} 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} ≠ ∅.
- CE_{1} is a subclass of CE_{2} w.r.t. O if (CE_{1})^{C} ⊆ (CE_{2})^{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 a^{I} ∈ C^{CE} 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 O_{1} and O_{2} be OWL 2 ontologies, D = ( N_{DT} , N_{CT} , ⋅ ^{DT} , ⋅ ^{CT} ) a datatype map such that each datatype mentioned in O_{1} and O_{2} occurs in N_{DT}, and D' = ( N_{DT}' , N_{CT}' , ⋅ ^{DT}' , ⋅ ^{CT}' ) a datatype map such that N_{DT} ⊆ N_{DT}', N_{CT} ⊆ N_{CT}', and ⋅ ^{DT}' and ⋅ ^{CT}' are extensions of ⋅ ^{DT} and ⋅ ^{CT}. Then, O_{1} entails O_{2} w.r.t. D if an only if O_{1} entails O_{2} w.r.t. D'.
Proof. The theorem is proved by showing the contrapositive: an interpretation Int w.r.t. D exists such that O_{1} is and O_{2} is not satisfied in Int if and only if an interpretation Int' w.r.t. D' exists such that O_{1} is and O_{2} 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 O_{1} is and O_{2} 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 N_{DT}' \ N_{DT}. Clearly, ComplementOf( DT )^{DT} ⊆ ComplementOf( DT )^{DT}' for each datatype DT ∈ N_{DT}. The interpretation of data properties is the same in Δ_{Int} and Δ_{Int}', so (CE)^{CE} = (CE)^{CE}' for each class expression CE occurring in O_{1} and O_{2}. Therefore, O_{1} is and O_{2} 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).