Difference between revisions of "Direct Semantics"

From OWL
Jump to: navigation, search
(Model-Theoretic Semantics for OWL 2)
(Data Range Expressions)
(3 intermediate revisions by one user not shown)
Line 40: Line 40:
 
=== Datatype Maps ===
 
=== Datatype Maps ===
  
A ''datatype map'' is a 4-tuple ''D'' = ( ''N<sub>DT</sub>'' , ''N<sub>CT</sub>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ) that defines the set of supported datatypes and their interpretation.
+
A ''datatype map'' is a 4-tuple ''D'' = ( ''N<sub>DT</sub>'' , ''N<sub>LT</sub>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ) that defines the set of supported datatypes and their interpretation.
  
 
* ''N<sub>DT</sub>'' is a set of datatypes as defined in the OWL 2 Specification [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>], each associated with a positive integer arity, containing at least the unary datatype ''rdfs:Literal''.
 
* ''N<sub>DT</sub>'' is a set of datatypes as defined in the OWL 2 Specification [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>], each associated with a positive integer arity, containing at least the unary datatype ''rdfs:Literal''.
* ''N<sub>CT</sub>'' is a function that assigns to each datatype ''DT'' &isin; ''N<sub>DT</sub>'' a set of ''constants'' ''N<sub>CT</sub>(DT)''; this set is sometimes also called a ''lexical space'' of ''DT''; furthermore, ''N<sub>CT</sub>(rdfs:Literal)'' = &empty;. The set of all constants for all datatypes is given as the set ''N<sub>CT</sub>'' (whether ''N<sub>CT</sub>'' is used as a function or as a set of all constants is expected to be clear from the context).
+
* ''N<sub>LT</sub>'' is a function that assigns to each datatype ''DT'' &isin; ''N<sub>DT</sub>'' a set of ''literals'' ''N<sub>LT</sub>(DT)''; this set is sometimes also called a ''lexical space'' of ''DT''; furthermore, ''N<sub>LT</sub>(rdfs:Literal)'' = &empty;. The set of all literals for all datatypes is given as the set ''N<sub>LT</sub>'' (whether ''N<sub>LT</sub>'' is used as a function or as a set of all literals is expected to be clear from the context).
 
* For each ''n''-ary datatype ''DT'' &isin; ''N<sub>DT</sub>'' \ { rdfs:Literal }, the function ''&sdot;&nbsp;<sup>DT</sup>'' assigns to ''DT'' an ''n''-ary relation ''(DT)<sup>DT</sup>'' called a ''value space''.
 
* For each ''n''-ary datatype ''DT'' &isin; ''N<sub>DT</sub>'' \ { rdfs:Literal }, the function ''&sdot;&nbsp;<sup>DT</sup>'' assigns to ''DT'' an ''n''-ary relation ''(DT)<sup>DT</sup>'' called a ''value space''.
* For each unary datatype ''DT'' &isin; ''N<sub>DT</sub>'' \ { rdfs:Literal } and each constant ''ct &isin; N<sub>CT</sub>(DT)'', the function ''&sdot;&nbsp;<sup>CT</sup>'' assigns to ''ct'' a ''data value'' ''(ct)<sup>CT</sup>'' &isin; ''(DT)<sup>DT</sup>''.
+
* For each unary datatype ''DT'' &isin; ''N<sub>DT</sub>'' \ { rdfs:Literal } and each literal ''lt &isin; N<sub>LT</sub>(DT)'', the function ''&sdot;&nbsp;<sup>LT</sup>'' assigns to ''lt'' a ''data value'' ''(lt)<sup>LT</sup>'' &isin; ''(DT)<sup>DT</sup>''.
  
