Difference between revisions of "Direct Semantics"

From OWL
Jump to: navigation, search
(switch to TR template [using an external editor])
m (more on XML Schema datatypes)
(3 intermediate revisions by one user not shown)
Line 16: Line 16:
  
 
Copyright © 2006-2007 by the Authors. This document is available under the [http://www.w3.org/Consortium/Legal/copyright-documents W3C Document License]. See the [http://www.w3.org/Consortium/Legal/ipr-notice#Copyright W3C Intellectual Rights Notice and Legal Disclaimers] for additional information.
 
Copyright © 2006-2007 by the Authors. This document is available under the [http://www.w3.org/Consortium/Legal/copyright-documents W3C Document License]. See the [http://www.w3.org/Consortium/Legal/ipr-notice#Copyright W3C Intellectual Rights Notice and Legal Disclaimers] for additional information.
 
</div>
 
  
 
__TOC__
 
__TOC__
Line 27: Line 25:
 
OWL 1.1 does not have an RDF-compatible semantics. Ontologies expressed in OWL RDF are given semantics by converting then into the functional-style syntax and interpreting the result as specified in this document.
 
OWL 1.1 does not have an RDF-compatible semantics. Ontologies expressed in OWL RDF are given semantics by converting then into the functional-style syntax and interpreting the result as specified in this document.
  
OWL 1.1 allows for annotations of ontologies and ontology axioms. Annotations, however, have no semantic meaning in OWL 1.1 and are ignored in this document.
+
OWL 1.1 allows for annotations of ontologies and ontology entities (classes, properties, and individuals) and ontology axioms. Annotations, however, have no semantic meaning in OWL 1.1 and are ignored in this document.  Definitions in OWL 1.1 similarly have no semantics.  Constructs only used in annotations and definitions, like <span class="name">ObjectProperty</span>, therefore do not show up in this document.
  
 
Since OWL 1.1 is an extension of OWL DL, this document also provides a formal semantics for OWL Lite and OWL DL and it is equivalent to the definition given in [<cite>[[#ref-owl-abstract-syntax-and-semantics|OWL Abstract Syntax and Semantics]]</cite>].
 
Since OWL 1.1 is an extension of OWL DL, this document also provides a formal semantics for OWL Lite and OWL DL and it is equivalent to the definition given in [<cite>[[#ref-owl-abstract-syntax-and-semantics|OWL Abstract Syntax and Semantics]]</cite>].
Line 50: Line 48:
 
* ''.<sup>D</sup>'' assigns to each datatype ''d ∈ N<sub>D</sub>'' with arity ''n'' an ''n''-ary relation ''d<sup>D</sup>'' over ''Δ<sub>D</sub>''.
 
* ''.<sup>D</sup>'' assigns to each datatype ''d ∈ N<sub>D</sub>'' with arity ''n'' an ''n''-ary relation ''d<sup>D</sup>'' over ''Δ<sub>D</sub>''.
  
The set of datatypes ''N<sub>D</sub>'' in each OWL 1.1 vocabulary must include a unary datatype ''rdfs:Literal'' interpreted as ''Δ<sub>D</sub>''<nowiki>; furthermore, it must also include the following unary datatypes: </nowiki>[http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#string ''xsd:string''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#boolean ''xsd:boolean''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#decimal ''xsd:decimal''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#float ''xsd:float''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#double ''xsd:double''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#dateTime ''xsd:dateTime''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#time ''xsd:time''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#date ''xsd:date''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gYearMonth ''xsd:gYearMonth''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gYear ''xsd:gYear''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gMonthDay ''xsd:gMonthDay''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gDay ''xsd:gDay''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gMonth ''xsd:gMonth''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#hexBinary ''xsd:hexBinary''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#base64Binary ''xsd:base64Binary''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#anyURI ''xsd:anyURI''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#normalizedString ''xsd:normalizedString''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#token ''xsd:token''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#language ''xsd:language''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#NMTOKEN ''xsd:NMTOKEN''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#Name ''xsd:Name''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#NCName ''xsd:NCName''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#integer ''xsd:integer''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#nonPositiveInteger ''xsd:nonPositiveInteger''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#negativeInteger ''xsd:negativeInteger''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#long ''xsd:long''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#int ''xsd:int''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#short ''xsd:short''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#byte ''xsd:byte''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#nonNegativeInteger ''xsd:nonNegativeInteger''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedLong ''xsd:unsignedLong''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedInt ''xsd:unsignedInt''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedShort ''xsd:unsignedShort''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedByte ''xsd:unsignedByte''], and [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#positiveInteger ''xsd:positiveInteger'']. These datatypes, as well as the well-formed constants from ''N<sub>V</sub>'', are interpreted as specified in [<cite>[[#ref-xml-schema-datatypes|XML Schema Datatypes]]</cite>].
+
The set of datatypes ''N<sub>D</sub>'' in each OWL 1.1 vocabulary must include a unary datatype ''rdfs:Literal'' interpreted as ''Δ<sub>D</sub>''<nowiki>; furthermore, it must also include the following unary datatypes: </nowiki>[http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#string ''xsd:string''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#boolean ''xsd:boolean''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#decimal ''xsd:decimal''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#float ''xsd:float''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#double ''xsd:double''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#dateTime ''xsd:dateTime''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#time ''xsd:time''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#date ''xsd:date''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gYearMonth ''xsd:gYearMonth''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gYear ''xsd:gYear''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gMonthDay ''xsd:gMonthDay''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gDay ''xsd:gDay''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#gMonth ''xsd:gMonth''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#hexBinary ''xsd:hexBinary''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#base64Binary ''xsd:base64Binary''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#anyURI ''xsd:anyURI''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#normalizedString ''xsd:normalizedString''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#token ''xsd:token''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#language ''xsd:language''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#NMTOKEN ''xsd:NMTOKEN''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#Name ''xsd:Name''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#NCName ''xsd:NCName''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#integer ''xsd:integer''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#nonPositiveInteger ''xsd:nonPositiveInteger''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#negativeInteger ''xsd:negativeInteger''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#long ''xsd:long''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#int ''xsd:int''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#short ''xsd:short''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#byte ''xsd:byte''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#nonNegativeInteger ''xsd:nonNegativeInteger''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedLong ''xsd:unsignedLong''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedInt ''xsd:unsignedInt''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedShort ''xsd:unsignedShort''], [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#unsignedByte ''xsd:unsignedByte''], and [http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/#positiveInteger ''xsd:positiveInteger'']. These datatypes, as well as the well-formed constants from ''N<sub>V</sub>'', are interpreted as specified in [<cite>[[#ref-xml-schema-datatypes|XML Schema Datatypes]]</cite>]. (Note that the value spaces of primitive XML Schema Datatypes are disjoint, so <span class="name">"2"^^xsd:decimal</span><sup>D</sup> is different from <span class="name">"2"^^xsd:float"</span><sup>D</sup>.)
  
 
The set ''Δ<sub>D</sub>'' is a fixed set that must be ''large enough''<nowiki>; that is, it must contain the extension of each datatype from </nowiki>''N<sub>D</sub>'' and, apart from that, an infinite number of other objects. Such a definition is ambiguous, as it does not uniquely single out a particular set ''Δ<sub>D</sub>''<nowiki>; however, the choice of the actual set is not actually relevant for the definition of the semantics, as long as it contains the interpretations of all datatypes that one can "reasonably think of." This allows the implementations to support datatypes other than the ones mentioned in the previous paragraphs without affecting the semantics.</nowiki>
 
The set ''Δ<sub>D</sub>'' is a fixed set that must be ''large enough''<nowiki>; that is, it must contain the extension of each datatype from </nowiki>''N<sub>D</sub>'' and, apart from that, an infinite number of other objects. Such a definition is ambiguous, as it does not uniquely single out a particular set ''Δ<sub>D</sub>''<nowiki>; however, the choice of the actual set is not actually relevant for the definition of the semantics, as long as it contains the interpretations of all datatypes that one can "reasonably think of." This allows the implementations to support datatypes other than the ones mentioned in the previous paragraphs without affecting the semantics.</nowiki>
Line 67: Line 65:
  
 
{| border="2" cellpadding="5"
 
{| border="2" cellpadding="5"
|+ <span class="caption">Table 1.</span> Interpreting Property Expressions
+
|+ <span class="caption">Table 1.</span> Interpreting Object Property Expressions
 
|-
 
|-
! Property
+
! Object Property Expression
 
! Interpretation
 
! Interpretation
|-
+
|-  
 
| class="name" | InverseObjectProperty(R)
 
| class="name" | InverseObjectProperty(R)
| { ''( x , y )'' | ''( y , x )'' ∈ ''R<sup>Ipo</sup>'' }
+
| { ''( x , y )'' <nowiki>|</nowiki> ''( y , x )'' ∈ ''R<sup>Ipo</sup>'' }
 
|}
 
|}
  
Line 101: Line 99:
 
</div>
 
</div>
  
We extend the class interpretation function ''.<sup>Ic</sup>'' to classes as shown in Table 3. With ''<nowiki>#S</nowiki>'' we denote the number of elements in a set ''S''.
+
We extend the class interpretation function ''.<sup>Ic</sup>'' to descriptions as shown in Table 3. With ''<nowiki>#S</nowiki>'' we denote the number of elements in a set ''S''.
  
 
<div style="text-align: center">
 
<div style="text-align: center">
  
 
{| border="2" cellpadding="5"
 
{| border="2" cellpadding="5"
|+ <span class="caption">Table 3.</span> Interpreting Classes
+
|+ <span class="caption">Table 3.</span> Interpreting Descriptions
 
|-
 
|-
! Class
+
! Description
 
! Interpretation
 
! Interpretation
 
|-
 
|-
Line 130: Line 128:
 
|-
 
|-
 
| class="name" | ObjectSomeValuesFrom(R C)
 
| class="name" | ObjectSomeValuesFrom(R C)
| { ''x'' | ∃ ''y'' : ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' and ''y'' ∈ ''C<sup>Ic</sup>'' }
+
| { ''x'' <nowiki>|</nowiki> ∃ ''y'' : ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' and ''y'' ∈ ''C<sup>Ic</sup>'' }
 
|-
 
|-
 
| class="name" | ObjectAllValuesFrom(R C)
 
| class="name" | ObjectAllValuesFrom(R C)
| { ''x'' | ∀ ''y'' : ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' implies ''y'' ∈ ''C<sup>Ic</sup>'' }
+
| { ''x'' <nowiki>|</nowiki> ∀ ''y'' : ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' implies ''y'' ∈ ''C<sup>Ic</sup>'' }
 
|-
 
|-
 
| class="name" | ObjectHasValue(R a)
 
| class="name" | ObjectHasValue(R a)
| { ''x'' | ''( x, a<sup>Ii</sup> )'' ∈ ''R<sup>Ipo</sup>'' }
+
| { ''x'' <nowiki>|</nowiki> ''( x, a<sup>Ii</sup> )'' ∈ ''R<sup>Ipo</sup>'' }
 
|-
 
|-
 
| class="name" | ObjectExistsSelf(R)
 
| class="name" | ObjectExistsSelf(R)
| { ''x'' | ''( x, x )'' ∈ ''R<sup>Ipo</sup>'' }
+
| { ''x'' <nowiki>|</nowiki> ''( x, x )'' ∈ ''R<sup>Ipo</sup>'' }
 
|-
 
|-
 
| class="name" | ObjectMinCardinality(n R C)
 
| class="name" | ObjectMinCardinality(n R C)
| { ''x'' | #{ ''y'' | ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' and ''y'' ∈ ''C<sup>Ic</sup>'' } ≥ n }
+
| { ''x'' <nowiki>|</nowiki> #{ ''y'' <nowiki>|</nowiki> ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' and ''y'' ∈ ''C<sup>Ic</sup>'' } ≥ n }
 
|-
 
|-
 
| class="name" | ObjectMaxCardinality(n R C)
 
| class="name" | ObjectMaxCardinality(n R C)
| { ''x'' | #{ ''y'' | ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' and ''y'' ∈ ''C<sup>Ic</sup>'' } ≤ n }
+
| { ''x'' <nowiki>|</nowiki> #{ ''y'' <nowiki>|</nowiki> ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' and ''y'' ∈ ''C<sup>Ic</sup>'' } ≤ n }
 
|-
 
|-
 
| class="name" | ObjectExactCardinality(n R C)
 
| class="name" | ObjectExactCardinality(n R C)
| { ''x'' | #{ ''y'' | ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' and ''y'' ∈ ''C<sup>Ic</sup>'' } = n }
+
| { ''x'' <nowiki>|</nowiki> #{ ''y'' <nowiki>|</nowiki> ''( x, y )'' ∈ ''R<sup>Ipo</sup>'' and ''y'' ∈ ''C<sup>Ic</sup>'' } = n }
 
|-
 
|-
| class="name" | DatatSomeValuesFrom(U<sub>1</sub> ... U<sub>n</sub> DR)
+
| class="name" | DataSomeValuesFrom(U<sub>1</sub> ... U<sub>n</sub> DR)
| { ''x'' | ∃ ''y<sub>1</sub>'', ..., ''y<sub>n</sub>'' : ''( x, y<sub>k</sub> )'' ∈ ''U<sub>k</sub><sup>Ipd</sup>'' for each 1 ≤ ''k'' ≤ ''n'' and ''( y<sub>1</sub>, ..., y<sub>n</sub> )'' ∈ ''DR<sup>D</sup>'' }
+
| { ''x'' <nowiki>|</nowiki> ∃ ''y<sub>1</sub>'', ..., ''y<sub>n</sub>'' : ''( x, y<sub>k</sub> )'' ∈ ''U<sub>k</sub><sup>Ipd</sup>'' for each 1 ≤ ''k'' ≤ ''n'' and ''( y<sub>1</sub>, ..., y<sub>n</sub> )'' ∈ ''DR<sup>D</sup>'' }
 
|-
 
|-
| class="name" | DatatAllValuesFrom(U<sub>1</sub> ... U<sub>n</sub> DR)
+
| class="name" | DataAllValuesFrom(U<sub>1</sub> ... U<sub>n</sub> DR)
| { ''x'' | ∀ ''y<sub>1</sub>'', ..., ''y<sub>n</sub>'' : ''( x, y<sub>k</sub> )'' ∈ ''U<sub>k</sub><sup>Ipd</sup>'' for each 1 ≤ ''k'' ≤ ''n'' implies ''( y<sub>1</sub>, ..., y<sub>n</sub> )'' ∈ ''DR<sup>D</sup>'' }
+
| { ''x'' <nowiki>|</nowiki> ∀ ''y<sub>1</sub>'', ..., ''y<sub>n</sub>'' : ''( x, y<sub>k</sub> )'' ∈ ''U<sub>k</sub><sup>Ipd</sup>'' for each 1 ≤ ''k'' ≤ ''n'' implies ''( y<sub>1</sub>, ..., y<sub>n</sub> )'' ∈ ''DR<sup>D</sup>'' }
 
|-
 
|-
 
| class="name" | DataHasValue(U v)
 
| class="name" | DataHasValue(U v)
| { ''x'' | ''( x, v<sup>D</sup> )'' ∈ ''U<sup>Ipd</sup>'' }
+
| { ''x'' <nowiki>|</nowiki> ''( x, v<sup>D</sup> )'' ∈ ''U<sup>Ipd</sup>'' }
 
|-
 
|-
 
| class="name" | DataMinCardinality(n U DR)
 
| class="name" | DataMinCardinality(n U DR)
| { ''x'' | #{ ''y'' | ''( x, y )'' ∈ ''U<sup>Ipd</sup>'' and ''y'' ∈ ''DR<sup>D</sup>'' } ≥ n }
+
| { ''x'' <nowiki>|</nowiki> #{ ''y'' <nowiki>|</nowiki> ''( x, y )'' ∈ ''U<sup>Ipd</sup>'' and ''y'' ∈ ''DR<sup>D</sup>'' } ≥ n }
 
|-
 
|-
| class="name" | DataMaxnCardinality(n U DR)
+
| class="name" | DataMaxCardinality(n U DR)
| { ''x'' | #{ ''y'' | ''( x, y )'' ∈ ''U<sup>Ipd</sup>'' and ''y'' ∈ ''DR<sup>D</sup>'' } ≤ n }
+
| { ''x'' <nowiki>|</nowiki> #{ ''y'' <nowiki>|</nowiki> ''( x, y )'' ∈ ''U<sup>Ipd</sup>'' and ''y'' ∈ ''DR<sup>D</sup>'' } ≤ n }
 
|-
 
|-
 
| class="name" | DataExactCardinality(n U DR)
 
| class="name" | DataExactCardinality(n U DR)
| { ''x'' | #{ ''y'' | ''( x, y )'' ∈ ''U<sup>Ipd</sup>'' and ''y'' ∈ ''DR<sup>D</sup>'' } = n }
+
| { ''x'' <nowiki>|</nowiki> #{ ''y'' <nowiki>|</nowiki> ''( x, y )'' ∈ ''U<sup>Ipd</sup>'' and ''y'' ∈ ''DR<sup>D</sup>'' } = n }
 
|}
 
|}
  
Line 206: Line 204:
 
|-
 
|-
 
| class="name" | ObjectPropertyDomain(R C)
 
| class="name" | ObjectPropertyDomain(R C)
| { ''x'' | ∃ y : ''(x , y )'' ∈ ''R<sup>Ipo</sup>'' } ⊆ ''C<sup>Ic</sup>''
+
| { ''x'' <nowiki>|</nowiki> ∃ y : ''(x , y )'' ∈ ''R<sup>Ipo</sup>'' } ⊆ ''C<sup>Ic</sup>''
 
|-
 
|-
 
| class="name" | ObjectPropertyRange(R C)
 
| class="name" | ObjectPropertyRange(R C)
| { ''y'' | ∃ x : ''(x , y )'' ∈ ''R<sup>Ipo</sup>'' } ⊆ ''C<sup>Ic</sup>''
+
| { ''y'' <nowiki>|</nowiki> ∃ x : ''(x , y )'' ∈ ''R<sup>Ipo</sup>'' } ⊆ ''C<sup>Ic</sup>''
 
|-
 
|-
 
| class="name" | InverseObjectProperties(R S)
 
| class="name" | InverseObjectProperties(R S)
| ''R<sup>Ipo</sup>'' = { ''( x , y )'' | ''( y , x )'' ∈ ''S<sup>Ipo</sup>'' }
+
| ''R<sup>Ipo</sup>'' = { ''( x , y )'' <nowiki>|</nowiki> ''( y , x )'' ∈ ''S<sup>Ipo</sup>'' }
 
|-
 
|-
 
| class="name" | FunctionalObjectProperty(R)
 
| class="name" | FunctionalObjectProperty(R)
Line 245: Line 243:
 
|-
 
|-
 
| class="name" | DataPropertyDomain(U C)
 
| class="name" | DataPropertyDomain(U C)
| { ''x'' | ∃ y : ''(x , y )'' ∈ ''U<sup>Ipd</sup>'' } ⊆ ''C<sup>Ic</sup>''
+
| { ''x'' <nowiki>|</nowiki> ∃ y : ''(x , y )'' ∈ ''U<sup>Ipd</sup>'' } ⊆ ''C<sup>Ic</sup>''
 
|-
 
|-
 
| class="name" | DataPropertyRange(U DR)
 
| class="name" | DataPropertyRange(U DR)
| { ''y'' | ∃ x : ''(x , y )'' ∈ ''U<sup>Ipd</sup>'' } ⊆ ''DR<sup>D</sup>''
+
| { ''y'' <nowiki>|</nowiki> ∃ x : ''(x , y )'' ∈ ''U<sup>Ipd</sup>'' } ⊆ ''DR<sup>D</sup>''
 
|-
 
|-
 
| class="name" | FunctionalDataProperty(U)
 
| class="name" | FunctionalDataProperty(U)
Line 277: Line 275:
 
</div>
 
</div>
  
Let ''O'' be an OWL 1.1 ontology with vocabulary ''V''. ''O'' is ''consistent'' if an interpretation ''I'' exists that satisfies all the axioms of the axiom closure of ''O'' (the axiom closure of ''O'' is defined in [<cite>[[#ref-owl-1.1-specification|OWL 1.1 Specification]]</cite>]); such ''I'' is then called a ''model'' of ''O''. A class ''C'' is satisfiable w.r.t. ''O'' if there is a model ''I'' of ''O'' such that ''C<sup>Ic</sup>'' is not empty. ''O'' ''entails'' an OWL 1.1 ontology ''O''' with vocabulary ''V'' if every model of ''O'' is also a model of ''O'''<nowiki>; furthermore, </nowiki>''O'' and ''O''' are ''equivalent'' if ''O'' entails ''O''' and ''O''' entails ''O''.
+
Let ''O'' be an OWL 1.1 ontology with vocabulary ''V''. ''O'' is ''consistent'' if an interpretation ''I'' exists that satisfies all the axioms of the axiom closure of ''O'' (the axiom closure of ''O'' is defined in [<cite>[[#ref-owl-1.1-specification|OWL 1.1 Specification]]</cite>]); such ''I'' is then called a ''model'' of ''O''. A description ''C'' is satisfiable w.r.t. ''O'' if there is a model ''I'' of ''O'' such that ''C<sup>Ic</sup>'' is not empty. ''O'' ''entails'' an OWL 1.1 ontology ''O''' with vocabulary ''V'' if every model of ''O'' is also a model of ''O'''<nowiki>; furthermore, </nowiki>''O'' and ''O''' are ''equivalent'' if ''O'' entails ''O''' and ''O''' entails ''O''.
  
 
----
 
----
Line 283: Line 281:
 
== References ==
 
== References ==
  
; [Description Logics]
+
; <span id="ref-description-logics">[Description Logics]</span>
 
: [http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=0521781760 <cite>The Description Logic Handbook</cite>]. Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, Peter Patel-Schneider, editors. Cambridge University Press, 2003; and [http://dl.kr.org/ <cite>Description Logics Home Page</cite>].
 
: [http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=0521781760 <cite>The Description Logic Handbook</cite>]. Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, Peter Patel-Schneider, editors. Cambridge University Press, 2003; and [http://dl.kr.org/ <cite>Description Logics Home Page</cite>].
; [Metamodeling]
+
; <span id="ref-metamodeling">[Metamodeling]</span>
 
: <cite>On the Properties of Metamodeling in OWL</cite>. Boris Motik. In Proceedings of ISWC-2005
 
: <cite>On the Properties of Metamodeling in OWL</cite>. Boris Motik. In Proceedings of ISWC-2005
; [OWL 1.1 Specification]
+
; <span id="ref-owl-1.1-specification">[OWL 1.1 Specification]</span>
 
: <cite>[owl_specification.html OWL 1.1 Web Ontology Language: Structural Specification and Functional-Style Syntax]</cite>. Peter F. Patel-Schneider, Ian Horrocks, and Boris Motik, eds., 2006.
 
: <cite>[owl_specification.html OWL 1.1 Web Ontology Language: Structural Specification and Functional-Style Syntax]</cite>. Peter F. Patel-Schneider, Ian Horrocks, and Boris Motik, eds., 2006.
; [OWL Abstract Syntax and Semantics]
+
; <span id="ref-owl-abstract-syntax-and-semantics">[OWL Abstract Syntax and Semantics]</span>
 
: <cite>[http://www.w3.org/TR/owl-semantics/ OWL Web Ontology Language: Semantics and Abstract Syntax]</cite>. Peter F. Patel-Schneider, Pat Hayes, and Ian Horrocks, Editors, W3C Recommendation, 10 February 2004.
 
: <cite>[http://www.w3.org/TR/owl-semantics/ OWL Web Ontology Language: Semantics and Abstract Syntax]</cite>. Peter F. Patel-Schneider, Pat Hayes, and Ian Horrocks, Editors, W3C Recommendation, 10 February 2004.
; [SROIQ]
+
; <span id="ref-sroiq">[SROIQ]</span>
 
: <cite>[http://www.cs.man.ac.uk/~sattler/publications/sroiq-tr.pdf The Even More Irresistible SROIQ]</cite>. 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.
 
: <cite>[http://www.cs.man.ac.uk/~sattler/publications/sroiq-tr.pdf The Even More Irresistible SROIQ]</cite>. 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]
+
; <span id="ref-xml-schema-datatypes">[XML Schema Datatypes]</span>
 
: <cite>[http://www.w3.org/TR/xmlschema-2/ XML Schema Part 2: Datatypes Second Edition]</cite>. Paul V. Biron and Ashok Malhotra, eds. W3C Recommendation 28 October 2004.
 
: <cite>[http://www.w3.org/TR/xmlschema-2/ XML Schema Part 2: Datatypes Second Edition]</cite>. Paul V. Biron and Ashok Malhotra, eds. W3C Recommendation 28 October 2004.

Revision as of 06:08, 31 October 2007

__NUMBEREDHEADINGS__

[Hide Review Comments]

Document title:
OWL 2 Web Ontology Language
Model-Theoretic Semantics (Second Edition)
Authors
Bernardo Cuenca Grau, The University of Manchester
Boris Motik, The University of Manchester
Contributors
Ian Horrocks, The University of Manchester
Bijan Parsia, The University of Manchester
Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies
Ulrike Sattler, The University of Manchester
Abstract
OWL 1.1 extends the W3C OWL Web Ontology Language with a small but useful set of features that have been requested by users, for which effective reasoning algorithms are now available, and that OWL tool developers are willing to support. The new features include extra syntactic sugar, additional property and qualified cardinality constructors, extended datatype support, simple metamodeling, and extended annotations. This document provides a model-theoretic semantics for OWL 1.1.
Status
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 © 2006-2007 by the Authors. This document is available under the W3C Document License. See the W3C Intellectual Rights Notice and Legal Disclaimers for additional information.

1 Introduction

This document defines the formal semantics of OWL 1.1. The semantics given here follows the principles for defining the semantics of description logics [Description Logics] and is compatible with the description logic SROIQ presented in [SROIQ]. Unfortunately, the definition of SROIQ given in [SROIQ] does not provide for datatypes and metamodeling. Therefore, the semantics of OWL 1.1 is defined in a direct model-theoretic way, by interpreting the constructs of the functional-style syntax from [OWL 1.1 Specification]. For the constructs available in SROIQ, the semantics of SROIQ trivially corresponds to the one defined in this document.

OWL 1.1 does not have an RDF-compatible semantics. Ontologies expressed in OWL RDF are given semantics by converting then into the functional-style syntax and interpreting the result as specified in this document.

OWL 1.1 allows for annotations of ontologies and ontology entities (classes, properties, and individuals) and ontology axioms. Annotations, however, have no semantic meaning in OWL 1.1 and are ignored in this document. Definitions in OWL 1.1 similarly have no semantics. Constructs only used in annotations and definitions, like ObjectProperty, therefore do not show up in this document.

Since OWL 1.1 is an extension of OWL DL, this document also provides a formal semantics for OWL Lite and OWL DL and it is equivalent to the definition given in [OWL Abstract Syntax and Semantics].

2 Model-Theoretic Semantics for OWL 1.1

A vocabulary (or signature) V = ( NC , NPo , NPd , NI , ND , NV ) is a 6-tuple where

  • NC is a set of OWL classes,
  • NPo is a set of object properties,
  • NPd is a set of data properties,
  • NI is a set of individuals, and
  • ND is a set of datatypes each associated with a positive integer datatype arity,
  • NV is a set of well-formed constants.

Since OWL 1.1 allows punning [Metamodeling] in the signature, we do not require the sets NC , NPo , NPd , NI , ND , and NV to be pair-wise disjoint. Thus, the same name can be used in an ontology to denote a class, a datatype, a property (object or data), an individual, and a constant. The set ND is defined as it is because a datatype is defined by its name and the arity, and such a definition allows one to reuse the same name with different arities.

The semantics of OWL 1.1 is defined with respect to a concrete domain, which is a tuple D = ( ΔD , .D ) where

  • ΔD is a fixed set called the data domain,
  • .D assigns to each constant v ∈ NV an element vD of ΔD, and
  • .D assigns to each datatype d ∈ ND with arity n an n-ary relation dD over ΔD.

The set of datatypes ND in each OWL 1.1 vocabulary must include a unary datatype rdfs:Literal interpreted as ΔD; furthermore, it must also include the following unary datatypes: xsd:string, xsd:boolean, xsd:decimal, xsd:float, xsd:double, xsd:dateTime, xsd:time, xsd:date, xsd:gYearMonth, xsd:gYear, xsd:gMonthDay, xsd:gDay, xsd:gMonth, xsd:hexBinary, xsd:base64Binary, xsd:anyURI, xsd:normalizedString, xsd:token, xsd:language, xsd:NMTOKEN, xsd:Name, xsd:NCName, xsd:integer, xsd:nonPositiveInteger, xsd:negativeInteger, xsd:long, xsd:int, xsd:short, xsd:byte, xsd:nonNegativeInteger, xsd:unsignedLong, xsd:unsignedInt, xsd:unsignedShort, xsd:unsignedByte, and xsd:positiveInteger. These datatypes, as well as the well-formed constants from NV, are interpreted as specified in [XML Schema Datatypes]. (Note that the value spaces of primitive XML Schema Datatypes are disjoint, so "2"^^xsd:decimalD is different from "2"^^xsd:float"D.)

The set ΔD is a fixed set that must be large enough; that is, it must contain the extension of each datatype from ND and, apart from that, an infinite number of other objects. Such a definition is ambiguous, as it does not uniquely single out a particular set ΔD; however, the choice of the actual set is not actually relevant for the definition of the semantics, as long as it contains the interpretations of all datatypes that one can "reasonably think of." This allows the implementations to support datatypes other than the ones mentioned in the previous paragraphs without affecting the semantics.

Given a vocabulary V and a concrete domain D, an interpretation I = ( ΔI , .Ic , .Ipo , .Ipd , .Ii ) is a 5-tuple where

  • ΔI is a nonempty set disjoint with ΔD, called the object domain;
  • .Ic is the class interpretation function that assigns to each OWL class A ∈ NIc a subset AIc of ΔI ;
  • .Ipo is the object property interpretation function that assigns to each object property R ∈ NPo a subset RIpo of ΔI x ΔI ;
  • .Ipd is the data property interpretation function that assigns to each data property U ∈ NPd a subset UIpd of ΔI x ΔD ;
  • .Ii is the individual interpretation function that assigns to each individual a ∈ NI an element aIi from ΔI.

We extend the object interpretation function .Ipo to object property expressions as shown in Table 1.

Table 1. Interpreting Object Property Expressions
Object Property Expression Interpretation
InverseObjectProperty(R) { ( x , y ) | ( y , x )RIpo }

We extend the interpretation function .D to data ranges as shown in Table 2.

Table 2. Interpreting Data Ranges
Data Range Interpretation
DataOneOf(v1 ... vn) { v1D , ... , vnD }
DataComplementOf(DR) ( ΔD )n \ DRD where n is the arity of DR
DatatypeRestriction(DR f v)

the n-ary relation over ΔD obtained by applying the facet f with value v
to the data range DR as specified in [XML Schema Datatypes]

We extend the class interpretation function .Ic to descriptions as shown in Table 3. With #S we denote the number of elements in a set S.

Table 3. Interpreting Descriptions
Description Interpretation
owl:Thing ΔI
owl:Nothing empty set
ObjectComplementOf(C) ΔI \ CIc
ObjectIntersectionOf(C1 ... Cn) C1Ic ∩ ... ∩ CnIc
ObjectUnionOf(C1 ... Cn) C1Ic ∪ ... ∪ CnIc
ObjectOneOf(a1 ... an) { a1Ii , ... , anIi }
ObjectSomeValuesFrom(R C) { x | ∃ y : ( x, y )RIpo and yCIc }
ObjectAllValuesFrom(R C) { x | ∀ y : ( x, y )RIpo implies yCIc }
ObjectHasValue(R a) { x | ( x, aIi )RIpo }
ObjectExistsSelf(R) { x | ( x, x )RIpo }
ObjectMinCardinality(n R C) { x | #{ y | ( x, y )RIpo and yCIc } ≥ n }
ObjectMaxCardinality(n R C) { x | #{ y | ( x, y )RIpo and yCIc } ≤ n }
ObjectExactCardinality(n R C) { x | #{ y | ( x, y )RIpo and yCIc } = n }
DataSomeValuesFrom(U1 ... Un DR) { x | ∃ y1, ..., yn : ( x, yk )UkIpd for each 1 ≤ kn and ( y1, ..., yn )DRD }
DataAllValuesFrom(U1 ... Un DR) { x | ∀ y1, ..., yn : ( x, yk )UkIpd for each 1 ≤ kn implies ( y1, ..., yn )DRD }
DataHasValue(U v) { x | ( x, vD )UIpd }
DataMinCardinality(n U DR) { x | #{ y | ( x, y )UIpd and yDRD } ≥ n }
DataMaxCardinality(n U DR) { x | #{ y | ( x, y )UIpd and yDRD } ≤ n }
DataExactCardinality(n U DR) { x | #{ y | ( x, y )UIpd and yDRD } = n }

Satisfaction of OWL 1.1 axioms in an interpretation I is defined as shown in Table 4. With o we denote the composition of binary relations.

Table 4. Satisfaction of Axioms in an Interpretation
Axiom Condition
SubClassOf(C D) CIcDIc
EquivalentClasses(C1 ... Cn) CjIc = CkIc for each 1 ≤ j , kn
DisjointClasses(C1 ... Cn) CjIcCkIc is empty for each 1 ≤ j , kn and jk
DisjointUnion(A C1 ... Cn) AIc = C1Ic ∪ ... ∪ CnIc and CjIcCkIc is empty for each 1 ≤ j , kn and jk
SubObjectPropertyOf(R S) RIpoSIpo
SubObjectPropertyOf(SubObjectPropertyChain(R1 ... Rn) S) R1Ipo o ... o RnIpoSIpo
EquivalentObjectProperties(R1 ... Rn) RjIpo = RkIpo for each 1 ≤ j , kn
DisjointObjectProperties(R1 ... Rn) RjIpoRkIpo is empty for each 1 ≤ j , kn and jk
ObjectPropertyDomain(R C) { x | ∃ y : (x , y )RIpo } ⊆ CIc
ObjectPropertyRange(R C) { y | ∃ x : (x , y )RIpo } ⊆ CIc
InverseObjectProperties(R S) RIpo = { ( x , y ) | ( y , x )SIpo }
FunctionalObjectProperty(R) ( x , y1 ) ∈ RIpo and ( x , y2 ) ∈ RIpo imply y1 = y2
InverseFunctionalObjectProperty(R) ( x1 , y ) ∈ RIpo and ( x2 , y ) ∈ RIpo imply x1 = x2
ReflexiveObjectProperty(R) x ∈ ΔI implies ( x , x ) ∈ RIpo
IrreflexiveObjectProperty(R) x ∈ ΔI implies ( x , x ) is not in RIpo
SymmetricObjectProperty(R) ( x , y ) ∈ RIpo implies ( y , x ) ∈ RIpo
AntisymmetricObjectProperty(R) ( x , y ) ∈ RIpo implies ( y , x ) is not in RIpo
TransitiveObjectProperty(R) RIpo o RIpo ⊆ RIpo
SubDataPropertyOf(U V) UIpdVIpd
EquivalentDataProperties(U1 ... Un) UjIpd = UkIpd for each 1 ≤ j , kn
DisjointDataProperties(U1 ... Un) UjIpdUkIpd is empty for each 1 ≤ j , kn and jk
DataPropertyDomain(U C) { x | ∃ y : (x , y )UIpd } ⊆ CIc
DataPropertyRange(U DR) { y | ∃ x : (x , y )UIpd } ⊆ DRD
FunctionalDataProperty(U) ( x , y1 ) ∈ UIpd and ( x , y2 ) ∈ UIpd imply y1 = y2
SameIndividual(a1 ... an) ajIi = akIi for each 1 ≤ j , kn
DifferentIndividuals(a1 ... an) ajIiakIi for each 1 ≤ j , kn and jk
ClassAssertion(a C) aIiCIc
ObjectPropertyAssertion(R a b) ( aIi , bIi )RIpo
NegativeObjectPropertyAssertion(R a b) ( aIi , bIi ) is not in RIpo
DataPropertyAssertion(U a v) ( aIi , vD )UIpd
NegativeDataPropertyAssertion(U a v) ( aIi , vD ) is not in UIpd

Let O be an OWL 1.1 ontology with vocabulary V. O is consistent if an interpretation I exists that satisfies all the axioms of the axiom closure of O (the axiom closure of O is defined in [OWL 1.1 Specification]); such I is then called a model of O. A description C is satisfiable w.r.t. O if there is a model I of O such that CIc is not empty. O entails an OWL 1.1 ontology O' with vocabulary V if every model of O is also a model of O; furthermore, O and O are equivalent if O entails O and O entails O.


3 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.
[Metamodeling]
On the Properties of Metamodeling in OWL. Boris Motik. In Proceedings of ISWC-2005
[OWL 1.1 Specification]
[owl_specification.html OWL 1.1 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.