The value spaces of the XML Schema Datatypes and the mappings of their constants to data values is defined as in XML Schema Datatypes [<cite>[[#ref-xml-schema-datatypes|XML Schema Datatypes]]</cite>]. The value space for ''owl:internationalizedString'' consists of all pairs <span class="name">&lt;"''text''",''languageTag''&gt;</span>, where <span class="name">"''text''"</span> is a string and <span class="name">''languageTag''</span> is a language tag.
+
The value spaces of the XML Schema Datatypes and the mappings of their literals to data values is defined as in XML Schema Datatypes [<cite>[[#ref-xml-schema-datatypes|XML Schema Datatypes]]</cite>]. The value space for ''owl:internationalizedString'' consists of all pairs <span class="name">&lt;"''text''",''languageTag''&gt;</span>, where <span class="name">"''text''"</span> is a string and <span class="name">''languageTag''</span> is a language tag.
  
 
=== Vocabulary ===
 
=== Vocabulary ===
  
Given a datatype map ''D'' = ( ''N<sub>DT</sub>'' , ''N<sub>CT</sub>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ), a ''vocabulary'' (or ''signature'') ''V = ( N<sub>C</sub> , N<sub>OP</sub> , N<sub>DP</sub> , N<sub>I</sub> , N<sub>DT</sub> , N<sub>CT</sub> )'' over ''D'' is a 6-tuple consisting of the following elements:
+
Given a datatype map ''D'' = ( ''N<sub>DT</sub>'' , ''N<sub>LT</sub>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ), a ''vocabulary'' (or ''signature'') ''V = ( N<sub>C</sub> , N<sub>OP</sub> , N<sub>DP</sub> , N<sub>I</sub> , N<sub>DT</sub> , N<sub>LT</sub> )'' over ''D'' is a 6-tuple consisting of the following elements:
  
 
* ''N<sub>C</sub>'' is a set of ''classes'' as defined in OWL 2 Specification [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>], containing at least the classes ''owl:Thing'' and ''owl:Nothing''.
 
* ''N<sub>C</sub>'' is a set of ''classes'' as defined in OWL 2 Specification [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>], containing at least the classes ''owl:Thing'' and ''owl:Nothing''.
Line 58: Line 58:
 
* ''N<sub>I</sub>'' is a set of ''individuals'' as defined in OWL 2 Specification [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>].
 
* ''N<sub>I</sub>'' is a set of ''individuals'' as defined in OWL 2 Specification [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>].
 
* ''N<sub>DT</sub>'' is the set of all datatypes of ''D''.
 
* ''N<sub>DT</sub>'' is the set of all datatypes of ''D''.
* ''N<sub>CT</sub>'' is a set of all constants of ''D''.
+
* ''N<sub>LT</sub>'' is a set of all literals of ''D''.
  
 
Given a vocabulary ''V'', the following conventions are used in this document to denote different syntactic parts of OWL 2 ontologies:
 
Given a vocabulary ''V'', the following conventions are used in this document to denote different syntactic parts of OWL 2 ontologies:
Line 71: Line 71:
 
* <span class="name">DR</span> denotes a data range;
 
* <span class="name">DR</span> denotes a data range;
 
* <span class="name">a</span> denotes an individual; and
 
* <span class="name">a</span> denotes an individual; and
* <span class="name">ct</span> denotes a constant.
+
* <span class="name">lt</span> denotes a literal.
  
 
=== Interpretations ===
 
=== Interpretations ===
  
Given a datatype map ''D'' and a vocabulary ''V'' over ''D'', an ''interpretation'' ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ) is a 8-tuple with the following structure.
+
Given a datatype map ''D'' and a vocabulary ''V'' over ''D'', an ''interpretation'' ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ) is a 8-tuple with the following structure.
  
 
* ''&Delta;<sub>Int</sub>'' is a nonempty set called the ''object domain''.
 
* ''&Delta;<sub>Int</sub>'' is a nonempty set called the ''object domain''.
Line 83: Line 83:
 
* ''&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>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>''.
* ''&sdot;&nbsp;<sup>DT</sup>'' and ''&sdot;&nbsp;<sup>CT</sup>'' are the same as in ''D''.
+
* ''&sdot;&nbsp;<sup>DT</sup>'' and ''&sdot;&nbsp;<sup>LT</sup>'' are the same as in ''D''.
  
 
The following sections define the extensions of ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , and ''&sdot;&nbsp;<sup>C</sup>'' 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 ''&sdot;&nbsp;<sup>DP</sup>'' to data property expressions.
 
The following sections define the extensions of ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , and ''&sdot;&nbsp;<sup>C</sup>'' 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 ''&sdot;&nbsp;<sup>DP</sup>'' to data property expressions.
Line 144: Line 144:
 
| ''&Delta;<sub>D</sub>''
 
| ''&Delta;<sub>D</sub>''
 
|-
 
|-
| class="name" | OneOf( ct<sub>1</sub> ... ct<sub>n</sub> )
+
| class="name" | OneOf( lt<sub>1</sub> ... lt<sub>n</sub> )
| { ''(ct<sub>1</sub>)<sup>CT</sup>'' , ... , ''(ct<sub>n</sub>)<sup>CT</sup>'' }
+
| { ''(lt<sub>1</sub>)<sup>LT</sup>'' , ... , ''(lt<sub>n</sub>)<sup>LT</sup>'' }
 
|-
 
|-
 
| class="name" | ComplementOf( DR )
 
| class="name" | ComplementOf( DR )
 
| ''(&Delta;<sub>D</sub>)<sup>n</sup>'' \ ''(DR)<sup>DT</sup>'' where ''n'' is the arity of ''DR''
 
| ''(&Delta;<sub>D</sub>)<sup>n</sup>'' \ ''(DR)<sup>DT</sup>'' where ''n'' is the arity of ''DR''
 
|-
 
|-
| class="name" | DatatypeRestriction( DT f<sub>1</sub> v<sub>1</sub> ... f<sub>n</sub> v<sub>n</sub> )
+
| class="name" | DatatypeRestriction( DT f<sub>1</sub> lt<sub>1</sub> ... f<sub>n</sub> lt<sub>n</sub> )
 
|
 
|
 
the subset of ''(DT)<sup>DT</sup>'' obtained by applying to it<br />
 
the subset of ''(DT)<sup>DT</sup>'' obtained by applying to it<br />
the facets ''f<sub>1</sub>'' to ''f<sub>n</sub>'' with values ''v<sub>1</sub>'' to ''v<sub>n</sub>'', respectively,<br />
+
the facets ''f<sub>1</sub>'' to ''f<sub>n</sub>'' with values ''lt<sub>1</sub>'' to ''lt<sub>n</sub>'', respectively,<br />
as specified by the definition of facets in XML Schema Datatypes [<cite>[[#ref-xml-schema-datatypes|XML Schema Datatypes]]</cite>]
+
as specified by the definition of facets in<br /> OWL 2 Specification [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>]
 
|}
 
|}
 
</div>
 
</div>
Line 223: Line 223:
 
| { ''x'' <nowiki>|</nowiki> &forall; ''y<sub>1</sub>'', ... , ''y<sub>n</sub>'' : &lt; ''x'' , ''y<sub>k</sub>'' &gt; &isin; ''(DPE<sub>k</sub>)<sup>DP</sup>'' for each 1 &le; ''k'' &le; ''n'' imply &lt; ''y<sub>1</sub>'' , ... , ''y<sub>n</sub>'' &gt; &isin; ''(DR)<sup>DT</sup>'' }
 
| { ''x'' <nowiki>|</nowiki> &forall; ''y<sub>1</sub>'', ... , ''y<sub>n</sub>'' : &lt; ''x'' , ''y<sub>k</sub>'' &gt; &isin; ''(DPE<sub>k</sub>)<sup>DP</sup>'' for each 1 &le; ''k'' &le; ''n'' imply &lt; ''y<sub>1</sub>'' , ... , ''y<sub>n</sub>'' &gt; &isin; ''(DR)<sup>DT</sup>'' }
 
|-
 
|-
| class="name" | HasValue( DPE ct )
+
| class="name" | HasValue( DPE lt )
| { ''x'' <nowiki>|</nowiki> &lt; ''x'' , ''(ct)<sup>CT</sup>'' &gt; &isin; ''(DPE)<sup>DP</sup>'' }
+
| { ''x'' <nowiki>|</nowiki> &lt; ''x'' , ''(lt)<sup>LT</sup>'' &gt; &isin; ''(DPE)<sup>DP</sup>'' }
 
|-
 
|-
 
| class="name" | MinCardinality( n DPE )
 
| class="name" | MinCardinality( n DPE )
Line 248: Line 248:
 
=== Models ===
 
=== Models ===
  
An interpretation ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ) is called a ''model of an axiom w.r.t. ontology'' ''O'' if the axiom is satisfied in ''Int'' according to the following definitions. The function ''ISNAMED'' is defined for each ''&alpha;'' &isin; ''&Delta;<sub>Int</sub>'' such that ''ISNAMED(&alpha;)'' = ''true'' if and only if an individual ''a'' exists such that it occurs in the axiom closure of ''O'' and ''a<sup>I</sup>'' = ''&alpha;''.
+
An interpretation ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ) is called a ''model of an axiom w.r.t. ontology'' ''O'' if the axiom is satisfied in ''Int'' according to the following definitions. The function ''ISNAMED'' is defined for each ''&alpha;'' &isin; ''&Delta;<sub>Int</sub>'' such that ''ISNAMED(&alpha;)'' = ''true'' if and only if an individual ''a'' exists such that it occurs in the axiom closure of ''O'' and ''a<sup>I</sup>'' = ''&alpha;''.
  
 
==== Class Expression Axioms ====
 
==== Class Expression Axioms ====
Line 407: Line 407:
 
| &lt; ''(a<sub>1</sub>)<sup>I</sup>'' , ''(a<sub>2</sub>)<sup>I</sup>'' &gt; &notin; ''(OPE)<sup>OP</sup>''
 
| &lt; ''(a<sub>1</sub>)<sup>I</sup>'' , ''(a<sub>2</sub>)<sup>I</sup>'' &gt; &notin; ''(OPE)<sup>OP</sup>''
 
|-
 
|-
| class="name" | PropertyAssertion( DPE a ct )
+
| class="name" | PropertyAssertion( DPE a lt )
| &lt; ''a<sup>I</sup>'' , ''(ct)<sup>CT</sup>'' &gt; &isin; ''(DPE)<sup>DP</sup>''
+
| &lt; ''a<sup>I</sup>'' , ''(lt)<sup>LT</sup>'' &gt; &isin; ''(DPE)<sup>DP</sup>''
 
|-
 
|-
| class="name" | NegativePropertyAssertion( DPE a ct )
+
| class="name" | NegativePropertyAssertion( DPE a lt )
| &lt; ''a<sup>I</sup>'' , ''(ct)<sup>CT</sup>'' &gt; &notin; ''(DPE)<sup>DP</sup>''
+
| &lt; ''a<sup>I</sup>'' , ''(lt)<sup>LT</sup>'' &gt; &notin; ''(DPE)<sup>DP</sup>''
 
|-
 
|-
 
|}
 
|}
Line 428: Line 428:
 
* ''O'' and ''O<nowiki>'</nowiki>'' are ''equivalent'' if ''O'' entails ''O<nowiki>'</nowiki>'' and ''O<nowiki>'</nowiki>'' entails ''O''.
 
* ''O'' and ''O<nowiki>'</nowiki>'' are ''equivalent'' if ''O'' entails ''O<nowiki>'</nowiki>'' and ''O<nowiki>'</nowiki>'' entails ''O''.
 
* ''O'' and ''O<nowiki>'</nowiki>'' are ''equisatisfiable'' if ''O'' is satisfiable if and only if ''O<nowiki>'</nowiki>'' is satisfiable.
 
* ''O'' and ''O<nowiki>'</nowiki>'' are ''equisatisfiable'' if ''O'' is satisfiable if and only if ''O<nowiki>'</nowiki>'' is satisfiable.
* ''CE'' is satisfiable w.r.t. ''O'' if a model ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ) of ''O'' exists such that ''(CE)<sup>C</sup>'' &ne; &empty;.
+
* ''CE'' is satisfiable w.r.t. ''O'' if a model ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ) of ''O'' exists such that ''(CE)<sup>C</sup>'' &ne; &empty;.
* ''CE<sub>1</sub>'' is a ''subclass'' of ''CE<sub>2</sub>'' w.r.t. ''O'' if ''(CE<sub>1</sub>)<sup>C</sup>'' &sube; ''(CE<sub>2</sub>)<sup>C</sup>'' for each model ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ) of ''O''.
+
* ''CE<sub>1</sub>'' is a ''subclass'' of ''CE<sub>2</sub>'' w.r.t. ''O'' if ''(CE<sub>1</sub>)<sup>C</sup>'' &sube; ''(CE<sub>2</sub>)<sup>C</sup>'' for each model ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ) of ''O''.
* ''a'' is an ''instance'' of ''CE'' w.r.t. ''O'' if ''a<sup>I</sup>'' &isin; ''C<sup>CE</sup>'' for each model ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ) of ''O''.
+
* ''a'' is an ''instance'' of ''CE'' w.r.t. ''O'' if ''a<sup>I</sup>'' &isin; ''C<sup>CE</sup>'' for each model ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ) of ''O''.
  
 
== Independence of the Semantics from the Datatype Map ==
 
== Independence of the Semantics from the Datatype Map ==
Line 436: Line 436:
 
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.
 
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<sub>1</sub>'' and ''O<sub>2</sub>'' be OWL 2 ontologies, ''D'' = ( ''N<sub>DT</sub>'' , ''N<sub>CT</sub>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ) a datatype map such that each datatype mentioned in ''O<sub>1</sub>'' and ''O<sub>2</sub>'' occurs in ''N<sub>DT</sub>'', and ''D<nowiki>'</nowiki>'' = ( ''N<sub>DT</sub><nowiki>'</nowiki>'' , ''N<sub>CT</sub><nowiki>'</nowiki>'' , ''&sdot;&nbsp;<sup>DT</sup><nowiki>'</nowiki>'' , ''&sdot;&nbsp;<sup>CT</sup><nowiki>'</nowiki>'' ) a datatype map such that ''N<sub>DT</sub>'' &sube; ''N<sub>DT</sub><nowiki>'</nowiki>'', ''N<sub>CT</sub>'' &sube; ''N<sub>CT</sub><nowiki>'</nowiki>'', and ''&sdot;&nbsp;<sup>DT</sup><nowiki>'</nowiki>'' and ''&sdot;&nbsp;<sup>CT</sup><nowiki>'</nowiki>'' are extensions of ''&sdot;&nbsp;<sup>DT</sup>'' and ''&sdot;&nbsp;<sup>CT</sup>''. Then, ''O<sub>1</sub>'' entails ''O<sub>2</sub>'' w.r.t. ''D'' if an only if ''O<sub>1</sub>'' entails ''O<sub>2</sub>'' w.r.t. ''D<nowiki>'</nowiki>''.
+
'''Theorem 1.''' Let ''O<sub>1</sub>'' and ''O<sub>2</sub>'' be OWL 2 ontologies, ''D'' = ( ''N<sub>DT</sub>'' , ''N<sub>LT</sub>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ) a datatype map such that each datatype mentioned in ''O<sub>1</sub>'' and ''O<sub>2</sub>'' occurs in ''N<sub>DT</sub>'', and ''D<nowiki>'</nowiki>'' = ( ''N<sub>DT</sub><nowiki>'</nowiki>'' , ''N<sub>LT</sub><nowiki>'</nowiki>'' , ''&sdot;&nbsp;<sup>DT</sup><nowiki>'</nowiki>'' , ''&sdot;&nbsp;<sup>LT</sup><nowiki>'</nowiki>'' ) a datatype map such that ''N<sub>DT</sub>'' &sube; ''N<sub>DT</sub><nowiki>'</nowiki>'', ''N<sub>LT</sub>'' &sube; ''N<sub>LT</sub><nowiki>'</nowiki>'', and ''&sdot;&nbsp;<sup>DT</sup><nowiki>'</nowiki>'' and ''&sdot;&nbsp;<sup>LT</sup><nowiki>'</nowiki>'' are extensions of ''&sdot;&nbsp;<sup>DT</sup>'' and ''&sdot;&nbsp;<sup>LT</sup>''. Then, ''O<sub>1</sub>'' entails ''O<sub>2</sub>'' w.r.t. ''D'' if an only if ''O<sub>1</sub>'' entails ''O<sub>2</sub>'' w.r.t. ''D<nowiki>'</nowiki>''.
  
''Proof.'' The theorem is proved by showing the contrapositive: an interpretation ''Int'' w.r.t. ''D'' exists such that ''O<sub>1</sub>'' is and ''O<sub>2</sub>'' is not satisfied in ''Int'' if and only if an interpretation ''Int<nowiki>'</nowiki>'' w.r.t. ''D<nowiki>'</nowiki>'' exists such that ''O<sub>1</sub>'' is and ''O<sub>2</sub>'' is not satisfied in ''Int<nowiki>'</nowiki>''. The (&lArr;) direction is trivial since each interpretation ''Int'' w.r.t. ''D<nowiki>'</nowiki>'' is also an interpretation w.r.t. ''D''. For the (&rArr;) direction, assume that an interpretation ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ) w.r.t. ''D'' exists such that ''O<sub>1</sub>'' is and ''O<sub>2</sub>'' is not satisfied in ''Int''. Let ''Int<nowiki>'</nowiki>'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub><nowiki>'</nowiki>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>CT</sup>'' ) be an interpretation where all the components are the same as in ''Int'' apart from ''&Delta;<sub>D</sub><nowiki>'</nowiki>'', which is defined obtained by extending ''&Delta;<sub>D</sub>'' with the value space of all datatypes in ''N<sub>DT</sub><nowiki>'</nowiki>'' \ ''N<sub>DT</sub>''. Clearly, ''<span class="name">ComplementOf( DT )</span><sup>DT</sup>'' &sube; ''<span class="name">ComplementOf( DT )</span><sup>DT</sup><nowiki>'</nowiki>'' for each datatype ''DT'' &isin; ''N<sub>DT</sub>''. The interpretation of data properties is the same in ''&Delta;<sub>Int</sub>'' and ''&Delta;<sub>Int</sub><nowiki>'</nowiki>'', so ''(CE)<sup>CE</sup>'' = ''(CE)<sup>CE</sup><nowiki>'</nowiki>'' for each class expression ''CE'' occurring in ''O<sub>1</sub>'' and ''O<sub>2</sub>''. Therefore, ''O<sub>1</sub>'' is and ''O<sub>2</sub>'' is not satisfied in ''Int<nowiki>'</nowiki>''. QED
+
''Proof.'' The theorem is proved by showing the contrapositive: an interpretation ''Int'' w.r.t. ''D'' exists such that ''O<sub>1</sub>'' is and ''O<sub>2</sub>'' is not satisfied in ''Int'' if and only if an interpretation ''Int<nowiki>'</nowiki>'' w.r.t. ''D<nowiki>'</nowiki>'' exists such that ''O<sub>1</sub>'' is and ''O<sub>2</sub>'' is not satisfied in ''Int<nowiki>'</nowiki>''. The (&lArr;) direction is trivial since each interpretation ''Int'' w.r.t. ''D<nowiki>'</nowiki>'' is also an interpretation w.r.t. ''D''. For the (&rArr;) direction, assume that an interpretation ''Int'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ) w.r.t. ''D'' exists such that ''O<sub>1</sub>'' is and ''O<sub>2</sub>'' is not satisfied in ''Int''. Let ''Int<nowiki>'</nowiki>'' = ( ''&Delta;<sub>Int</sub>'' , ''&Delta;<sub>D</sub><nowiki>'</nowiki>'' , ''&sdot;&nbsp;<sup>C</sup>'' , ''&sdot;&nbsp;<sup>OP</sup>'' , ''&sdot;&nbsp;<sup>DP</sup>'' , ''&sdot;&nbsp;<sup>I</sup>'' , ''&sdot;&nbsp;<sup>DT</sup>'' , ''&sdot;&nbsp;<sup>LT</sup>'' ) be an interpretation where all the components are the same as in ''Int'' apart from ''&Delta;<sub>D</sub><nowiki>'</nowiki>'', which is defined obtained by extending ''&Delta;<sub>D</sub>'' with the value space of all datatypes in ''N<sub>DT</sub><nowiki>'</nowiki>'' \ ''N<sub>DT</sub>''. Clearly, ''<span class="name">ComplementOf( DT )</span><sup>DT</sup>'' &sube; ''<span class="name">ComplementOf( DT )</span><sup>DT</sup><nowiki>'</nowiki>'' for each datatype ''DT'' &isin; ''N<sub>DT</sub>''. The interpretation of data properties is the same in ''&Delta;<sub>Int</sub>'' and ''&Delta;<sub>Int</sub><nowiki>'</nowiki>'', so ''(CE)<sup>CE</sup>'' = ''(CE)<sup>CE</sup><nowiki>'</nowiki>'' for each class expression ''CE'' occurring in ''O<sub>1</sub>'' and ''O<sub>2</sub>''. Therefore, ''O<sub>1</sub>'' is and ''O<sub>2</sub>'' is not satisfied in ''Int<nowiki>'</nowiki>''. 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.
 
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.

Revision as of 15:42, 3 August 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 , NLT , ⋅ DT , ⋅ LT ) 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.
  • NLT is a function that assigns to each datatype DTNDT a set of literals NLT(DT); this set is sometimes also called a lexical space of DT; furthermore, NLT(rdfs:Literal) = ∅. The set of all literals for all datatypes is given as the set NLT (whether NLT is used as a function or as a set of all literals 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 literal lt ∈ NLT(DT), the function ⋅ LT assigns to lt a data value (lt)LT(DT)DT.

The value spaces of the XML Schema Datatypes and the mappings of their literals 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 , NLT , ⋅ DT , ⋅ LT ), a vocabulary (or signature) V = ( NC , NOP , NDP , NI , NDT , NLT ) 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.
  • NLT is a set of all literals 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
  • lt denotes a literal.

2.3 Interpretations

Given a datatype map D and a vocabulary V over D, an interpretation Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT ) 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 ⋅ LT 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( lt1 ... ltn ) { (lt1)LT , ... , (ltn)LT }
ComplementOf( DR ) D)n \ (DR)DT where n is the arity of DR
DatatypeRestriction( DT f1 lt1 ... fn ltn )

the subset of (DT)DT obtained by applying to it
the facets f1 to fn with values lt1 to ltn, respectively,
as specified by the definition of facets in
OWL 2 Specification [OWL 2 Specification]

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 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.4 Models

An interpretation Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT ) is called a model of an axiom w.r.t. ontology O if the axiom is satisfied in Int according to the following definitions. The function ISNAMED is defined for each αΔInt such that ISNAMED(α) = true if and only if an individual a exists such that it occurs in the axiom closure of O and aI = α.

2.4.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 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 w.r.t. O 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 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( 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 Object and Data Property Expression Axioms

Satisfaction of OWL 2 axioms about both object and data property expressions in Int w.r.t. O is defined as shown in Table 8.

Table 8. Satisfaction of Axioms about Both Object and Data Property Expressions in an Interpretation
Axiom Condition
KeyFor( OPE1 ... OPEm DPE1 ... DPEn CE ) x , y , u1 , ... , um , v1 , ... , vn :
       ISNAMED(x) and ISNAMED(y) and ISNAMED(u1) and ... and ISNAMED(um) and
       x(CE)C and < x , u1 > ∈ (OPE1)OP and ... and < x , um > ∈ (OPEm)OP and < x , v1 > ∈ (DPE1)DP and ... and < x , vn > ∈ (DPEn)DP
       y(CE)C and < y , u1 > ∈ (OPE1)OP and ... and < y , um > ∈ (OPEn)OP and < y , v1 > ∈ (DPE1)DP and ... and < y , vn > ∈ (DPEn)DP
    implies
       x = y

2.4.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 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 lt ) < aI , (lt)LT > ∈ (DPE)DP
NegativePropertyAssertion( DPE a lt ) < aI , (lt)LT > ∉ (DPE)DP

2.4.6 Ontologies

Int is a model of an OWL 2 ontology O if it is a model w.r.t. O for each 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 , ⋅ LT ) 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 , ⋅ LT ) 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 , ⋅ LT ) 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 , NLT , ⋅ DT , ⋅ LT ) a datatype map such that each datatype mentioned in O1 and O2 occurs in NDT, and D' = ( NDT' , NLT' , ⋅ DT' , ⋅ LT' ) a datatype map such that NDTNDT', NLTNLT', and ⋅ DT' and ⋅ LT' are extensions of ⋅ DT and ⋅ LT. 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 , ⋅ LT ) 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 , ⋅ LT ) 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).