Difference between revisions of "RDF-Based Semantics"

From OWL
Jump to: navigation, search
(Resolution of LC 16: added to changelog)
(F2F5 Resolution: changed RDF encoding of sub property chains)
Line 494: Line 494:
 
|+ <span class="caption">Table 3.2: OWL 2 Full Vocabulary</span>
 
|+ <span class="caption">Table 3.2: OWL 2 Full Vocabulary</span>
 
|-
 
|-
| class="name" | owl:AllDifferent owl:AllDisjointClasses owl:AllDisjointProperties owl:allValuesFrom owl:Annotation owl:AnnotationProperty owl:assertionProperty owl:AsymmetricProperty owl:Axiom owl:backwardCompatibleWith owl:bottomDataProperty owl:bottomObjectProperty owl:cardinality owl:Class owl:complementOf owl:DataRange owl:datatypeComplementOf owl:DatatypeProperty owl:deprecated owl:DeprecatedClass owl:DeprecatedProperty owl:differentFrom owl:disjointUnionOf owl:disjointWith owl:distinctMembers owl:equivalentClass owl:equivalentProperty owl:FunctionalProperty owl:hasKey owl:hasSelf owl:hasValue owl:imports owl:incompatibleWith owl:intersectionOf owl:InverseFunctionalProperty owl:inverseOf owl:IrreflexiveProperty owl:maxCardinality owl:maxQualifiedCardinality owl:members owl:minCardinality owl:minQualifiedCardinality owl:NamedIndividual owl:NegativePropertyAssertion owl:Nothing owl:object owl:ObjectProperty owl:onClass owl:onDataRange owl:onDatatype owl:oneOf owl:onProperty owl:onProperties owl:Ontology owl:OntologyProperty owl:predicate owl:priorVersion owl:propertyChain owl:propertyDisjointWith owl:qualifiedCardinality owl:ReflexiveProperty owl:Restriction owl:sameAs owl:someValuesFrom owl:sourceIndividual owl:subject owl:SymmetricProperty owl:targetIndividual owl:targetValue owl:Thing owl:topDataProperty owl:topObjectProperty owl:TransitiveProperty owl:unionOf owl:versionInfo owl:withRestrictions
+
| class="name" | owl:AllDifferent owl:AllDisjointClasses owl:AllDisjointProperties owl:allValuesFrom owl:Annotation owl:AnnotationProperty owl:assertionProperty owl:AsymmetricProperty owl:Axiom owl:backwardCompatibleWith owl:bottomDataProperty owl:bottomObjectProperty owl:cardinality owl:Class owl:complementOf owl:DataRange owl:datatypeComplementOf owl:DatatypeProperty owl:deprecated owl:DeprecatedClass owl:DeprecatedProperty owl:differentFrom owl:disjointUnionOf owl:disjointWith owl:distinctMembers owl:equivalentClass owl:equivalentProperty owl:FunctionalProperty owl:hasKey owl:hasSelf owl:hasValue owl:imports owl:incompatibleWith owl:intersectionOf owl:InverseFunctionalProperty owl:inverseOf owl:IrreflexiveProperty owl:maxCardinality owl:maxQualifiedCardinality owl:members owl:minCardinality owl:minQualifiedCardinality owl:NamedIndividual owl:NegativePropertyAssertion owl:Nothing owl:object owl:ObjectProperty owl:onClass owl:onDataRange owl:onDatatype owl:oneOf owl:onProperty owl:onProperties owl:Ontology owl:OntologyProperty owl:predicate owl:priorVersion owl:propertyChainAxiom owl:propertyDisjointWith owl:qualifiedCardinality owl:ReflexiveProperty owl:Restriction owl:sameAs owl:someValuesFrom owl:sourceIndividual owl:subject owl:SymmetricProperty owl:targetIndividual owl:targetValue owl:Thing owl:topDataProperty owl:topObjectProperty owl:TransitiveProperty owl:unionOf owl:versionInfo owl:withRestrictions
 
|-
 
|-
 
|}
 
|}
Line 1,221: Line 1,221:
 
under the OWL 2 Full semantics.
 
under the OWL 2 Full semantics.
 
The language features in question are
 
The language features in question are
''sub property chains''
 
in [[#Semantic_Conditions_for_Sub_Property_Chains|Section 5.9]],
 
 
''n-ary axioms''  
 
''n-ary axioms''  
 
in [[#Semantic_Conditions_for_N-ary_Axioms|Section 5.11]],
 
in [[#Semantic_Conditions_for_N-ary_Axioms|Section 5.11]],
Line 1,583: Line 1,581:
 
and Section 5.5 of [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>]  
 
and Section 5.5 of [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>]  
 
for <span class="name">owl:deprecated</span>).
 
for <span class="name">owl:deprecated</span>).
 
The domain of the property
 
<span class="name">owl:propertyChain</span>
 
is unrestricted,
 
since the left hand side node of a triple
 
having this property as its predicate
 
is considered to be an arbitrary "root node"
 
of a sub property chain axiom.
 
  
 
<div id="tab-semcond-properties" class="center">
 
<div id="tab-semcond-properties" class="center">
Line 1,757: Line 1,747:
 
| &sube; IX &times; IX
 
| &sube; IX &times; IX
 
|-
 
|-
| <span class="name">owl:propertyChain</span>
+
| <span class="name">owl:propertyChainAxiom</span>
 
| &isin; IP
 
| &isin; IP
| &sube; IR &times; ISEQ
+
| &sube; IP &times; ISEQ
 
|-
 
|-
 
| <span class="name">owl:propertyDisjointWith</span>
 
| <span class="name">owl:propertyDisjointWith</span>
Line 2,155: Line 2,145:
 
lists the semantic conditions for sub property chains,
 
lists the semantic conditions for sub property chains,
 
which allow for specifying complex property subsumption axioms.
 
which allow for specifying complex property subsumption axioms.
 +
 
As an example,
 
As an example,
one can define a sub property chain expressing that
+
one can define a sub property chain axiom,
 +
for which
 
the chain consisting of the extensions of the properties  
 
the chain consisting of the extensions of the properties  
 
<span class="name">ex:hasFather</span>
 
<span class="name">ex:hasFather</span>
Line 2,163: Line 2,155:
 
is covered by the extension of the property
 
is covered by the extension of the property
 
<span class="name">ex:hasUncle</span>.
 
<span class="name">ex:hasUncle</span>.
The semantics have been specified in a way
 
to allow a sub property chain axiom to be satisfiable
 
without requiring the existence of a property
 
that represents the property chain.
 
In particular, the property on the left hand side of the sub property assertion
 
does not necessarily represent the property chain.
 
  
 
''Informative note:''
 
''Informative note:''
Line 2,186: Line 2,172:
 
[[#topic-semcond-conditionform|notes on the form of semantic conditions]]
 
[[#topic-semcond-conditionform|notes on the form of semantic conditions]]
 
for further information on these topics.
 
for further information on these topics.
 +
The semantics have been specified in a way
 +
to allow a sub property chain axiom to be satisfiable
 +
without requiring the existence of a property
 +
that represents the property chain.
  
 
<div id="tab-semcond-subpropertychains" class="center">
 
<div id="tab-semcond-subpropertychains" class="center">
Line 2,191: Line 2,181:
 
|+ <span class="caption">Table 5.9: Semantic Conditions for Sub Property Chains</span>
 
|+ <span class="caption">Table 5.9: Semantic Conditions for Sub Property Chains</span>
 
|-
 
|-
! style="text-align: center" | if
+
! colspan="3" style="text-align: center" | if ''s'' sequence of ''p<sub>1</sub>'' , &hellip; , ''p<sub>n</sub>'' &isin; IR then
! style="text-align: center" | then
+
 
|-
 
|-
| ''s'' sequence of ''p<sub>1</sub>'' , &hellip; , ''p<sub>n</sub>'' &isin; IR ,<br/>&lang; ''z'' , ''p'' &rang; &isin; IEXT(''I''(<span class="name">rdfs:subPropertyOf</span>)) ,<br/>&lang; ''z'' , ''s'' &rang; &isin; IEXT(''I''(<span class="name">owl:propertyChain</span>))
+
| &lang; ''p'' , ''s'' &rang; &isin; IEXT(''I''(<span class="name">owl:propertyChainAxiom</span>))
| ''p<sub>1</sub>'' , &hellip; , ''p<sub>n</sub>'' &isin; IP ,<br/>''p'' &isin; IP ,<br/>&forall; ''y<sub>0</sub>'' , &hellip; , ''y<sub>n</sub>'' : &lang; ''y<sub>0</sub>'' , ''y<sub>1</sub>'' &rang; &isin; IEXT(''p<sub>1</sub>'') and &hellip; and &lang; ''y<sub>n-1</sub>'' , ''y<sub>n</sub>'' &rang; &isin; IEXT(''p<sub>n</sub>'') implies &lang; ''y<sub>0</sub>'' , ''y<sub>n</sub>'' &rang; &isin; IEXT(''p'')
+
! rowspan="1" style="text-align: center" | iff
|-
+
| ''p'' &isin; IP ,<br/>''p<sub>1</sub>'' , &hellip; , ''p<sub>n</sub>'' &isin; IP ,<br/>&forall; ''y<sub>0</sub>'' , &hellip; , ''y<sub>n</sub>'' : &lang; ''y<sub>0</sub>'' , ''y<sub>1</sub>'' &rang; &isin; IEXT(''p<sub>1</sub>'') and &hellip; and &lang; ''y<sub>n-1</sub>'' , ''y<sub>n</sub>'' &rang; &isin; IEXT(''p<sub>n</sub>'') implies &lang; ''y<sub>0</sub>'' , ''y<sub>n</sub>'' &rang; &isin; IEXT(''p'')
! style="text-align: center" | if
+
! style="text-align: center" | then exists ''z'' &isin; IR
+
|-
+
| ''s'' sequence of ''p<sub>1</sub>'' , &hellip; , ''p<sub>n</sub>'' &isin; IP ,<br/>''p'' &isin; IP ,<br/>&forall; ''y<sub>0</sub>'' , &hellip; , ''y<sub>n</sub>'' : &lang; ''y<sub>0</sub>'' , ''y<sub>1</sub>'' &rang; &isin; IEXT(''p<sub>1</sub>'') and &hellip; and &lang; ''y<sub>n-1</sub>'' , ''y<sub>n</sub>'' &rang; &isin; IEXT(''p<sub>n</sub>'') implies &lang; ''y<sub>0</sub>'' , ''y<sub>n</sub>'' &rang; &isin; IEXT(''p'')
+
| &lang; ''z'' , ''p'' &rang; &isin; IEXT(''I''(<span class="name">rdfs:subPropertyOf</span>)) ,<br/>&lang; ''z'' , ''s'' &rang; &isin; IEXT(''I''(<span class="name">owl:propertyChain</span>))
+
 
|-
 
|-
 
|}
 
|}
Line 4,266: Line 4,250:
 
can occur having blank nodes.
 
can occur having blank nodes.
 
* ''Case 1:'' A blank node corresponds to some anonymous individual in ''A'' (for ''A'' being one of a class assertion, object property assertion or data property assertion, according to Sections 5.6, 9.5 and 11.2 in [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>]). The same blank node is used in ''A'', and ''J'' interprets it as an existential variable. This renders the semantic relationship that is expressed by ''A'' into an existential assertion. After applying the definition of ''J'', the analog existential assertion holds w.r.t. ''I'', with the same blank node as the same existential variable in ''g<sub>A</sub>''.
 
* ''Case 1:'' A blank node corresponds to some anonymous individual in ''A'' (for ''A'' being one of a class assertion, object property assertion or data property assertion, according to Sections 5.6, 9.5 and 11.2 in [<cite>[[#ref-owl-2-specification|OWL 2 Specification]]</cite>]). The same blank node is used in ''A'', and ''J'' interprets it as an existential variable. This renders the semantic relationship that is expressed by ''A'' into an existential assertion. After applying the definition of ''J'', the analog existential assertion holds w.r.t. ''I'', with the same blank node as the same existential variable in ''g<sub>A</sub>''.
* ''Case 2:'' A blank node is the "root" node of the multi-triple RDF encoding ''g<sub>A</sub>'' of ''A'' (for ''g<sub>A</sub>'' being one of a sub property chain from [[#Semantic_Conditions_for_Sub_Property_Chains|Section 5.9]], an n-ary axiom from [[#Semantic_Conditions_for_N-ary_Axioms|Section 5.11]], or a negative property assertion from [[#Semantic_Conditions_for_Negative_Property_Assertions|Section 5.15]]). The right-to-left direction of the semantic condition for this kind of axiom is of a form that the triples in ''g<sub>A</sub>'' containing the blank node will be OWL 2 Full satisfied after all the premises of the semantic condition are met.
+
* ''Case 2:'' A blank node is the "root" node of the multi-triple RDF encoding ''g<sub>A</sub>'' of ''A'' (for ''g<sub>A</sub>'' being an n-ary axiom from [[#Semantic_Conditions_for_N-ary_Axioms|Section 5.11]], or a negative property assertion from [[#Semantic_Conditions_for_Negative_Property_Assertions|Section 5.15]]). The right-to-left direction of the semantic condition for this kind of axiom is of a form that the triples in ''g<sub>A</sub>'' containing the blank node will be OWL 2 Full satisfied after all the premises of the semantic condition are met.
 
* ''Case 3:'' A blank node is the "root" node of the multi-triple RDF encoding ''g<sub>E</sub>'' of an expression in ''A'' (for ''g<sub>E</sub>'' being either a sequence, or one of a boolean connective from [[#Semantic_Conditions_for_Boolean_Connectives|Section 5.4]], an enumeration from [[#Semantic_Conditions_for_Enumerations|Section 5.5]], a property restriction from [[#Semantic_Conditions_for_Property_Restrictions|Section 5.6]], or a datatype restriction from [[#Semantic_Conditions_for_Datatype_Restrictions|Section 5.7]]). Since ''G<sub>1</sub>'' is OWL 2 balanced w.r.t. ''G<sub>2</sub>'', ''g<sub>E</sub>'' also occurs in ''G<sub>1</sub>''. Since ''I'' OWL 2 Full satisfies ''G<sub>1</sub>'', ''g<sub>E</sub>'' is OWL 2 Full satisfied, either, taking into account that blank nodes are existential variables. Hence, the left-to-right direction of the respective semantic condition for the particular sort of expression can be applied. This can be done for all the expressions occurring in ''g<sub>A</sub>'', and ''g<sub>A</sub>'' can be seen as a directed acyclic graph with the triples encoding the actual axiom on top, and the different component expressions being connected via blank nodes. Eventually, one can see that all the premises of the right-to-left direction of the semantic condition for the axiom encoded by ''g<sub>A</sub>'' hold.
 
* ''Case 3:'' A blank node is the "root" node of the multi-triple RDF encoding ''g<sub>E</sub>'' of an expression in ''A'' (for ''g<sub>E</sub>'' being either a sequence, or one of a boolean connective from [[#Semantic_Conditions_for_Boolean_Connectives|Section 5.4]], an enumeration from [[#Semantic_Conditions_for_Enumerations|Section 5.5]], a property restriction from [[#Semantic_Conditions_for_Property_Restrictions|Section 5.6]], or a datatype restriction from [[#Semantic_Conditions_for_Datatype_Restrictions|Section 5.7]]). Since ''G<sub>1</sub>'' is OWL 2 balanced w.r.t. ''G<sub>2</sub>'', ''g<sub>E</sub>'' also occurs in ''G<sub>1</sub>''. Since ''I'' OWL 2 Full satisfies ''G<sub>1</sub>'', ''g<sub>E</sub>'' is OWL 2 Full satisfied, either, taking into account that blank nodes are existential variables. Hence, the left-to-right direction of the respective semantic condition for the particular sort of expression can be applied. This can be done for all the expressions occurring in ''g<sub>A</sub>'', and ''g<sub>A</sub>'' can be seen as a directed acyclic graph with the triples encoding the actual axiom on top, and the different component expressions being connected via blank nodes. Eventually, one can see that all the premises of the right-to-left direction of the semantic condition for the axiom encoded by ''g<sub>A</sub>'' hold.
  
Line 4,483: Line 4,467:
 
since the [http://www.w3.org/TR/2008/WD-owl2-rdf-based-semantics-20081202/ Second Public Working Draft].
 
since the [http://www.w3.org/TR/2008/WD-owl2-rdf-based-semantics-20081202/ Second Public Working Draft].
  
* The [[#tab-semcond-properties|domain of <span class="name">owl:propertyChain</span>]] has been relaxed to IR (was IP), since the left hand side of a sub property axiom is only considered a "root node".
 
 
* The [[#Introduction_.28Informative.29|"Introduction" section]] has been revised.
 
* The [[#Introduction_.28Informative.29|"Introduction" section]] has been revised.
 
* All references to the term "URI" have been replaced by the term "IRI" [<cite>[[#ref-rfc-3987|RFC 3987]]</cite>], following the rest of the OWL 2 documents. This is a backwards-compatible deviation from the RDF Semantics, which used the term URI according to [<cite>[[#ref-rfc-2396|RFC 2396]]</cite>].  
 
* All references to the term "URI" have been replaced by the term "IRI" [<cite>[[#ref-rfc-3987|RFC 3987]]</cite>], following the rest of the OWL 2 documents. This is a backwards-compatible deviation from the RDF Semantics, which used the term URI according to [<cite>[[#ref-rfc-2396|RFC 2396]]</cite>].  
Line 4,521: Line 4,504:
 
* Splitted "Axiomatic Triples" section into subsections.
 
* Splitted "Axiomatic Triples" section into subsections.
 
* Changed use of term "lexical value" to "lexical form" according to [http://www.w3.org/2009/02/24-owl-irc#T22-14-33 WG Resolution] on [http://lists.w3.org/Archives/Public/public-owl-comments/2009Jan/0007.html LC Comment 16] ("lexical value").
 
* Changed use of term "lexical value" to "lexical form" according to [http://www.w3.org/2009/02/24-owl-irc#T22-14-33 WG Resolution] on [http://lists.w3.org/Archives/Public/public-owl-comments/2009Jan/0007.html LC Comment 16] ("lexical value").
 +
* Changed RDF encoding of sub property chain axioms to single triple form according to [http://www.w3.org/2009/02/24-owl-irc#T16-34-32-1 WG Resolution] with [http://www.w3.org/2009/02/24-owl-irc#T16-33-31 addendum] on [http://lists.w3.org/Archives/Public/public-owl-comments/2009Jan/att-0051/index.html LC Comment 34] (TQ / "Property chain inclusion axioms").
  
 
</div>
 
</div>

Revision as of 04:15, 25 February 2009

__NUMBEREDHEADINGS__

[Hide Review Comments]

Document title:
OWL 2 Web Ontology Language
RDF-Based Semantics (Second Edition)
Editor
Michael Schneider, FZI Research Center for Information Technology
Contributors (alphabetical order)
Jeremy Carroll, HP (now at TopQuadrant)
Peter F Patel-Schneider, Bell Labs Research, Alcatel-Lucent
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 the RDF-compatible model-theoretic semantics for OWL 2, called OWL 2 Full.
Status of this Document
This is an editors' draft of a Recommendation-Track document.
The OWL Working Group solicits feedback on how to improve and update this document.

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

Contents

Editor's Note: It will be considered to give the name "OWL 2 Full" to the whole language consisting of syntax and semantics, instead of only the semantics.
Editor's Note: The WG will reconsider the nameing scheme for the different languages, their syntaxes and semantics.
Editor's Note: Reconsider the use of the terms "RDF universe" and "OWL 2 Full universe".
Editor's Note: Change all RDF examples to the serialization syntax used in the other documents. Add Citation to used RDF Serializaton.

1 Introduction (Informative)

This document defines the RDF-based model-theoretic semantics of OWL 2, called OWL 2 Full. OWL 2 Full provides a semantics for OWL 2 that is fully compatible with the semantics presented in the RDF Semantics specification [RDF Semantics], and that allows for interpreting arbitrary RDF graphs [RDF Concepts].

Technically, OWL 2 Full is defined as a semantic extension of RDFS with datatype support ("D-Entailment"), as specified in [RDF Semantics]. In other words, the semantic meaning given to an RDF graph by OWL 2 Full includes the meaning given to the graph by the semantics of RDFS with datatypes, and additional meaning is given to all the language features of OWL 2, such as boolean connectives, sub property chains and qualified cardinality restrictions. The definition of the semantics for the extra features follows the same design principles that have been applied to the RDF semantics.

The content of this document is not meant to be self-contained, but builds on top of the RDF Semantics document [RDF Semantics] by adding only those aspects that are specific to OWL 2. Hence, the complete definition of OWL 2 Full is given by the combination of both the RDF Semantics document and the OWL 2 RDF-Based Semantics document. In particular, the terminology used in the RDF Semantics is reused in the document at hand, except for cases where a conflict exists with the rest of the OWL 2 specification.

The following paragraphs outline this document's structure and content, and provide an overview of some of the distinguishing features of OWL 2 Full.

Every RDF graph [RDF Concepts] is an OWL 2 Full ontology (Section 2), and is given a precise semantic meaning by the OWL 2 Full semantics. OWL 2 Full provides vocabulary interpretations [RDF Semantics] for the RDF and RDFS vocabularies and for the OWL 2 Full vocabulary (Section 3). The OWL 2 Full vocabulary is a set of IRI references [RFC 3987], which occur in the sets of RDF triples that define the RDF syntax of OWL 2 [OWL 2 RDF Mapping].

OWL 2 Full vocabulary interpretations (Section 4) are defined on the OWL 2 Full universe, which is, as in RDF, a set of resources. The OWL 2 Full universe is divided into parts, namely individuals, classes, and properties, which are identified with their RDF counterparts. In particular, the part of individuals equals the whole OWL 2 Full universe. This means that all classes and properties are also individuals on their own right.

The three basic parts are further divided into subparts as follows. The part of individuals subsumes the part of data values, which comprises the denotations of all literals. Also subsumed by the individuals is the part of ontologies. The part of classes subsumes the part of datatypes, which are classes entirely consisting of data values. And finally, the part of properties subsumes the parts of object properties, data properties, annotation properties and ontology properties. In particular, the part of object properties equals the whole part of properties, and all other kinds of properties are therefore also object properties.

For the particular case of annotations properties it is important to note that annotations cannot really be regarded as "semantic-free comments" in OWL 2 Full. Just like every other triple or set of triples occurring in an RDF graph, an annotation is actually an interpreted assertion that denotes a truth value under the OWL 2 Full semantics. This means that adding an annotation may change the semantic meaning of an OWL 2 Full ontology. An analog discussion holds for statements that are built from ontology properties.

Every class represents a specific set of individuals, called the class extension of the class: an individual a is an instance of a given class C, exactly if a is a member of the class extension of C, written as "ICEXT(C)". Since a class is itself an individual in OWL 2 Full, classes are distinguished from their respective class extensions. This distinction allows, for example, for a class to be an instance of itself by being a member of its own class extension. Also, two classes may be equivalent by sharing the same class extension, though still being different individuals (i.e., they do not need to share the same properties). Similarly, every property has a property extension associated with it, consisting of pairs of individuals: an individual a1 has a relationship to another individual a2 based on a given property p, exactly if the pair 〈 a1 , a2 〉 is a member of the property extension of p, written as "IEXT(p)".

Individuals may play different roles in an OWL 2 Full ontology. For example, an individual can be both a data property and an annotation property, since the different parts of the OWL 2 Full universe are not required to be mutually disjoint. Or an individual can be both a class and a property, since a class extension and a property extension may independently be associated with the same individual.

The actual semantics of OWL 2 Full is specified by the set of OWL 2 Full semantic conditions (Section 5), which extend all the semantic conditions given in [RDF Semantics]. The OWL 2 Full semantic conditions effectively determine which sets of RDF triples are assigned a specific meaning, and what this meaning is. For example, there exist semantic conditions that allow to interpret the RDF triple "C owl:disjointWith D" to mean that the denotations of the IRI references "C" and "D" have disjoint class extensions.

There is usually no need to provide localizing information (e.g. by means of "typing triples") for the IRI references occurring in an OWL 2 Full ontology. As for the RDF semantics, the OWL 2 Full semantic conditions have been designed to ensure that the denotation of any IRI reference will actually be in the appropriate part of the OWL 2 universe. For example, the RDF triple "C owl:disjointWith D" is sufficient to deduce that the denotations of the IRI references "C" and "D" are actually classes. It is not necessary to explicitly add additional typing triples "C rdf:type rdfs:Class" and "D rdf:type rdfs:Class" to the ontology.

In the RDF semantics, this kind of "automatic localization" was to some extend achieved by so called "axiomatic triples" [RDF Semantics], such as "rdfs:subClassOf rdf:type rdf:Property" or "rdfs:subClassOf rdfs:domain rdfs:Class". However, there is no explicit collection of additional axiomatic triples for OWL 2 Full but, instead, the specific axiomatic aspects of OWL 2 Full are determined by a subset of the OWL 2 Full semantic conditions. Section 6 discusses axiomatic triples in general, and presents one possible set of axiomatic triples, which is compatible with the OWL 2 Full semantic conditions.

Section 7 compares OWL 2 Full with the OWL 2 Direct Semantics, which is based on a particular description logic according to [OWL 2 Direct Semantics]. Several fundamental differences that exist between the two semantics are discussed in the section. However, a strong relationship will be presented, showing that OWL 2 Full is able to reflect all logical conclusions of the OWL 2 Direct Semantics. This means that the OWL 2 Direct Semantics can in a sense be regarded as a sub language of OWL 2 Full. The precise relationship is stated by the OWL 2 correspondence theorem in Section 7.3.

Significant effort has been spent in keeping the design of OWL 2 Full as close as possible to that of the original specification of OWL Full [OWL Full]. While this aim was achieved to a wide degree, OWL 2 Full deviates from OWL Full in several relevant aspects. One important change is that, while there still exist comprehension conditions for OWL 2 Full, these are not part of the normative collection of OWL 2 Full semantic conditions anymore. OWL 2 Full also corrects several errors of OWL Full. A list of differences between the two languages is given in Section 8.

The italicized keywords MUST, MUST NOT, SHOULD, SHOULD NOT, and MAY are used to specify normative features of OWL 2 documents and tools, and are interpreted as specified in RFC 2119 [RFC 2119].

2 Ontologies

This section determines the syntax of OWL 2 Full, and specifies what an OWL 2 Full ontology is. There will also be a note on the typical content an OWL 2 Full ontology MAY have.

2.1 Syntax

Following Sections 0.2 and 0.3 of the RDF Semantics specification [RDF Semantics], the semantics of OWL 2 Full is defined on every RDF graph (Section 6.2 of [RDF Concepts]), i.e. on every set of RDF triples (Section 6.1 of [RDF Concepts]).

In accordance with the rest of the OWL 2 specification (see Section 2.3 of [OWL 2 Specification]), this document uses an extended notion of an RDF graph by allowing the RDF triples in an RDF graph to contain arbitrary IRI references ("Internationalized Resource Identifiers") according to [RFC 3987]. In contrast, the RDF Semantics specification [RDF Semantics] is defined on RDF graphs containing URI references [RFC 2396]. This deviation from the RDF Semantics specification is backwards compatible with both the RDF specification and with the original specification of OWL Full [OWL Full].

In this document, IRI references are abbreviated as a CURIE [CURIE] consisting of a namespace prefix and a local part, such as "prefix:localpart".

The definition of an RDF triple in Section 6.1 of [RDF Concepts] is restricted to cases where the subject of an RDF triple is a URI or a blank node (Section 6.6 of [RDF Concepts]), and where the predicate of an RDF triple is a URI. As a consequence, the definition does not treat cases, where, for example, the subject of a triple is a literal (Section 6.5 of [RDF Concepts]), as in "s" ex:p ex:o, or where the predicate of a triple is a blank node, as in ex:s _:p ex:o. In order to allow for interoperability with other existing or future standards and tools, the document at hand does not explicitly forbid RDF graphs to contain generalized RDF triples, which are defined to allow for IRI references, literals and blank nodes to occur in the subject, predicate and object position. Thus, an RDF graph MAY contain generalized RDF triples.

A word on nomenclature: OWL 2 Full is considered an ontology language, therefore the term "OWL 2 Full ontology" will be used interchangeably with the term "RDF graph" in this document.

2.2 Content of Ontologies (Informative)

While there do not exist any syntactic restrictions on the set of RDF graphs that can be OWL 2 Full ontologies, in practice an OWL 2 Full ontology will often contain certain kinds of components that are aimed to support ontology management tasks. Examples are ontology headers and ontology IRI references, as well as components that are about versioning, importing and annotating of ontologies, including the concept of incompatibility between ontologies.

These topics are outside the scope of this semantics specification. Section 3 of [OWL 2 Structural Spec] deals with these topics in greater detail, and can therefore be used as a guide on how to apply these compontents in OWL 2 Full ontologies accordingly. The mappings of all these components to their respective RDF encodings are defined in [OWL 2 RDF Mapping].

Be informed, however, that none of the restrictions defined in Section 3 of [OWL 2 Structural Spec] have any normative relevance for OWL 2 Full, since they would have the potential to restrict the set of syntactically valid OWL 2 Full ontologies, and would thus be in conflict with the definitions provided in the document at hand.

3 Vocabulary

This section specifies the OWL 2 Full vocabulary, and lists the names of the datatypes and facets used in OWL 2 Full.

3.1 Namespaces

Table 3.1 lists the namespace prefixes and the respective IRI references of the namespaces referred to in this document.

Table 3.1: Namespaces
Namespace Prefix IRI Reference
OWL owl http://www.w3.org/2002/07/owl#
RDF rdf http://www.w3.org/1999/02/22-rdf-syntax-ns#
RDFS rdfs http://www.w3.org/2000/01/rdf-schema#
XML Schema xsd http://www.w3.org/2001/XMLSchema#

3.2 Vocabulary Terms

Table 3.2 lists the OWL 2 Full vocabulary, which extends the RDF and RDFS vocabulary as specified by Sections 3.1 and 4.1 of [RDF Semantics]. The OWL 2 Full vocabulary is a set of IRI references [RFC 3987] in the OWL namespace with the namespace prefix owl (see Section 3.1). Table 3.2 excludes those IRI references from the OWL namespace, which are mentioned in either Section 3.3 on datatype names or Section 3.4 on facet names.

Table 3.2: OWL 2 Full Vocabulary
owl:AllDifferent owl:AllDisjointClasses owl:AllDisjointProperties owl:allValuesFrom owl:Annotation owl:AnnotationProperty owl:assertionProperty owl:AsymmetricProperty owl:Axiom owl:backwardCompatibleWith owl:bottomDataProperty owl:bottomObjectProperty owl:cardinality owl:Class owl:complementOf owl:DataRange owl:datatypeComplementOf owl:DatatypeProperty owl:deprecated owl:DeprecatedClass owl:DeprecatedProperty owl:differentFrom owl:disjointUnionOf owl:disjointWith owl:distinctMembers owl:equivalentClass owl:equivalentProperty owl:FunctionalProperty owl:hasKey owl:hasSelf owl:hasValue owl:imports owl:incompatibleWith owl:intersectionOf owl:InverseFunctionalProperty owl:inverseOf owl:IrreflexiveProperty owl:maxCardinality owl:maxQualifiedCardinality owl:members owl:minCardinality owl:minQualifiedCardinality owl:NamedIndividual owl:NegativePropertyAssertion owl:Nothing owl:object owl:ObjectProperty owl:onClass owl:onDataRange owl:onDatatype owl:oneOf owl:onProperty owl:onProperties owl:Ontology owl:OntologyProperty owl:predicate owl:priorVersion owl:propertyChainAxiom owl:propertyDisjointWith owl:qualifiedCardinality owl:ReflexiveProperty owl:Restriction owl:sameAs owl:someValuesFrom owl:sourceIndividual owl:subject owl:SymmetricProperty owl:targetIndividual owl:targetValue owl:Thing owl:topDataProperty owl:topObjectProperty owl:TransitiveProperty owl:unionOf owl:versionInfo owl:withRestrictions

Note: The use of the IRI reference owl:DataRange has been deprecated as of OWL 2. The IRI reference rdfs:Datatype SHOULD be used instead.

3.3 Datatype Names

Table 3.3 lists the IRI references of the datatypes of OWL 2 Full. The normative set of datatypes for OWL 2 Full equals the set of datatypes described in Section 4 of [OWL 2 Specification]. The meaning of rdf:XMLLiteral is described in Section 3.1 of [RDF Semantics]. rdf:text is described in [RDF:TEXT]. All other datatypes are described in Section 4 of [OWL 2 Specification].

Table 3.3: Datatypes of OWL 2 Full
xsd:anyURI xsd:base64Binary xsd:boolean xsd:byte xsd:dateTimeStamp xsd:decimal xsd:double xsd:float xsd:hexBinary xsd:int xsd:integer xsd:language xsd:long xsd:Name xsd:NCName xsd:negativeInteger xsd:NMTOKEN xsd:nonNegativeInteger xsd:nonPositiveInteger xsd:normalizedString xsd:positiveInteger owl:rational owl:real owl:realPlus xsd:short xsd:string rdf:text xsd:token xsd:unsignedByte xsd:unsignedInt xsd:unsignedLong xsd:unsignedShort rdf:XMLLiteral

Feature At Risk #1: owl:rational support

Note: This feature is "at risk" and may be removed from this specification based on feedback. Please send feedback to public-owl-comments@w3.org. For the current status see features "at risk" in OWL 2

The owl:rational datatype might be removed from OWL 2 if implementation experience reveals problems with supporting this datatype.

Feature At Risk #2: owl:dateTime name

The name owl:dateTime was previously used as a placeholder. XML Schema 1.1 Working Group has introduced a datatype for date-time with required timezone. This datatype was changed to the new datatype, xsd:dateTimeStamp. If the XML Schema WG proceeds as planned, this section may be removed.

Please send feedback to public-owl-comments@w3.org.

3.4 Facet Names

Table 3.4 lists the IRI references of the facets of OWL 2 Full. The normative set of facets for OWL 2 Full equals the set of facets described in Section 4 of [OWL 2 Specification]. The meaning of each facet, to which datatypes it can be applied, and which values it can take for a given datatype is described in Section 4 of [OWL 2 Specification] The facet rdf:langPattern is further described in [RDF:TEXT].

Table 3.4: Datatype Facets of OWL 2 Full
rdf:langPattern xsd:length xsd:maxExclusive xsd:maxInclusive xsd:maxLength xsd:minExclusive xsd:minInclusive xsd:minLength xsd:pattern

4 Interpretations

OWL 2 Full provides vocabulary interpretations and vocabulary entailment (see Section 2.1 of [RDF Semantics]) for the RDF and RDFS vocabularies and for the OWL 2 Full vocabulary. This section defines what a OWL 2 Full datatype map and a OWL 2 Full interpretation is, and what satisfaction of OWL 2 Full ontologies, consistency and entailment means under the OWL 2 Full semantics. In addition, the so called "parts" of the OWL 2 Full universe will be defined.

4.1 Datatype Maps

According to Section 5.1 of the RDF semantics specification [RDF Semantics], a datatype d has the following components:

  • LS(d), the lexical space of d, which is a non-empty set of lexical forms.
  • VS(d), the value space of d, which is a non-empty set of data values.
  • L2V(d), the lexical-to-value mapping of d, which maps lexical forms in LS(d) to data values in VS(d).

Terminological notes: The document at hand uses the term "data value" in accordance with the rest of the OWL 2 specification (see Section 4 of [OWL 2 Specification]), where the RDF semantics specification [RDF Semantics] uses the term "datatype value" instead. Further, the names "LS" and "VS", which stand for the lexical space and the value space of a datatype, respectively, are not used in the RDF semantics specification [RDF Semantics], but have been introduced here for easier reference.

Further, Section 5.1 of the RDF semantics specification [RDF Semantics] defines a datatype map D to be a set of pairs 〈 u , d 〉 consisting of an IRI reference u and a datatype d, such that no IRI reference appears twice in the set.

In this document, the basic definition of a datatype is extended to take facets into account. Note that Section 5.1 of the RDF semantics specification [RDF Semantics] explicitly permits to semantic extensions of RDF to impose more elaborate datatyping conditions than those listed above.

A datatype with facets, d, is a datatype that has the following additional components:

  • FS(d), the facet space of d, which is a possibly empty set of pairs 〈 F , v 〉, called facet-value pairs, where F is an IRI reference called a constraining facet, and v is an arbitrary object called a value.
  • F2V(d), the facet-to-value mapping of d, which maps each pair 〈 F , v 〉 in the facet space FS(d) to a subset of the value space VS(d).
Editor's Note: There is an LC Comment asking what it means in the Structural Specification that the values of facets are "arbitrary objects". (LC Comment at http://lists.w3.org/Archives/Public/public-owl-comments/2009Jan/0006.html)

Note that the value v of a facet-value pair 〈 F , v 〉 contained in the facet space FS(d) of a datatype d does not need to be included in the value space VS(d) of d itself. For example, the datatype xsd:string (Section 3.3) has the facet xsd:length (Section 3.4), which takes non-negative integers as its values, rather than strings. Hence, in general, all the datatypes of the values of facets need to be available, either.

In this document, it will always be assumed from now on that every datatype d is a datatype with facets. In particular, every datatype map D will entirely consist of datatypes with facets. If the facet space FS(d) of a datatype d has not been explicitly defined, or is not derived from another datatype's facet space according to some well defined condition, then FS(d) is the empty set. Unless there is any risk of confusion, the term "datatype" will always refer to a datatype with facets.

The following definition specifies what an OWL 2 Full datatype map is.

Definition 4.1 (OWL 2 Full Datatype Map): Let D be a datatype map. D is an OWL 2 Full datatype map, if it contains at least every datatype d having its name listed in Section 3.3, with its respective lexical space LS(d), value space VS(d), lexical-to-value mapping L2V(d), facet space FS(d) and facet-to-value mapping F2V(d) specified according to the definitions in Section 4 of [OWL 2 Specification] (for the facets listed in Section 3.4).

Note for the special case of an OWL 2 Full datatype map D that exclusively consists of the datatypes having their names listed in Section 3.3, it is ensured that there are datatypes available for all the facet values, i.e., for every datatype d in D and for every facet-value pair 〈 F , v 〉 in the facet space FS(d) there exists a datatype d* in D that contains v in its value space VS(d*), together with a lexical form a in the lexical space LS(d*) with L2V(d*)(a) = v.

4.2 Vocabulary Interpretations

From the RDF semantics specification [RDF Semantics], let V be a set of IRI references and literals containing the RDF and RDFS vocabularies, and let D be a datatype map according to Section 5.1 of [RDF Semantics] (and accordingly Section 4.1). A D-interpretation I of V with respect to D is a tuple

I = 〈 IR , IP , IEXT , IS , IL , LV 〉 .

IR is the OWL 2 Full universe, i.e., a nonempty set that contains the denotations of IRI references and literals in V. IP is a subset of IR, the properties of I. LV, the data values of I, is a subset of IR that contains at least the set of plain literals (see Section 6.5 of [RDF Concepts]), and the value spaces for each datatype in D. IEXT is used to associate properties with their property extension, and is a mapping from IP to P(IR × IR), where P is the powerset. IS is a mapping from IRI references in V to their denotations in IR. In particular, IS(u) = d for any datatype d and its name u in D. IL is a mapping from typed literals "sss"^^ddd in V to their denotations in IR, where IL("sss"^^ddd) = L2V(d)(sss), provided that d is a datatype in D, I(ddd) = d, and sss is in the lexical space LS(d); otherwise IL("sss"^^ddd) is not in LV.

As detailed in [RDF Semantics], a D-interpretation has to meet all the semantic conditions for ground graphs and blank nodes, those for RDF interpretations and RDFS interpretations, and the "general semantic conditions for datatypes".

In this document, the basic definition of a D-interpretation is extended to take facets into account.

A D-interpretation with facets, I, is a D-interpretation for a datatype map D consisting entirely of datatypes with facets (Section 4.1), where I meets the following additional semantic conditions. For each datatype d in D and for each facet-to-value pair 〈 F , v 〉 in the facet space FS(d):

  • the vocabulary V of I contains the facet IRI reference F;
  • the vocabulary V of I contains a literal "sss"^^ddd*, if a datatype d* is available, such that ddd* is the IRI reference of d*, sss is in the lexical space LS(d*), the value v is in the value space VS(d*), and L2V(d*)(sss) = v.
Editor's Note: Check whether the second extra condition is ok.

Note that these extra semantic conditions are weak in several respects.

First, it is not further specified of what kind the denotation of a facet name is, i.e. it is only known that a facet name denotes some individual. The definition of datatypes with facets in (Section 4.1) does not suggest a certain kind of objects. Semantic extensions MAY impose further restrictions on the denotations of facets.

Second, the extra semantic conditions do not require the datatype map D of a D-interpretation to include all the datatypes d* covering all the facet values v for each datatype d in D and for each facet-value pair 〈 F , v 〉 in the facet space FS(d). However, if D contains a datatype d* for some value v in a facet-value pair, then it is ensured, by both the "general semantic conditions for datatypes", as given in Section 5.1 of [RDF Semantics], and the extra semantic conditions on D-interpretations with facets that v is contained in the set LV of I, and that there exists a typed literal "sss"^^ddd* in the vocabulary V of I, such that IL("sss"^^ddd*) = v for the mapping IL of I.

In this document, it will always be assumed from now on that every D-interpretation I is a D-interpretation with facets. Unless there is any risk of confusion, the term "D-interpretation" will always refer to a D-interpretation with facets.

The following definition specifies what an OWL 2 Full interpretation is.

Definition 4.2 (OWL 2 Full Interpretation): Let D be an OWL 2 Full datatype map, and let V be a vocabulary that includes the RDF and RDFS vocabularies and the OWL 2 Full vocabulary together with all the datatype and facet names listed in Section 3. An OWL 2 Full interpretation, I = 〈 IR , IP , IEXT , IS , IL , LV 〉, of V with respect to D, is a D-interpretation of V with respect to D that meet all the extra semantic conditions given in Section 5.

Note for the special case of an OWL 2 Full interpretation w.r.t. a datatype map D that exclusively consists of the datatypes having their names listed in Section 3.3, it is ensured that every value v occurring in a facet-value pair 〈 F , v 〉 in the facet space FS(d) of any datatype d in D will be contained in the value space VS(d*) of some datatype d* in D (see the last paragraph in Section 4.1). As a result, every value v in a facet-value pair will be included in the set LV, and a typed literal "sss"^^ddd* will exist in in the vocabulary V of I, such that IL("sss"^^ddd*) = v (see the notes on the extra semantic conditions of D-interpretations above).

4.3 Satisfaction, Consistency and Entailment

The notion of satisfaction in OWL 2 Full is based on the notion of satisfaction for D-intepretations and Simple interpretations, as defined in [RDF Semantics]. In essence, in order to satisfy an RDF graph, an interpretation I has to satisfy all the triples in the graph, i.e., for a triple of the form "s p o" it is necessary that the relationship 〈 I(s) , I(o) 〉 ∈ IEXT(I(p)) holds (special treatment is necessary for blank nodes, as detailed in Section 1.5 of [RDF Semantics]). With other words, the given graph has to be compatible with the IEXT mapping of the interpretation I. The main distinguishing aspect of "OWL 2 Full satisfaction" is that an interpretation I needs to meet all the OWL 2 Full semantic conditions (Section 5), which actually constraint the possible forms the mapping IEXT of I can have.

Definition 4.3 (OWL 2 Full Satisfaction): Let K be a collection of RDF graphs, let D be an OWL 2 Full datatype map, let V be a vocabulary that includes the RDF and RDFS vocabularies and the OWL 2 Full vocabulary together with all the datatype and facet names listed in Section 3, and let I be a D-interpretation of V with respect to D. I OWL 2 Full satisfies K with respect to V and D iff I is an OWL 2 Full interpretation of V with respect to D that satisfies K as a D-interpretation of V with respect to D according to [RDF Semantics].

The following definitions specify what a consistent OWL 2 Full ontology is, and what it means that an OWL 2 Full ontology entails another OWL 2 Full ontology.

Definition 4.4 (OWL 2 Full Consistency): Let K be a collection of RDF graphs, and let D be an OWL 2 Full datatype map. K is OWL 2 Full consistent with respect to D iff there is some OWL 2 Full interpretation with respect to D (of some vocabulary that includes the RDF and RDFS vocabularies and the OWL 2 Full vocabulary together with all the datatype and facet names listed in Section 3) that OWL 2 Full satisfies all the RDF graphs in K.

Definition 4.5 (OWL 2 Full Entailment): Let K and Q be collections of RDF graphs, and let D be an OWL 2 Full datatype map. K OWL 2 Full entails Q with respect to D iff every OWL 2 Full interpretation with respect to D (of any vocabulary V that includes the RDF and RDFS vocabularies and the OWL 2 Full vocabulary together with all the datatype and facet names listed in Section 3) that OWL 2 Full satisfies all the RDF graphs in K also OWL 2 Full satisfies all the RDF graphs in Q.

4.4 Parts of the Universe

Table 4.1 defines the "parts" of the OWL 2 Full universe.

The first column tells the name of the part. The second column gives a definition of the part in terms of the mapping IEXT of an OWL 2 Full interpretation, and by referring to the RDF, RDFS and OWL 2 Full vocabularies. The third column notes what the defined part is meant to be.

As an example, the part of all datatypes is named "IDC", and it is defined as the set of all resources x for which the relationship "〈 x , I(rdfs:Datatype) 〉 ∈ IEXT(I(rdf:type))" holds. According to the semantics of rdf:type, as defined in Section 4.1 of [RDF Semantics], this actually means that the name "IDC" denotes the set of all members of the class extension of rdfs:Datatype.

Table 4.1: Parts of the OWL 2 Full Universe
Name of
Part S
Definition of S as
{ x ∈ IR | 〈 x , I(E) 〉 ∈ IEXT(I(rdf:type)) }
where IRI Reference E is
Note
IR rdfs:Resource individuals
LV rdfs:Literal data values
IX owl:Ontology ontologies
IC rdfs:Class classes
IDC rdfs:Datatype datatypes
IP rdf:Property properties
IODP owl:DatatypeProperty data properties
IOAP owl:AnnotationProperty annotation properties
IOXP owl:OntologyProperty ontology properties

4.5 Class Extensions

For members of the part IC of classes, as defined in Section 4.4, the class extension will be defined in terms of the mapping IEXT of an OWL 2 Full interpretation and by referring to the RDF vocabulary.

The mapping ICEXT from IC to P(IR), that associates classes with their class extension, where P is the power set, is defined as

ICEXT(c) = { x ∈ IR | 〈 x , c 〉 ∈ IEXT(I(rdf:type)) }

for every c ∈ IC.

5 Semantic Conditions

Editor's Note: In table texts, say "Informative Note:", where necessary.
Editor's Note: Editorial: Consider better alignment of order of semantic conditions with Direct Semantics document.

This section defines the semantic conditions of OWL 2 Full. The semantic conditions presented here are only those for the specific features of OWL 2. The complete set of semantic conditions for OWL 2 Full is the combination of the semantic conditions presented here and the semantic conditions for Simple Entailment, RDF, RDFS and D-Entailment, as specified in [RDF Semantics].

Section 5.1 specifies semantic conditions for the different parts of the OWL 2 Full universe, which have been defined in Section 4.4. Section 5.2 and Section 5.3 list semantic conditions for the classes and the properties of the OWL 2 Full vocabulary. In the rest of this section, the OWL 2 Full semantic conditions for the different language features of OWL 2 are specified.

Conventions used in this Section

Conjunctive commas: A comma (",") that separates two assertions in a semantic condition, as in "c ∈ IC , p ∈ IP", is read as a logical "and". Further, a comma separating two variables, as in an expression such as "c, d ∈ IC", is used for abbreviating two comma separated assertions, "c ∈ IC , d ∈ IC" in this example.

Unscoped variables: If no scope is explicitly given for a variable "x", as in "∀ x : …" or "{ x | … }", then x is unconstrained, which means that x ∈ IR, i.e. "x" denotes an arbitrary individual in the OWL 2 Full universe.

Sequence expressions: An expression of the form "s sequence of a1 , … , anS" means that s represents a list of n ≥ 0 elements, all of them being members of the set S. Precisely, s = I(rdf:nil) for n = 0, and for n > 0 there exist z1 ∈ IR , … , zn ∈ IR, such that

s = z1 ,
a1S , 〈 z1 , a1 〉 ∈ IEXT(I(rdf:first)) , 〈 z1 , z2 〉 ∈ IEXT(I(rdf:rest)) ,
… ,
anS, 〈 zn , an 〉 ∈ IEXT(I(rdf:first)) , 〈 zn , I(rdf:nil) 〉 ∈ IEXT(I(rdf:rest)) .

Set names: The following names for certain sets are used as convenient abbreviations:

  • ISEQ: The set of all sequences. This set equals the class extension of rdf:List, i.e., ISEQ := ICEXT(I(rdf:List)).
  • INNI: The set of all non-negative integers. This set equals the value space of xsd:NonNegativeInteger, i.e., INNI := ICEXT(I(xsd:NonNegativeInteger)), but is also subsumed by the value spaces of other numerical datatypes, such as xsd:integer.

Notes on the Form of Semantic Conditions (Informative)

One design goal behind the definition of the semantic conditions for OWL 2 Full was to ensure an appropriate degree of alignment between the semantics of OWL 2 Full and the OWL 2 Direct Semantics [OWL 2 Direct Semantics]. The way this semantic alignment is actually described is via the OWL 2 Correspondence Theorem in Section 7.3. For this theorem to hold, the semantic conditions that treat the RDF encodings of axioms (Section 3.2.5 of [OWL 2 RDF Mapping]) in OWL 2 DL (Section 9 of [OWL 2 Specification]), such as inverse property axioms, must have the form of "iff" ("if-and-only-if") conditions. This means that these semantic conditions completely determine the semantics of these feature encodings. On the other hand, the RDF encodings of descriptions (Section 3.2.4 of [OWL 2 RDF Mapping]) in OWL 2 DL (Sections 6 - 8 of [OWL 2 Specification]), such as property restrictions, are treated by "if-then" conditions. These weaker semantic conditions for expressions are sufficient for the correspondence theorem to hold, so there is no necessity to define stronger "iff" conditions in OWL 2 Full for these language features.

Special cases are the semantic conditions for boolean connectives of classes and enumerations of individuals. These language features actually build expressions in OWL 2 DL. However, for backwards compatibility reasons there are also RDF encodings of axioms based on the vocabulary for these language features (see Table 18 in Section 3.2.5 of [OWL 2 RDF Mapping]). For example, an RDF expression of the form

ex:c1 owl:unionOf (SEQ ex:c2 ex:c3)

is allowed to occur in an OWL 2 DL ontology in RDF graph form, and encodes an axiom that states the equivalence of the class denoted by ex:c1 with the union of the classes denoted by ex:c2 and ex:c3. So, in order to ensure that the correspondence theorem holds, and in accordance with the original OWL Full specification [OWL Full], the semantic conditions for the mentioned language features are "iff" conditions.

Further, special treatment exists for axioms that have a multi-triple representation in RDF, where the different triples share a common "root node", such as the blank node "_:x" in the example

_:x rdf:type owl:AllDisjointClasses
_:x owl:members (SEQ ex:c1 ex:c2)

In essence, the semantic conditions for the encodings of these language features are "iff" conditions, as usual for axioms. However, in order to cope with the specific syntactic aspect of a "root node", the "iff" conditions of these language features have been split into two "if-then" conditions, where the "if-then" condition representing the right-to-left direction contains an additional premise of the form "∃ z ∈ IR". The single purpose of this premise is to ensure the existence of an individual that is needed to satisfy the root node under the OWL 2 Full semantics. The language features in question are n-ary axioms in Section 5.11, and negative property assertions in Section 5.15.

The "if-then" semantic conditions in this section sometimes do not explicitly list typing statements in their consequent that one might expect. For example, the semantic condition for owl:allValuesFrom restrictions in Section 5.6 does not list the statement "x ∈ ICEXT(I(owl:Restriction))" on its right hand side. Consequences are generally not mentioned, if they can already be deduced by other means. Often, these redundant consequences follow from the semantic conditions for classes and properties in Section 5.2 and Section 5.3, occasionally in connection with the semantic conditions for the parts of the OWL 2 Full universe in Section 5.1. In the example above, the omitted consequence can be obtained from the third column of the entry for owl:allValuesFrom in the table in Section 5.3, which determines that IEXT(I(owl:allValuesFrom)) ⊆ ICEXT(I(owl:Restriction)) × IC.

5.1 Semantic Conditions for the Parts of the Universe

Table 5.1 lists the semantic conditions for the parts of the OWL 2 Full universe, as defined in Section 4.4.

The first column tells the name of the part. The second column defines certain conditions on the part. In most cases, it is specified for the part by which other part it is subsumed, and by this the position of the part in the "parts hierarchy" of the OWL 2 Full universe is narrowed down. The third column provides further information about the instances of those parts that consist of classes or properties. In general, if the part consists of classes, then it is specified for the class extensions of the member classes by which part of the OWL 2 Full universe they are subsumed. If the part consists of properties, then the domains and ranges of the member properties are determined.

Table 5.1: Semantic Conditions for the Parts of the OWL 2 Full Universe
Name of
Part S
Conditions on S Conditions on
Instances x of S
IR S ≠ ∅
LV S ⊆ IR
IX S ⊆ IR
IC S ⊆ IR ICEXT(x) ⊆ IR
IDC S ⊆ IC ICEXT(x) ⊆ LV
IP S ⊆ IR IEXT(x) ⊆ IR × IR
IODP S ⊆ IP IEXT(x) ⊆ IR × LV
IOAP S ⊆ IP IEXT(x) ⊆ IR × IR
IOXP S ⊆ IP IEXT(x) ⊆ IX × IX

5.2 Semantic Conditions for Classes

Table 5.2 lists the semantic conditions for the classes of the OWL 2 Full vocabulary, and certain classes from RDF and RDFS.

The first column tells the name of the class. The second column defines of what particular kind a class is, i.e. whether it is a general class (a member of the part IC) or a datatype (a member of IDC). The third column specifies for the class extension of the class by which part of the OWL 2 Full universe (Section 4.4) it is subsumed. Thus, from an entry of the form "ICEXT(I(C)) ⊆S", for a class name C and a set S, and given an RDF triple of the form "u rdf:type C" one can deduce that I(u) ∈ S holds.

Not included in this table are the datatypes of OWL 2 Full, as given in Section 3.3. For each datatype IRI reference E, the following semantic conditions hold:

  • I(E) ∈ IDC
  • ICEXT(I(E)) ⊆ LV

As a specific note: For owl:NamedIndividual that there is no way in OWL 2 Full to restrict the set of individuals to only those being named by an IRI reference, hence the extension of this class has been specified to equal the whole domain.

Table 5.2: Semantic Conditions for Classes
IRI Reference E I(E) ICEXT(I(E))
owl:AllDifferent ∈ IC ⊆ IR
owl:AllDisjointClasses ∈ IC ⊆ IR
owl:AllDisjointProperties ∈ IC ⊆ IR
owl:Annotation ∈ IC ⊆ IR
owl:AnnotationProperty ∈ IC = IOAP
owl:AsymmetricProperty ∈ IC ⊆ IP
owl:Axiom ∈ IC ⊆ IR
rdfs:Class ∈ IC = IC
owl:Class ∈ IC = IC
owl:DataRange ∈ IC = IDC
rdfs:Datatype ∈ IC = IDC
owl:DatatypeProperty ∈ IC = IODP
owl:DeprecatedClass ∈ IC ⊆ IC
owl:DeprecatedProperty ∈ IC ⊆ IP
owl:FunctionalProperty ∈ IC ⊆ IP
owl:InverseFunctionalProperty ∈ IC ⊆ IP
owl:IrreflexiveProperty ∈ IC ⊆ IP
rdfs:Literal ∈ IDC = LV
owl:NamedIndividual ∈ IC = IR
owl:NegativePropertyAssertion ∈ IC ⊆ IR
owl:Nothing ∈ IC = ∅
owl:ObjectProperty ∈ IC = IP
owl:Ontology ∈ IC = IX
owl:OntologyProperty ∈ IC = IOXP
rdf:Property ∈ IC = IP
owl:ReflexiveProperty ∈ IC ⊆ IP
rdfs:Resource ∈ IC = IR
owl:Restriction ∈ IC ⊆ IC
owl:SymmetricProperty ∈ IC ⊆ IP
owl:Thing ∈ IC = IR
owl:TransitiveProperty ∈ IC ⊆ IP

5.3 Semantic Conditions for Properties

Table 5.3 lists the semantic conditions for the properties of the OWL 2 Full vocabulary and certain properties from RDFS.

The first column tells the name of the property. The second column defines of what particular kind a property is, i.e. whether it is a general property (a member of the part IP), a datatype property (a member of IODP), an ontology property (a member of IOXP) or an annotation property (a member of IOAP). The third column specifies the domain and range of the property. Thus, from an entry of the form "IEXT(I(p)) ⊆ S1 × S2", for a property name p and sets S1 and S2, and given an RDF triple of the form "s p o" one can deduce that I(s) ∈ S1 and I(o) ∈ S2 hold.

Not included in this table are the datatype facets of OWL 2 Full, as given in Section 3.4, which are used to specify datatype restrictions (see Section 5.7). For each facet IRI reference E, the following semantic conditions hold:

  • I(E) ∈ IP
  • IEXT(I(E)) ⊆ IR × LV

As specific notes:

owl:topObjectProperty relates every two individuals in the universe to each other. Likewise, owl:topDataProperty relates every individual to every datavalue. owl:bottomObjectProperty and owl:bottomDataProperty do not relate any individuals to each other at all.

The ranges of the properties owl:deprecated and owl:hasSelf are not restricted in any form, in particular, they are not restricted to be boolean values. The actual object values of these properties do not have any intended semantic meaning, but could have been defined to be of any value. Therefore, the semantics given here are of a form that the values can be arbitrarily chosen, without leading to any non-trivial semantic conclusions. It is, however, recommended to still use an object value of the form "true"^^xsd:boolean in OWL 2 Full ontologies, in order to not get in conflict with the required usage of these properties in OWL 2 DL (compare Table 13 in Section 3.2.4 of [OWL 2 RDF Mapping] for owl:hasSelf, and Section 5.5 of [OWL 2 Specification] for owl:deprecated).

Table 5.3: Semantic Conditions for Properties
IRI Reference E I(E) IEXT(I(E))
owl:allValuesFrom ∈ IP ⊆ ICEXT(I(owl:Restriction)) × IC
owl:assertionProperty ∈ IP ⊆ ICEXT(I(owl:NegativePropertyAssertion)) × IP
owl:backwardCompatibleWith ∈ IOXP ⊆ IX × IX
owl:bottomDataProperty ∈ IODP = ∅
owl:bottomObjectProperty ∈ IP = ∅
owl:cardinality ∈ IP ⊆ ICEXT(I(owl:Restriction)) × INNI
rdfs:comment ∈ IOAP ⊆ IR × LV
owl:complementOf ∈ IP ⊆ IC × IC
owl:datatypeComplementOf ∈ IP ⊆ IDC × IDC
owl:deprecated ∈ IOAP ⊆ IR × IR
owl:differentFrom ∈ IP ⊆ IR × IR
owl:disjointUnionOf ∈ IP ⊆ IC × ISEQ
owl:disjointWith ∈ IP ⊆ IC × IC
owl:distinctMembers ∈ IP ⊆ ICEXT(I(owl:AllDifferent)) × ISEQ
owl:equivalentClass ∈ IP ⊆ IC × IC
owl:equivalentProperty ∈ IP ⊆ IP × IP
owl:hasKey ∈ IP ⊆ IC × ISEQ
owl:hasSelf ∈ IP ⊆ ICEXT(I(owl:Restriction)) × IR
owl:hasValue ∈ IP ⊆ ICEXT(I(owl:Restriction)) × IR
owl:imports ∈ IOXP ⊆ IX × IX
owl:incompatibleWith ∈ IOXP ⊆ IX × IX
owl:intersectionOf ∈ IP ⊆ IC × ISEQ
owl:inverseOf ∈ IP ⊆ IP × IP
rdfs:isDefinedBy ∈ IOAP ⊆ IR × IR
rdfs:label ∈ IOAP ⊆ IR × LV
owl:maxCardinality ∈ IP ⊆ ICEXT(I(owl:Restriction)) × INNI
owl:maxQualifiedCardinality ∈ IP ⊆ ICEXT(I(owl:Restriction)) × INNI
owl:members ∈ IP ⊆ IR × ISEQ
owl:minCardinality ∈ IP ⊆ ICEXT(I(owl:Restriction)) × INNI
owl:minQualifiedCardinality ∈ IP ⊆ ICEXT(I(owl:Restriction)) × INNI
owl:object ∈ IP ⊆ IR × IR
owl:onClass ∈ IP ⊆ ICEXT(I(owl:Restriction)) × IC
owl:onDataRange ∈ IP ⊆ ICEXT(I(owl:Restriction)) × IDC
owl:onDatatype ∈ IP ⊆ IDC × IDC
owl:oneOf ∈ IP ⊆ IC × ISEQ
owl:onProperty ∈ IP ⊆ ICEXT(I(owl:Restriction)) × IP
owl:onProperties ∈ IP ⊆ ICEXT(I(owl:Restriction)) × ISEQ
owl:predicate ∈ IP ⊆ IR × IP
owl:priorVersion ∈ IOXP ⊆ IX × IX
owl:propertyChainAxiom ∈ IP ⊆ IP × ISEQ
owl:propertyDisjointWith ∈ IP ⊆ IP × IP
owl:qualifiedCardinality ∈ IP ⊆ ICEXT(I(owl:Restriction)) × INNI
owl:sameAs ∈ IP ⊆ IR × IR
rdfs:seeAlso ∈ IOAP ⊆ IR × IR
owl:someValuesFrom ∈ IP ⊆ ICEXT(I(owl:Restriction)) × IC
owl:sourceIndividual ∈ IP ⊆ ICEXT(I(owl:NegativePropertyAssertion)) × IR
owl:subject ∈ IP ⊆ IR × IR
owl:targetIndividual ∈ IP ⊆ ICEXT(I(owl:NegativePropertyAssertion)) × IR
owl:targetValue ∈ IP ⊆ ICEXT(I(owl:NegativePropertyAssertion)) × LV
owl:topDataProperty ∈ IODP = IR × LV
owl:topObjectProperty ∈ IP = IR × IR
owl:unionOf ∈ IP ⊆ IC × ISEQ
owl:versionInfo ∈ IOAP ⊆ IR × IR
owl:withRestrictions ∈ IP ⊆ IDC × ISEQ

5.4 Semantic Conditions for Boolean Connectives

Table 5.4 lists the semantic conditions for boolean connectives, including complements, intersections, and unions of classes. An intersection or union of a collection of datatypes is itself a datatype. While a complement of a class is created w.r.t. to the whole domain, a datatype complement is created for a datatype w.r.t. the set of data values only, and results itself in a datatype.

Informative note: The second, fourth and sixth semantic conditions are "iff" conditions, since the treated language features have the status of both class expressions and axioms in OWL 2. In contrast, the first semantic condition on datatype complements is an "if-then" condition, since it only has the status of a datarange expression. See the notes on the form of semantic conditions for further information on this topic. For the remaining semantic conditions that treat the cases of intersections and unions of datatypes it is sufficient to have "if-then" conditions, since an additional right-to-left directions would already be covered by the respective semantic conditions for general classes.

Table 5.4: Semantic Conditions for Boolean Connectives
if then
z , d 〉 ∈ IEXT(I(owl:datatypeComplementOf)) z , d ∈ IDC ,
ICEXT(z) = LV \ ICEXT(d)
z , c 〉 ∈ IEXT(I(owl:complementOf)) iff z , c ∈ IC ,
ICEXT(z) = IR \ ICEXT(c)
if then
s sequence of d1 , … , dn ∈ IDC , n ≥ 1 ,
z , s 〉 ∈ IEXT(I(owl:intersectionOf))
z ∈ IDC
if s sequence of c1 , … , cn ∈ IR then
z , s 〉 ∈ IEXT(I(owl:intersectionOf)) iff z , c1 , … , cn ∈ IC ,
ICEXT(z) = ICEXT(c1) ∩ … ∩ ICEXT(cn)
if then
s sequence of d1 , … , dn ∈ IDC , n ≥ 1 ,
z , s 〉 ∈ IEXT(I(owl:unionOf))
z ∈ IDC
if s sequence of c1 , … , cn ∈ IR then
z , s 〉 ∈ IEXT(I(owl:unionOf)) iff z , c1 , … , cn ∈ IC ,
ICEXT(z) = ICEXT(c1) ∪ … ∪ ICEXT(cn)

5.5 Semantic Conditions for Enumerations

Table 5.5 lists the semantic conditions for enumerations, i.e. classes that consist of an explicitly given finite set of instances. In particular, an enumeration entirely consisting of data values is a datatype.

Informative note: The second semantic condition is an "iff" condition, since the treated language feature has the status of both a class expression and an axiom in OWL 2. See the notes on the form of semantic conditions for further information on this topic. For the remaining semantic condition that treats the case of enumerations of data values it is sufficient to have "if-then" conditions, since an additional right-to-left direction would already be covered by the respective semantic condition for general individuals.

Table 5.5: Semantic Conditions for Enumerations
if then
s sequence of v1 , … , vn ∈ LV , n ≥ 1 ,
z , s 〉 ∈ IEXT(I(owl:oneOf))
z ∈ IDC
if s sequence of a1 , … , an ∈ IR then
z , s 〉 ∈ IEXT(I(owl:oneOf)) iff z ∈ IC ,
ICEXT(z) = { a1 , … , an }

5.6 Semantic Conditions for Property Restrictions

Table 5.6 lists the semantic conditions for property restrictions. Value restrictions require that all or at least one of the values of a certain property must be from some given class. Cardinality restrictions determine how often a certain property is allowed to be used with every given individual. Qualified cardinality restrictions are more specific than cardinality restrictions in that they determine the quantity of property applications with respect to a particular class from which the property objects are taken. By putting a self restriction on a property one regards only those individuals for which this property also points to the individual itself as its object. There are also semantic conditions for value restrictions dealing with n-ary datatypes.

As a convention, for a set S, an expression of the form "#S" means the number of elements in S.

Note that the semantic condition for self restrictions does not constrain the right hand side of a owl:hasSelf assertion to be the boolean value "true"^^xsd:boolean. See Section 5.3 for an explanation.

Informative note: All the semantic conditions are "if-then" conditions, since the treated language features have the status of class expressions in OWL 2. Also, the "if-then" conditions generally only list those consequences on their right hand side that are specific for the respective condition, i.e. consequences that do not already follow by other means. See the notes on the form of semantic conditions for further information on these topics.

Table 5.6: Semantic Conditions for Property Restrictions
if then
z , v 〉 ∈ IEXT(I(owl:hasSelf)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | 〈 x , x 〉 ∈ IEXT(p) }
z , c 〉 ∈ IEXT(I(owl:allValuesFrom)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | ∀ y : 〈 x , y 〉 ∈ IEXT(p) implies y ∈ ICEXT(c) }
s sequence of p1 , … , pn ∈ IR ,
z , d 〉 ∈ IEXT(I(owl:allValuesFrom)) ,
z , s 〉 ∈ IEXT(I(owl:onProperties))
p1 , … , pn ∈ IODP ,
d ∈ IDC ,
ICEXT(z) = { x | ∀ y1 , … , yn ∈ LV : 〈 x , yk 〉 ∈ IEXT(pk) for each 1 ≤ kn implies 〈 y1 , … , yn 〉 ∈ ICEXT(d) }
z , c 〉 ∈ IEXT(I(owl:someValuesFrom)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | ∃ y : 〈 x , y 〉 ∈ IEXT(p) and y ∈ ICEXT(c) }
s sequence of p1 , … , pn ∈ IR ,
z , d 〉 ∈ IEXT(I(owl:someValuesFrom)) ,
z , s 〉 ∈ IEXT(I(owl:onProperties))
p1 , … , pn ∈ IODP ,
d ∈ IDC ,
ICEXT(z) = { x | ∃ y1 , … , yn ∈ LV : 〈 x , yk 〉 ∈ IEXT(pk) for each 1 ≤ kn and 〈 y1 , … , yn 〉 ∈ ICEXT(d) }
z , a 〉 ∈ IEXT(I(owl:hasValue)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | 〈 x , a 〉 ∈ IEXT(p) }
z , n 〉 ∈ IEXT(I(owl:cardinality)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | #{ y | 〈 x , y 〉 ∈ IEXT(p) } = n }
z , n 〉 ∈ IEXT(I(owl:minCardinality)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | #{ y | 〈 x , y 〉 ∈ IEXT(p) } ≥ n }
z , n 〉 ∈ IEXT(I(owl:maxCardinality)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | #{ y | 〈 x , y 〉 ∈ IEXT(p) } ≤ n }
z , n 〉 ∈ IEXT(I(owl:qualifiedCardinality)) ,
z , c 〉 ∈ IEXT(I(owl:onClass)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | #{ y | 〈 x , y 〉 ∈ IEXT(p) and y ∈ ICEXT(c) } = n }
z , n 〉 ∈ IEXT(I(owl:qualifiedCardinality)) ,
z , d 〉 ∈ IEXT(I(owl:onDataRange)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
p ∈ IODP ,
ICEXT(z) = { x | #{ y ∈ LV | 〈 x , y 〉 ∈ IEXT(p) and y ∈ ICEXT(d) } = n }
z , n 〉 ∈ IEXT(I(owl:minQualifiedCardinality)) ,
z , c 〉 ∈ IEXT(I(owl:onClass)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | #{ y | 〈 x , y 〉 ∈ IEXT(p) and y ∈ ICEXT(c) } ≥ n }
z , n 〉 ∈ IEXT(I(owl:minQualifiedCardinality)) ,
z , d 〉 ∈ IEXT(I(owl:onDataRange)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
p ∈ IODP ,
ICEXT(z) = { x | #{ y ∈ LV | 〈 x , y 〉 ∈ IEXT(p) and y ∈ ICEXT(d) } ≥ n }
z , n 〉 ∈ IEXT(I(owl:maxQualifiedCardinality)) ,
z , c 〉 ∈ IEXT(I(owl:onClass)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
ICEXT(z) = { x | #{ y | 〈 x , y 〉 ∈ IEXT(p) and y ∈ ICEXT(c) } ≤ n }
z , n 〉 ∈ IEXT(I(owl:maxQualifiedCardinality)) ,
z , d 〉 ∈ IEXT(I(owl:onDataRange)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
p ∈ IODP ,
ICEXT(z) = { x | #{ y ∈ LV | 〈 x , y 〉 ∈ IEXT(p) and y ∈ ICEXT(d) } ≤ n }

5.7 Semantic Conditions for Datatype Restrictions

Table 5.7 lists the semantic conditions for datatype restrictions, which are used to define sub datatypes of existing datatypes by restricting the original datatype via a set of facet-value pairs. For example, one can define the datatype consisting of all strings of length 5 by a datatype restriction on the datatype xsd:string (Section 3.3) with the facet name xsd:length (Section 3.4) and the literal "5"^^xsd:integer.

Note that if no facet-value pair is applied to a given datatype at all, then the resulting datatype will be equivalent to the original datatype. Note further that, if a facet-value pair is applied to a datatype without being a member of the datatype's facet space, then the ontology cannot be satisfied and will therefore be inconsistent. In particular, a datatype restriction with one or more specified facet-value pairs will result in an inconsistent ontology, if applied to a datatype having an empty facet space (usually, a non-empty facet space only exists for those datatypes belonging to the datatype map).

The set IFS is defined by IFS(d) := { 〈 I(F) , v 〉 | 〈 F , v 〉 ∈ FS(d) } , where d is a datatype, F is the IRI reference of a facet, and v is a value of the facet. This set corresponds to the facet space, FS, of d, as defined in Section 4.1, but rather consists of pairs of the denotation of a facet and its value.

The mapping IF2V is defined by IF2V(d)(〈 I(F) , v 〉) := F2V(d)(〈 F , v 〉) , where d is a datatype, F is the IRI reference of a facet, and v is a value of the facet. This mapping corresponds to the facet-to-value mapping, F2V, of d, as defined in Section 4.1, resulting in the same subsets of the value space VS(d), but rather applies to pairs of the denotation of a facet and its value.

Informative note: The semantic condition is an "if-then" condition, since the treated language feature has the status of a datarange expression in OWL 2. Also, the "if-then" condition only lists those consequences on its right hand side that are specific for the condition, i.e. consequences that do not already follow by other means. See the notes on the form of semantic conditions for further information on these topics.

Table 5.7: Semantic Conditions for Datatype Restrictions
if then
s sequence of z1 , … , zn ∈ IR ,
f1 , … , fn ∈ IP ,
z , d 〉 ∈ IEXT(I(owl:onDatatype)) ,
z , s 〉 ∈ IEXT(I(owl:withRestrictions)) ,
z1 , v1 〉 ∈ IEXT(f1) , … , 〈 zn , vn 〉 ∈ IEXT(fn)
z , d ∈ IDC ,
f1 , … , fn ∈ IODP ,
v1 , … , vn ∈ LV ,
f1 , v1 〉 , … , 〈 fn , vn 〉 ∈ IFS(d) ,
ICEXT(z) = ICEXT(d) ∩ IF2V(d)(〈 f1 , v1 〉) ∩ … ∩ IF2V(d)(〈 fn , vn 〉)

5.8 Semantic Conditions for the RDFS Vocabulary

Table 5.8 extends the semantic conditions for parts of the RDFS vocabulary, including subclass axioms, subproperty axioms, domain axioms and range axioms, as originally defined in Section 4.1 of [RDF Semantics]. Only the additional semantic conditions are given here and the other conditions on the RDF and RDFS vocabularies are retained.

Informative note: All the semantic conditions are "iff" conditions, since the treated language features have the status of axioms in OWL 2. See the notes on the form of semantic conditions for further information on this topic. Note that the original semantics for the RDFS axioms only provide for weaker "if-then" semantic conditions.

Table 5.8: Semantic Conditions for the RDFS Vocabulary
c1 , c2 〉 ∈ IEXT(I(rdfs:subClassOf)) iff c1 , c2 ∈ IC ,
ICEXT(c1) ⊆ ICEXT(c2)
p1 , p2 〉 ∈ IEXT(I(rdfs:subPropertyOf)) p1 , p2 ∈ IP ,
IEXT(p1) ⊆ IEXT(p2)
p , c 〉 ∈ IEXT(I(rdfs:domain)) p ∈ IP , c ∈ IC ,
x , y : 〈 x , y 〉 ∈ IEXT(p) implies x ∈ ICEXT(c)
p , c 〉 ∈ IEXT(I(rdfs:range)) p ∈ IP , c ∈ IC ,
x , y : 〈 x , y 〉 ∈ IEXT(p) implies y ∈ ICEXT(c)

5.9 Semantic Conditions for Sub Property Chains

Table 5.9 lists the semantic conditions for sub property chains, which allow for specifying complex property subsumption axioms.

As an example, one can define a sub property chain axiom, for which the chain consisting of the extensions of the properties ex:hasFather and ex:hasBrother is covered by the extension of the property ex:hasUncle.

Informative note: The semantic conditions essentially represent an "iff" condition, since the treated language feature has the status of an axiom in OWL 2. However, there are actually two such semantic conditions, due to the multi-triple RDF encoding of this language feature. Also, the actual "if-then" conditions only list those consequences on their right hand side that are specific for the respective condition, i.e. consequences that do not already follow by other means. See the notes on the form of semantic conditions for further information on these topics. The semantics have been specified in a way to allow a sub property chain axiom to be satisfiable without requiring the existence of a property that represents the property chain.

Table 5.9: Semantic Conditions for Sub Property Chains
if s sequence of p1 , … , pn ∈ IR then
p , s 〉 ∈ IEXT(I(owl:propertyChainAxiom)) iff p ∈ IP ,
p1 , … , pn ∈ IP ,
y0 , … , yn : 〈 y0 , y1 〉 ∈ IEXT(p1) and … and 〈 yn-1 , yn 〉 ∈ IEXT(pn) implies 〈 y0 , yn 〉 ∈ IEXT(p)

5.10 Semantic Conditions for Equivalence and Disjointness Axioms

Table 5.10 lists the semantic conditions for specifying that two individuals are equal or different from each other, and that two classes or properties are equivalent or disjoint with each other. Also treated here are disjoint union axioms that allow for stating that a given class is equivalent to the union of a given collection of mutually disjoint classes.

Informative note: All the semantic conditions are "iff" conditions, since the treated language features have the status of axioms in OWL 2. See the notes on the form of semantic conditions for further information on this topic.

Table 5.10: Semantic Conditions for Equivalence and Disjointness Axioms
a1 , a2 〉 ∈ IEXT(I(owl:sameAs)) iff a1 = a2
a1 , a2 〉 ∈ IEXT(I(owl:differentFrom)) a1a2
c1 , c2 〉 ∈ IEXT(I(owl:equivalentClass)) c1 , c2 ∈ IC ,
ICEXT(c1) = ICEXT(c2)
c1 , c2 〉 ∈ IEXT(I(owl:disjointWith)) c1 , c2 ∈ IC ,
ICEXT(c1) ∩ ICEXT(c2) = ∅
p1 , p2 〉 ∈ IEXT(I(owl:equivalentProperty)) p1 , p2 ∈ IP ,
IEXT(p1) = IEXT(p2)
p1 , p2 〉 ∈ IEXT(I(owl:propertyDisjointWith)) p1 , p2 ∈ IP ,
IEXT(p1) ∩ IEXT(p2) = ∅
if s sequence of c1 , … , cn ∈ IR then
c , s 〉 ∈ IEXT(I(owl:disjointUnionOf)) iff c , c1 , … , cn ∈ IC ,
ICEXT(c) = ICEXT(c1) ∪ … ∪ ICEXT(cn) ,
ICEXT(cj) ∩ ICEXT(ck) = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk

5.11 Semantic Conditions for N-ary Axioms

Table 5.11 lists the semantic conditions for specifying n-ary axioms, i.e. that several individuals are mutually different from each other, and that either several classes or several properties are mutually disjoint with each other.

Note that there are two alternative ways to specify owl:AllDifferent axioms, by using either the property owl:members that is used for all other constructs, too, or by applying the legacy property owl:distinctMembers. Both constructs have the same model-theoretic meaning.

Informative note: The semantic conditions essentially represent "iff" conditions, since the treated language features have the status of axioms in OWL 2. However, there are actually two such semantic conditions for each language feature, due to the multi-triple RDF encoding of these language features. Also, the actual "if-then" conditions only list those consequences on their right hand side that are specific for the respective condition, i.e. consequences that do not already follow by other means. See the notes on the form of semantic conditions for further information on these topics.

Table 5.11: Semantic Conditions for N-ary Axioms
if then
s sequence of a1 , … , an ∈ IR ,
z ∈ ICEXT(I(owl:AllDifferent)) ,
z , s 〉 ∈ IEXT(I(owl:distinctMembers))
ajak for each 1 ≤ jn and each 1 ≤ kn such that jk
if then exists z ∈ IR
s sequence of a1 , … , an ∈ IR ,
ajak for each 1 ≤ jn and each 1 ≤ kn such that jk
z ∈ ICEXT(I(owl:AllDifferent)) ,
z , s 〉 ∈ IEXT(I(owl:distinctMembers))
if then
s sequence of a1 , … , an ∈ IR ,
z ∈ ICEXT(I(owl:AllDifferent)) ,
z , s 〉 ∈ IEXT(I(owl:members))
ajak for each 1 ≤ jn and each 1 ≤ kn such that jk
if then exists z ∈ IR
s sequence of a1 , … , an ∈ IR ,
ajak for each 1 ≤ jn and each 1 ≤ kn such that jk
z ∈ ICEXT(I(owl:AllDifferent)) ,
z , s 〉 ∈ IEXT(I(owl:members))
if then
s sequence of c1 , … , cn ∈ IR ,
z ∈ ICEXT(I(owl:AllDisjointClasses)) ,
z , s 〉 ∈ IEXT(I(owl:members))
c1 , … , cn ∈ IC ,
ICEXT(cj) ∩ ICEXT(ck) = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
if then exists z ∈ IR
s sequence of c1 , … , cn ∈ IC ,
ICEXT(cj) ∩ ICEXT(ck) = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
z ∈ ICEXT(I(owl:AllDisjointClasses)) ,
z , s 〉 ∈ IEXT(I(owl:members))
if then
s sequence of p1 , … , pn ∈ IR ,
z ∈ ICEXT(I(owl:AllDisjointProperties)) ,
z , s 〉 ∈ IEXT(I(owl:members))
p1 , … , pn ∈ IP ,
IEXT(pj) ∩ IEXT(pk) = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
if then exists z ∈ IR
s sequence of p1 , … , pn ∈ IP ,
IEXT(pj) ∩ IEXT(pk) = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
z ∈ ICEXT(I(owl:AllDisjointProperties)) ,
z , s 〉 ∈ IEXT(I(owl:members))

5.12 Semantic Conditions for Inverse Property Axioms

Table 5.12 lists the semantic conditions for inverse property axioms. One receives the inverse of a given property by swapping the subject and object in every property assertion.

Informative note: The semantic condition is an "iff" condition, since the treated language feature has the status of an axiom in OWL 2. See the notes on the form of semantic conditions for further information on this topic.

Table 5.12: Semantic Conditions for Inverse Property Axioms
p1 , p2 〉 ∈ IEXT(I(owl:inverseOf)) iff p1 , p2 ∈ IP ,
IEXT(p1) = { 〈 x , y 〉 | 〈 y , x 〉 ∈ IEXT(p2) }

5.13 Semantic Conditions for Property Characteristics

Table 5.13 lists the semantic conditions for property characteristics. A functional property can only be assigned at most once to a given individual. An inverse functional property can be regarded as a "key" property. A reflexive property relates every individual in the universe to itself, where an irreflexive property does not relate any individual with itself at all. If two individuals are related by a symmetric property, then this property also relates them by the reverse relationship, while this is never the case for an asymmetric property. A transitive property that relates an individual a with an individual b and the latter with an individual c also relates a with c.

Informative note: All the semantic conditions are "iff" conditions, since the treated language features have the status of axioms in OWL 2. See the notes on the form of semantic conditions for further information on this topic.

Table 5.13: Semantic Conditions for Property Characteristics
p ∈ ICEXT(I(owl:FunctionalProperty)) iff p ∈ IP ,
x , y1 , y2 : 〈 x , y1 〉 ∈ IEXT(p) and 〈 x , y2 〉 ∈ IEXT(p) implies y1 = y2
p ∈ ICEXT(I(owl:InverseFunctionalProperty)) p ∈ IP ,
x1 , x2 , y : 〈 x1 , y 〉 ∈ IEXT(p) and 〈 x2 , y 〉 ∈ IEXT(p) implies x1 = x2
p ∈ ICEXT(I(owl:ReflexiveProperty)) p ∈ IP ,
x : 〈 x , x 〉 ∈ IEXT(p)
p ∈ ICEXT(I(owl:IrreflexiveProperty)) p ∈ IP ,
x : 〈 x , x 〉 ∉ IEXT(p)
p ∈ ICEXT(I(owl:SymmetricProperty)) p ∈ IP ,
x , y : 〈 x , y 〉 ∈ IEXT(p) implies 〈 y , x 〉 ∈ IEXT(p)
p ∈ ICEXT(I(owl:AsymmetricProperty)) p ∈ IP ,
x , y : 〈 x , y 〉 ∈ IEXT(p) implies 〈 y , x 〉 ∉ IEXT(p)
p ∈ ICEXT(I(owl:TransitiveProperty)) p ∈ IP ,
x , y , z : 〈 x , y 〉 ∈ IEXT(p) and 〈 y , z 〉 ∈ IEXT(p) implies 〈 x , z 〉 ∈ IEXT(p)

5.14 Semantic Conditions for Keys

Table 5.14 lists the semantic conditions for Keys. Keys provide an alternative to inverse functional properties (see Section 5.13). They allow for defining a property as a key local to a given class: the specified property will have the features of a key only for individuals within the class, and no assumption is made about individuals external to the class, or for which it is unknown whether they are instances of the class. Further, it is possible to define "compound keys", i.e. several properties can be combined into a single key applicable to composite values.

Informative note: The semantic condition is an "iff" condition, since the treated language feature has the status of an axiom in OWL 2. See the notes on the form of semantic conditions for further information on this topic.

Table 5.14: Semantic Conditions for Keys
if s sequence of p1 , … , pn ∈ IR then
c , s 〉 ∈ IEXT(I(owl:hasKey)) iff c ∈ IC ,
p1 , … , pn ∈ IP ,
x , y , z1 , … , zn :
   if x ∈ ICEXT(c) and y ∈ ICEXT(c) and
      for each 1 ≤ kn
         〈 x , zk 〉 ∈ IEXT(pk) and 〈 y , zk 〉 ∈ IEXT(pk)
   then x = y

5.15 Semantic Conditions for Negative Property Assertions

Table 5.15 lists the semantic conditions for negative property assertions. They allow to state that an individual a1 does not stand in a relationship p with another individual a2. The second form based on owl:targetValue is more specific than the first form based on owl:targetIndividual in that it is restricted to the case of negative data property assertions. Note that the second form will coerce the target individual of a negative property assertion into a data value, due to the range defined for the property owl:targetValue in Section 5.3.

Informative note: The semantic conditions essentially represent "iff" conditions, since the treated language features have the status of axioms in OWL 2. However, there are actually two such semantic conditions for each language feature, due to the multi-triple RDF encoding of these language features. Also, the actual "if-then" conditions only list those consequences on their right hand side that are specific for the respective condition, i.e. consequences that do not already follow by other means. See the notes on the form of semantic conditions for further information on these topics.

Table 5.15: Semantic Conditions for Negative Property Assertions
if then
z , a1 〉 ∈ IEXT(I(owl:sourceIndividual)) ,
z , p 〉 ∈ IEXT(I(owl:assertionProperty)) ,
z , a2 〉 ∈ IEXT(I(owl:targetIndividual))
a1 , a2 〉 ∉ IEXT(p)
if then exists z ∈ IR
a1 ∈ IR ,
p ∈ IP ,
a2 ∈ IR ,
a1 , a2 〉 ∉ IEXT(p)
z , a1 〉 ∈ IEXT(I(owl:sourceIndividual)) ,
z , p 〉 ∈ IEXT(I(owl:assertionProperty)) ,
z , a2 〉 ∈ IEXT(I(owl:targetIndividual))
if then
z , a 〉 ∈ IEXT(I(owl:sourceIndividual)) ,
z , p 〉 ∈ IEXT(I(owl:assertionProperty)) ,
z , v 〉 ∈ IEXT(I(owl:targetValue))
p ∈ IODP ,
a , v 〉 ∉ IEXT(p)
if then exists z ∈ IR
a ∈ IR ,
p ∈ IODP ,
v ∈ LV ,
a , v 〉 ∉ IEXT(p)
z , a 〉 ∈ IEXT(I(owl:sourceIndividual)) ,
z , p 〉 ∈ IEXT(I(owl:assertionProperty)) ,
z , v 〉 ∈ IEXT(I(owl:targetValue))

6 Axiomatic Triples (Informative)

The RDF Semantics document [RDF Semantics] defines so called "axiomatic triples" for the RDF and RDFS vocabularies. Examples of axiomatic triples are:

rdf:type rdf:type rdf:Property ,
rdf:type rdfs:domain rdfs:Resource ,
rdf:type rdfs:range rdfs:Class .

Axiomatic triples are used to give certain basic semantic meaning to all the IRI references in the RDF and RDFS vocabularies. This semantic meaning is meant to be "axiomatic", in the sense that it holds for every ontology of the regarded language, including the empty ontology.

Typically, as shown by the example triples above, axiomatic triples are used in the RDF Semantics to specify the part of the universe that the denotation of a vocabulary IRI reference belongs to. In the case of properties of the regarded vocabulary, the domains and the ranges are also specified. These kinds of axiomatic triples can be equivalently restated in the form of semantic conditions that have neither premises nor bound variables. Using the names of the different parts of the universe, defined in Section 4.4, the example axiomatic triples above can be restated as:

I(rdf:type) ∈ IP ,
IEXT(I(rdf:type)) ⊆ IR × IC .

Unlike the RDF Semantics, OWL 2 Full does not provide an explicit set of axiomatic triples. It might not be possible to give a definition of OWL 2 Full that captures all intended "axiomatic aspects" of the language in the form of sets of RDF triples, just as it is not possible to define the whole semantics of OWL 2 Full in the form of a set of RDF entailment rules. However, Section 5 contains sets of semantic conditions that are "axiomatic" in the sense described above. Most of these semantic conditions actually have a form similar to those semantic conditions, which resulted from equivalently restating the example axiomatic triples above.

6.1 Class Axiomatic Triples

The semantic conditions for "Classes", given in Section 5.2, can be regarded as a set of OWL 2 Full axiomatic triples for classes: for each IRI reference E occurring in the first column of the table there, if the second column contains an entry "I(E) ∈ S" for some set S, then this entry corresponds to some RDF triple of the form "E rdf:type C", where C is the IRI reference of some class with ICEXT(I(C)) = S. In the table, S will always be either the set IC of all classes, or some subset of IC. Hence, in a corresponding RDF triple the IRI reference C will typically be one of "rdfs:Class" or "owl:Class" (S=IC in both cases), or "rdfs:Datatype" (S=IDC).

For example, the semantic condition for the IRI reference "owl:FunctionalProperty", given by

I(owl:FunctionalProperty) ∈ IC ,

has the corresponding RDF triple

owl:FunctionalProperty rdf:type rdfs:Class .

Further, for each IRI reference E in the first column, if the third column contains an entry "ICEXT(I(E)) ⊆ S" (or "ICEXT(I(E)) = S") for some set S, then this entry corresponds to some RDF triple of the form "E rdfs:subClassOf C" (or "E owl:equivalentClass C"), where C is the IRI reference of some class with ICEXT(I(C)) = S.

For example, the semantic condition

ICEXT(I(owl:FunctionalProperty)) ⊆ IP

has the corresponding RDF triple

owl:FunctionalProperty rdfs:subClassOf rdf:Property .

Additionally, the semantic conditions on the sets, given in Section 5.1, have to be taken into account. In particular, if an entry of the first column in the table there states "S1S2" for some sets S1 and S2, then this corresponds to some RDF triple C1 owl:subClassOf C2, where C1 and C2 are the IRI references of some classes with ICEXT(I(C1)) = S1 and ICEXT(I(C2)) = S2, respectively, according to Section 5.2.

Note that some of the RDF triples generated this way already follow from the RDFS semantics [RDF Semantics].

6.2 Property Axiomatic Triples

The semantic conditions for "Properties", given in Section 5.3, can be regarded as a set of OWL 2 Full axiomatic triples for properties: for each IRI reference E occurring in the first column of the table there, if the second column contains an entry "I(E) ∈ S" for some set S, then this entry corresponds to some RDF triple of the form "E rdf:type C", where C is the IRI reference of some class with ICEXT(I(C)) = S. In the table, S will always be either the set IP of all properties, or some subset of IP. Hence, in a corresponding RDF triple the IRI reference C will typically be one of "rdf:Property" or "owl:ObjectProperty" (S=IP in both cases), or "owl:DatatypeProperty" (S=IODP), or "owl:AnnotationProperty" (S=IOAP), or "owl:OntologyProperty" (S=IOXP).

For example, the semantic condition for the IRI reference "owl:disjointWith", given by

I(owl:disjointWith) ∈ IP ,

has the corresponding RDF triple

owl:disjointWith rdf:type rdf:Property .

Further, for each IRI reference E in the first column, if the third column contains an entry "IEXT(I(E)) ⊆ S1 × S2" for some sets S1 and S2, then this entry corresponds to some RDF triples of the forms "E rdfs:domain C1" and "E rdfs:range C2", where C1 and C2 are the IRI references of some classes with ICEXT(I(C1)) = S1 and ICEXT(I(C2)) = S2, respectively.

For example, the semantic condition

IEXT(I(owl:disjointWith)) ⊆ IC × IC

has the corresponding RDF triples

owl:disjointWith rdfs:domain rdfs:Class ,
owl:disjointWith rdfs:range rdfs:Class .

Exceptions are the semantic conditions "IEXT(I(owl:topObjectProperty)) = IR × IR" and "IEXT(I(owl:topDataProperty)) = IR × LV" , for which there are no corresponding domain and range triples.

6.3 Simple Axiomatic Triples

These axiomatic triples are "simple" in the following sense: for every set S mentioned in the second and the third column of the table in Section 5.2 on semantic conditions for "Classes", there exists an IRI reference C of some class in the vocabularies for RDF and RDFS, or those given in Section 3, for which S = ICEXT(I(C)).

For every set S mentioned in the second column of the table in Section 5.3 on semantic conditions for "Properties", and as the left or right hand side of a Cartesian product in the third column of the table, there exists an IRI reference C of some class in the vocabularies for RDF and RDFS or those given in Section 3, for which S = ICEXT(I(C)).

7 Relationship to OWL 2 DL (Informative)

Editor's Note: Update this section intro to new forms of Balancing definition and lemma, and new form of correspondence theorem.

This section compares OWL 2 Full with the OWL 2 Direct Semantics, which is based on the description logic SROIQ according to [OWL 2 Direct Semantics]. In contrast, OWL 2 Full is an RDF based language, in that OWL 2 Full interpretations are defined as special D-interpretations [RDF Semantics], as detailed in Section 4.2. Several fundamental differences that exist between the two semantics are discussed in this section. However, a strong relationship will be presented, showing that OWL 2 Full is able to reflect all logical conclusions of the OWL 2 Direct Semantics. This means that the OWL 2 Direct Semantics can in a sense be regarded as a sub language of OWL 2 Full. The notion of a logical conclusion will be that of an entailment, so that the actual relationship can, roughly speaking, be expressed in the form that every OWL 2 Direct entailment is also an OWL 2 Full entailment (with certain technically caused restrictions being discussed later in this section).

The two ontologies that build such an entailment will be required to meet several syntactic constraints. First, they both have to be valid OWL 2 DL ontologies in RDF graph form. These are RDF graphs that can be mapped by the reverse OWL 2 RDF mapping [OWL 2 RDF Mapping] to a corresponding OWL 2 DL ontology in Functional Syntax form [OWL 2 Functional Specification], which additionally meets all the global syntactical constraints that are specified in [OWL 2 Functional Specification]. In fact, these global constraints must hold mutually for both ontologies in the regarded entailment.

Furthermore, due to certain fundamental differences that exist between OWL 2 Full and the OWL 2 Direct Semantics (as exposed in Section 7.1), it cannot be ensured technically that every syntactic variations of two ontologies that build an OWL 2 Direct entailment will also build an OWL 2 Full entailment.

To come accross this problem, Section 7.2 introduces a general and effective method for "balancing" the differences between the two semantics, by means of a purely syntactic operation that works on every valid OWL 2 Direct entailment query. This balancing process, when applied to a pair of OWL 2 DL ontologies in RDF graph form G1 and G2, will result in a new pair of RDF graphs G1* and G2*, that again are OWL 2 DL ontologies in RDF graph form. The semantic meaning of G1* will equals that of G1 under the OWL 2 Direct Semantics, and likewise for G2* compared to G2. Hence, G1* will OWL 2 Direct entail G2* if and only if G1 OWL 2 Direct entails G2.

Nevertheless, the new RDF graphs G1* and G2*, which result from the ontology balancing process, will generally differ syntactically from the original RDF graphs G1 and G2. This syntactic difference is responsible for a change of the semantic meaning under the OWL 2 Full semantics, which is just sufficient to ensure that G1* OWL 2 Full entails G2* whenever G1 OWL 2 Direct entails G2. This is the gist of the the OWL 2 Correspondence Theorem, which will be presented in Section 7.3.

However, the correspondence theorem does not make any assertions about entailment queries that do not consist of valid OWL 2 DL ontologies in RDF graph form. For certain pairs of RDF graphs it might still be reasonable to expect that they build an OWL 2 Full entailment, even if these graphs do not formally adhere to the syntax of OWL 2 DL. It turns out that there are cases, where the normative semantics of OWL 2 Full does not provide such an expected entailment. Section 7.4 will list the so called "OWL 2 Full comprehension conditions", which is a collection of additional model-theoretic semantic conditions that may be used as a foundation for creating methods to treat the general case of arbitrary RDF graphs in entailment queries.

Editor's Note: TODO: small glossar of most relevant terms, such as "OWL 2 Direct entailment"

7.1 Differences to the OWL 2 Direct Semantics

Editor's Note: Update this section to new forms of Balancing definition and lemma, and new form of correspondence theorem.
Editor's Note: Add text regarding root nodes of multi-triple axiom encodings and "named" boolean connectives, to illustrate what cannot be done with balancing.
Editor's Note: It has been proposed to summarize somewhere in the text how the methods (balancing, stripping) work.

Two fundamental differences exist between OWL 2 Full and the OWL 2 Direct Semantics, which complicate a comparison of the expressivity of these two semantics. This section discusses these differences by means of an example and points to some of the problems that may arise from the differences. Further, it is shown for the same example how these problems can be overcome by an approach to "balance" the differences.

The first difference is that the OWL 2 Direct Semantics does not interpret every language construct of OWL 2. Examples of uninterpreted constructs are entity declarations and annotations. Hence, under the OWL 2 Direct Semantics, the RDF encodings of these constructs do not have a semantic meaning, while, in contrast, OWL 2 Full gives a semantic meaning to every RDF graph. If the right hand side of an OWL 2 DL entailment consists of uninterpreted constructs, it is not always guaranteed that the same entailment also holds under the OWL 2 Full semantics.

For example, consider the following two RDF graphs G1 and G2:

G1 := {

(1) ex:c1 rdf:type owl:Class .
(2) ex:c2 rdf:type owl:Class .
(3) ex:c1 rdfs:subClassOf ex:c2 .

}

G2 := {

(1) ex:c1 rdf:type owl:Class .
(2) ex:c2 rdf:type owl:Class .
(3) ex:c3 rdf:type owl:Class .
(4) ex:c3 rdfs:comment "an annotation" .
(5) _:x rdf:type owl:Class .
(6) _:x owl:unionOf (SEQ ex:c2 ex:c3) .
(7) ex:c1 rdfs:subClassOf _:x .

}

Both G1 and G2 are OWL 2 DL ontologies in RDF graph form, and it is easy to verify that G1 OWL 2 Direct entails G2. For this to hold, the typing triples (1) and (2) in G1 and (1), (2) and (3) in G2 can be ignored, since they are mapped by the reverse OWL 2 RDF Mapping to entity declarations, which are not interpreted by the OWL 2 Direct Semantics. Likewise, the annotation in triple (4) of G2 does not have a semantic meaning under the OWL 2 Direct Semantics.

However, all the typing triples and the annotation in G2 are actually interpreted by OWL 2 Full. Since the typing triple (3) and the annotation triple (4) of G2 do not also occur in G1, there are OWL 2 Full interpretations that satisfy G1 but not the triples (3) and (4). Hence, G1 does not OWL 2 Full entail G2.

This problem can be overcome by copying the triples (3) and (4) to G1, leading to the new graph G1a

G1a := {

(1) ex:c1 rdf:type owl:Class .
(2) ex:c2 rdf:type owl:Class .
(3) ex:c3 rdf:type owl:Class .
(4) ex:c3 rdfs:comment "an annotation" .
(5) ex:c1 rdfs:subClassOf ex:c2 .

}

The graph G1a is, again, a syntactically valid OWL 2 DL ontology in RDF graph form. The performed copying operation does not have a semantic effect under the OWL 2 Direct semantics, since only uninterpreted constructs have been added to G1, i.e., G1a and G1 are semantically equivalent. From this follows that G1a OWL 2 Direct entails G2 if and only if G1 OWL 2 Direct entails G2. However, the situation has changed for OWL 2 Full, since the triples (3) and (4) of G2 are now satisfied by every OWL 2 Full interpretation that satisfies G1a.

The second difference between OWL 2 Full and the OWL 2 Direct Semantics is that the OWL 2 Direct Semantics treats classes as sets, i.e. subsets of the universe. However, a class in OWL 2 Full is an individual in the universe, and it is distinguished from the subset of the universe it represents, i.e. its respective class extension. An analog distinction holds for properties. An effect of this difference is that certain logical conclusions of the OWL 2 Direct Semantics do not become "visible" in OWL 2 Full, although they are reflected by OWL 2 Full at a set theoretical level.

As stated earlier, G1a OWL 2 Direct entails G2. However, in OWL 2 Full this entailment does not hold. This is mainly due to triple (6) in G2, which contains a blank node (see Section 6.6 of [RDF Concepts]) as the left hand side of a owl:unionOf triple. Under the OWL 2 Full semantics, this triple, roughly speaking, claims that an individual exists in the universe that has the union of two specific sets as its class extension. From a set theoretical perspective, it is, of course, always ensured that for two given subsets of the universe there is another subset of the universe that is the union of the original sets. However, in general no guarantee is given for the existence of an individual in the universe having the result set as its class extension. And in this particular example, there is also no premise that would justify such a conclusion.

Nevertheless, OWL 2 Full interprets G2 in a way such that the set theoretical relationship

ICEXT(I(ex:c1)) ⊆ ICEXT(I(ex:c2)) ∪ ICEXT(I(ex:c3))

holds. This is basically the same semantic relationship that results from interpreting G2 under the OWL 2 Direct Semantics, which does not distinguish between classes and their class extensions. Hence, with respect to the "relevant logical conclusions" OWL 2 Full essentially reflects the results of the OWL 2 Direct Semantics in this example.

However, in order to also satisfy G2 under the OWL 2 Full semantics, it is necessary to go beyond this semantic relationship by additionally ensuring the existence of a "helper" individual a with the set S, defined by

S := ICEXT(a) = ICEXT(I(ex:c2)) ∪ ICEXT(I(ex:c3))

as its class extension. This can actually be achieved by adding the following RDF graph

{

_:x rdf:type owl:Class .
_:x owl:unionOf (SEQ ex:c2 ex:c3) .
_:x owl:equivalentClass _:x .

}

to G1a, resulting in the new graph G1b

G1b := {

(1) ex:c1 rdf:type owl:Class .
(2) ex:c2 rdf:type owl:Class .
(3) ex:c3 rdf:type owl:Class .
(4) ex:c3 rdfs:comment "an annotation" .
(5) ex:c1 rdfs:subClassOf ex:c2 .
(6) _:x rdf:type owl:Class .
(7) _:x owl:unionOf (SEQ ex:c2 ex:c3) .
(8) _:x owl:equivalentClass _:x .

}

The basic idea here is to assert the existence of an individual that represents the class expression in question, i.e. makeing the triples (5) and (6) of G2 available on the left hand side of the entailment in a way, such that the resulting graph is still a syntactically valid OWL 2 DL ontology in RDF graph form, and without changing the semantic meaning of the original ontology G1a. However, simply copying the two triples would generally not lead to the desired result, since this would produce a class expression that has no connection to any axiom in the ontology. An OWL 2 DL ontology is basically a set of axioms, and, in particular, it does not allow for the occurrence of "dangling" class expression. For this reason, the additional triple "_:x owl:equivalentClass _:x" has been added to G1b (triple (8)), which, in combination with the triples (5) and (6), encodes a valid OWL 2 DL axiom. This axiom is actually a tautology w.r.t. the OWL 2 Direct Semantics, i.e. adding it does not change the semantic meaning of the original ontology.

Hence, the graph G1b is, again, a syntactically valid OWL 2 DL ontology in RDF graph form. And, again, the performed operation does not have any semantic effect under the OWL 2 Direct semantics, i.e., G1b and G1a are semantically equivalent. From this follows that G1b OWL 2 Direct entails G2 if and only if G1a OWL 2 Direct entails G2. However, the situation has changed for OWL 2 Full, since all the triples of G2 are now satisfied by every OWL 2 Full interpretation that satisfies G1b. As the added tautological axiom has been build from the encoding of the union class expression consisting of the triples (6) and (5) in G2, and since this subgraph consists of the original blank node, the existence of the missing individual in G2 is finally ensured (and in addition, the existence of the list in triple (6) of G2 is ensured by this, either).

To summarize, for the particular example given in this section it was possible to "balance" the fundamental differences that hold between OWL 2 Full and the OWL 2 Direct Semantics, by performing a purely syntactic transformation on an OWL 2 Direct entailment consisting of two OWL 2 DL ontologies in RDF graph form, G1 and G2, to receive a semantically equivalent OWL 2 Direct entailment consisting again of two OWL 2 DL ontologies in RDF graph form, G1b and G2, for which it is ensured that G1b OWL 2 Full entails G2, either. Section 7.2 will generalize this idea of "balancing" to arbitrary OWL 2 Direct entailment queries.

7.2 Balancing

Editor's Note: Adjust the intro text to the new form of balancing definition and lemma.

Motivated by the discussion in Section 7.1, this section describes the general approach to balance an OWL 2 Direct entailment query that consists of two OWL 2 DL ontologies in RDF graph form. Balancing will be the foundation for the OWL 2 Correspondence Theorem presented in Section 7.3.

Definition 7.1 tells what it means for an OWL 2 Direct entailment query to be balanced. In essence, the original pair of OWL 2 DL ontologies in RDF graph form will be transformed into a new pair of RDF graphs in a way that, according to Theorem 7.1, the semantic meaning of the original entailment query is preserved w.r.t. the OWL 2 Direct semantics.

TODO: EXPLAIN FURTHER

From Theorem 7.1 follows that it is effectively possible to balance arbitrary OWL 2 Direct entailment queries. The proof for this theorem will give useful advice on how to construct an algorithm for such a transformation, which is based entirely on syntactic processing of the pair of input ontologies.

Definition 7.1 (OWL 2 Balancing): A pair of RDF graphs 〈 G1 , G2 〉 is called OWL 2 balanced, iff G1 and G2 are OWL 2 DL ontologies in RDF graph form, with F(G1) and F(G2) being the corresponding OWL 2 DL ontologies in Functional Syntax form [OWL 2 Specification] that result from applying the reverse OWL 2 RDF mapping [OWL 2 RDF Mapping] to G1 and G2, respectively, such that all the following additional conditions hold:

  • F(G1) and F(G2) mutually meet the global syntactic restrictions on OWL 2 DL ontologies as specified in [OWL 2 Specification].
  • G2 does not contain:
    • RDF encodings of annotations (Sections 3.2.2 and 3.2.3, and Table 17 in [OWL 2 RDF Mapping]), nor
    • triples with an ontology property as their predicates (Section 5.3 in the document at hand), nor
    • deprecation triples (Table 16 in [OWL 2 RDF Mapping]).
  • Each subgraph g of G2 is also a subgraph of G1, provided that g is the RDF encoding of:
Editor's Note: Something needs to be said about the "corresponding OWL 2 DL datatype map" of an OWL 2 Full datatype map, because this is referred to in the Balancing Lemma.

Theorem 7.1 (OWL 2 Balancing Lemma): An algorithm exists with the following input/output behaviour:

Let the input of the algorithm be a pair of RDF graphs 〈 G1* , G2* 〉, where G1* and G2* are OWL 2 DL ontologies in RDF graph form, with F(G1*) and F(G2*) being the corresponding OWL 2 DL ontologies in Functional Syntax form [OWL 2 Specification] that result from applying the reverse OWL 2 RDF mapping [OWL 2 RDF Mapping] to G1* and G2*, respectively, such that F(G1*) and F(G2*) mutually meet the global syntactic restrictions on OWL 2 DL ontologies as specified in [OWL 2 Specification].

Then the output of the algorithm will be a pair of RDF graphs 〈 G1 , G2 〉, where G1 and G2 are OWL 2 DL ontologies in RDF graph form, with F(G1) and F(G2) being the corresponding OWL 2 DL ontologies in Functional Syntax form that result from applying the reverse OWL 2 RDF mapping to G1 and G2, respectively, such that for any OWL 2 Full datatype map D according to Definition 4.1, with F(D) being the corresponding OWL 2 DL datatype map according to Section 2.1 of [OWL 2 Direct Semantics], all the following conditions hold:

  • The pair 〈 G1 , G2 〉 is OWL 2 balanced according to Definition 7.1.
  • F(G1) OWL 2 Direct entails F(G1*) with respect to F(D), and F(G1*) OWL 2 Direct entails F(G1) with respect to F(D).
  • F(G2) OWL 2 Direct entails F(G2*) with respect to F(D), and F(G2*) OWL 2 Direct entails F(G2) with respect to F(D).

Proof: See Appendix 9.1.

7.3 Correspondence Theorem

Editor's Note: Update the section intro to the new form of the correspondence theorem, possibly taking the new form of the balancing definition and theorem into account.

This section presents the OWL 2 Correspondence Theorem, which compares the semantic expressivity of OWL 2 Full with that of the OWL 2 Direct Semantics. The theorem basically states that every entailment with respect to the OWL 2 Direct Semantics is also an OWL 2 Full entailment. Precisely:

Theorem 7.2 (OWL 2 Correspondence Theorem):

Let D be an OWL 2 Full datatype map according to Definition 4.1, with F(D) being the corresponding OWL 2 DL datatype map according to Section 2.1 of [OWL 2 Direct Semantics]. Let G1* and G2* be RDF graphs that are OWL 2 DL ontologies in RDF graph form, with F(G1*) and F(G2*) being the corresponding OWL 2 DL ontologies in Functional Syntax form [OWL 2 Specification] that result from applying the reverse OWL 2 RDF mapping [OWL 2 RDF Mapping] to G1* and G2*, respectively, such that F(G1*) and F(G2*) mutually meet the global syntactic restrictions on OWL 2 DL ontologies as specified in [OWL 2 Specification].

Then, there exist RDF graphs G1 and G2 that are OWL 2 DL ontologies in RDF graph form, with F(G1) and F(G2) being the corresponding OWL 2 DL ontologies in Functional Syntax form that result from applying the reverse OWL 2 RDF mapping to G1 and G2, respectively, such that all the following conditions hold:

  • F(G1) and F(G2) mutually meet the global syntactic restrictions on OWL 2 DL ontologies.
  • F(G1) OWL 2 Direct entails F(G2) with respect to F(D), if and only if F(G1*) OWL 2 Direct entails F(G2*) with respect to F(D).
  • If F(G1) OWL 2 Direct entails F(G2) with respect to F(D), then G1 OWL 2 Full entails G2 with respect to D.

Proof Sketch: See Appendix 9.2.

Some technical notes:

Editor's Note: Update the notes to the new form of the correspondence theorem, possibly taking the new form of the balancing definition and theorem into account.

Based on the results in Section 7.2 it is possible to restrict the comparison to entailments that are composed of balanced OWL 2 DL ontologies in RDF graph form. According to Theorem 7.1 it is always possible to transform an OWL 2 Direct entailment query consisting of arbitrary OWL 2 DL ontologies in RDF graph form into a semantically equivalent OWL 2 Direct entailment query that consists of balanced component ontologies. In particular, the theorem only considers entailments consisting of ontolgies that mutually meet the global syntactic restrictions on OWL 2 DL ontologies, as specified in [OWL 2 Specification]. Actually, only entailments of this sort are treated by the OWL 2 Direct Semantics (see the final paragraph in Section 2.5 of OWL 2 Direct Semantics).

The theorem does not consider entailments with annotations, deprecation statements, statements with ontology properties, or ontology headers on the right hand side. In fact, the theorem would become wrong if this would be allowed. The OWL 2 Direct Semantics does not assign any semantic meaning to these kinds of language constructs. Hence, having some of them in an OWL 2 DL ontology in RDF graph form does not change the semantic meaning of the ontology with respect to the OWL 2 Direct Semantics. OWL 2 Full, however, actually provides semantic meaning to every subset of triples in an RDF graph, including the RDF encodings of the language constructs discussed here. Therefore, adding some of them to an RDF graph changes the semantic meaning of the graph in OWL 2 Full, and thus may render a formerly valid entailment invalid. See Section 7.1 for an example and further discussion.

The theorem is restricted to single RDF graphs on the left and right hand side of an entailment query. For the purpose of comparing the semantic expressivity it can, without loss of generality, always be assumed that collections of more than one RDF graphs on either the left or right hand side of an entailment query have been replaced by the corresponding merge of the respective collection of RDF graphs (see Section 0.3 of [RDF Semantics]). This has no actual effect on the semantic relationship considered here.

The theorem distinguishes between a OWL 2 Full datatype map, as defined by definition 4.1, and the "corresponding" OWL 2 Direct datatype map, as defined in Section 2.1 of [OWL 2 Direct Semantics]. The distinction is necessary due to the different formats of the datatype maps. However, a translation between the two notions is straightforward.

Editor's Note: Find a better place for the following transformation of datatype maps. This is already needed for the Balancing Lemma.

Let D be an OWL 2 Full datatype map according to definition 4.1. The corresponding OWL 2 Direct datatype map F(D) := ( NDT , NLS , NFS , ⋅ DT , ⋅ LS , ⋅ FS ) is given as follows.

  • The set of datatypes NDT is the set of each IRI reference ddd and datatype d, where 〈 ddd , d 〉 ∈ D, except for the IRI reference rdfs:Literal.
  • The lexical space NLS(ddd) := LS(d), for each IRI reference dddNDT and datatype d, where 〈 ddd , d 〉 ∈ D.
  • The facet space NFS(ddd) := FS(d), for each IRI reference dddNDT and datatype d, where 〈 ddd , d 〉 ∈ D.
  • The value space (ddd) DT := VS(d), for each IRI reference dddNDT and datatype d, where 〈 ddd , d 〉 ∈ D.
  • The data value (〈 a , ddd 〉) LS := L2V(d)(a), for each IRI reference dddNDT and datatype d, where 〈 ddd , d 〉 ∈ D, and for each lexical form aNLS(ddd).
  • The interpretation of the facet-value pair (〈 F , v 〉) FS := F2V(d)(〈 F , v 〉), for each IRI reference dddNDT and datatype d, where 〈 ddd , d 〉 ∈ D, and for each facet-value pair 〈 F , v 〉 ∈ NFS(ddd).

7.4 Comprehension Conditions

Editor's Note: Provide an example in the intro that shows what the problem is.

The method given in Section 7.2 to balance a graph G1 with respect to another graph G2 has been defined only for cases, in which G1 and G2 are OWL 2 DL ontologies in RDF graph form. However, the problem of making certain semantic conclusions visible in the form of an entailment, as discussed in Section 7.1, is not restricted to valid OWL 2 DL ontologies. For the general case of arbitrary OWL 2 Full ontologies G1 and G2, this section provides a collection of model-theoretic semantic conditions, called "comprehension conditions", which provide for the existence of list expressions, class expressions and datatype restrictions, created from arbitrary collections of appropriate individuals in the universe.

The comprehension conditions are not part of the set of semantic conditions given in Section 5, and therefore do not need to be met by an OWL 2 Full interpretation as defined in Section 4. Implementers have to notice that the comprehension conditions add significantly to the complexity and semantic expressivity of the language. In fact, the OWL working group has found that OWL 2 Full extended by the comprehension conditions leads to a semantically inconsistent language. Implementers MAY thus decide to only use a fraction of the comprehension conditions, or to use them as a starting basis for creating heuristical approaches to balance entailments in a way motivated by the method described in Section 7.2.

Note: This section reuses the conventions stated in the introduction of Section 5 ("Semantic Conditions").

7.4.1 Comprehension Conditions for Sequences

Table 7.1 lists the comprehension conditions for sequences, i.e. RDF lists. These comprehension conditions provide the existence of sequences built from any possible combination of individuals contained in the OWL 2 Full universe.

Table 7.1: Comprehension Conditions for Sequences
if then exists z1 , … , zn ∈ IR
a1 , … , an ∈ IR z1 , a1 〉 ∈ IEXT(I(rdf:first)) , 〈 z1 , z2 〉 ∈ IEXT(I(rdf:rest)) , … ,
zn , an 〉 ∈ IEXT(I(rdf:first)) , 〈 zn , I(rdf:nil) 〉 ∈ IEXT(I(rdf:rest))

7.4.2 Comprehension Conditions for Boolean Class Connectives

Table 7.2 lists the comprehension conditions for boolean connectives (see Section 5.4 for the corresponding semantic conditions). These comprehension conditions provide the existence of complement classes for any class, and of unions and intersections built from any possible set of classes contained in the OWL 2 Full universe.

Table 7.2: Comprehension Conditions for Boolean Connectives
if then exists z ∈ IR
c ∈ IC z , c 〉 ∈ IEXT(I(owl:complementOf))
d ∈ IDC z , d 〉 ∈ IEXT(I(owl:datatypeComplementOf))
s sequence of c1 , … , cn ∈ IC z , s 〉 ∈ IEXT(I(owl:intersectionOf))
s sequence of c1 , … , cn ∈ IC z , s 〉 ∈ IEXT(I(owl:unionOf))

7.4.3 Comprehension Conditions for Enumerations

Table 7.3 lists the comprehension conditions for enumerations (see Section 5.5 for the corresponding semantic conditions). These comprehension conditions provide the existence of enumeration classes built from any possible set of individuals contained in the OWL 2 Full universe.

Table 7.3: Comprehension Conditions for Enumerations
if then exists z ∈ IR
s sequence of a1 , … , an ∈ IR z , s 〉 ∈ IEXT(I(owl:oneOf))

7.4.4 Comprehension Conditions for Property Restrictions

Table 7.4 lists the comprehension conditions for property restrictions (see Section 5.6 for the corresponding semantic conditions). These comprehension conditions provide the existence of cardinality restriction classes on any property and for any non-negative integer, as well as value restriction classes on any property and on any class contained in the OWL 2 Full universe.

Note that the comprehension conditions for self restrictions constrains the right hand side of the produced owl:hasSelf assertions to be the boolean value "true"^^xsd:boolean. This is in accordance with Table 13 in Section 3.2.4 of [OWL 2 RDF Mapping].

Table 7.4: Comprehension Conditions for Property Restrictions
if then exists z ∈ IR
p ∈ IP z , I("true"^^xsd:boolean) 〉 ∈ IEXT(I(owl:hasSelf)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
c ∈ IC ,
p ∈ IP
z , c 〉 ∈ IEXT(I(owl:allValuesFrom)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
d ∈ IDC ,
s sequence of p1 , … , pn ∈ IODP
z , d 〉 ∈ IEXT(I(owl:allValuesFrom)) ,
z , s 〉 ∈ IEXT(I(owl:onProperties))
c ∈ IC ,
p ∈ IP
z , c 〉 ∈ IEXT(I(owl:someValuesFrom)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
d ∈ IDC ,
s sequence of p1 , … , pn ∈ IODP
z , d 〉 ∈ IEXT(I(owl:someValuesFrom)) ,
z , s 〉 ∈ IEXT(I(owl:onProperties))
a ∈ IR ,
p ∈ IP
z , a 〉 ∈ IEXT(I(owl:hasValue)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
n ∈ INNI ,
p ∈ IP
z , n 〉 ∈ IEXT(I(owl:cardinality)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
n ∈ INNI ,
p ∈ IP
z , n 〉 ∈ IEXT(I(owl:minCardinality)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
n ∈ INNI ,
p ∈ IP
z , n 〉 ∈ IEXT(I(owl:maxCardinality)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
n ∈ INNI ,
c ∈ IC ,
p ∈ IP
z , n 〉 ∈ IEXT(I(owl:qualifiedCardinality)) ,
z , c 〉 ∈ IEXT(I(owl:onClass)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
n ∈ INNI ,
d ∈ IDC ,
p ∈ IODP
z , n 〉 ∈ IEXT(I(owl:qualifiedCardinality)) ,
z , d 〉 ∈ IEXT(I(owl:onDataRange)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
n ∈ INNI ,
c ∈ IC ,
p ∈ IP
z , n 〉 ∈ IEXT(I(owl:minQualifiedCardinality)) ,
z , c 〉 ∈ IEXT(I(owl:onClass)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
n ∈ INNI ,
d ∈ IDC ,
p ∈ IODP
z , n 〉 ∈ IEXT(I(owl:minQualifiedCardinality)) ,
z , d 〉 ∈ IEXT(I(owl:onDataRange)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
n ∈ INNI ,
c ∈ IC ,
p ∈ IP
z , n 〉 ∈ IEXT(I(owl:maxQualifiedCardinality)) ,
z , c 〉 ∈ IEXT(I(owl:onClass)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))
n ∈ INNI ,
d ∈ IDC ,
p ∈ IODP
z , n 〉 ∈ IEXT(I(owl:maxQualifiedCardinality)) ,
z , d 〉 ∈ IEXT(I(owl:onDataRange)) ,
z , p 〉 ∈ IEXT(I(owl:onProperty))

7.4.5 Comprehension Conditions for Datatype Restrictions

Table 7.5 lists the comprehension conditions for datatype restrictions (see Section 5.7 for the corresponding semantic conditions). These comprehension conditions provide the existence of datatypes built from restricting any datatype contained in the OWL 2 Full universe by any possible set of facet-value pairs contained in the facet space (see Section 4.1) of the original datatype.

The set IFS is defined in Section 5.7.

Table 7.5: Comprehension Conditions for Datatype Restrictions
if then exists z ∈ IR , s sequence of z1 , … , zn ∈ IR
d ∈ IDC ,
f1 , … , fn ∈ IODP ,
v1 , … , vn ∈ LV ,
f1 , v1 〉 , … , 〈 fn , vn 〉 ∈ IFS(d)
z , d 〉 ∈ IEXT(I(owl:onDatatype)) ,
z , s 〉 ∈ IEXT(I(owl:withRestrictions)) ,
z1 , v1 〉 ∈ IEXT(f1) , … , 〈 zn , vn 〉 ∈ IEXT(fn)

7.4.6 Comprehension Conditions for Inverse Property Expressions

Table 7.6 lists the comprehension conditions for inverse property expressions. These comprehension conditions provide the existence of an inverse property for any property contained in the OWL 2 Full universe.

Inverse property expressions can be used to build axioms with anonymous inverse properties, such as

_:x owl:inverseOf ex:p
_:x rdfs:subPropertyOf owl:topObjectProperty

Note that, to some extend, OWL 2 Full already covers the use of inverse property expressions by means of the semantic conditions of inverse property axioms (see Section 5.12), since these semantic conditions also apply to existential variables on the left hand side of inverse property axioms. However, not all relevant cases are covered by this semantic condition. For example, one might expect the above graph A to be generally true. But the OWL 2 Full semantics does not permit this conclusion, since it is not ensured that for every property p there is an individual in the universe that happens to be the inverse property of p.

Table 7.6: Comprehension Conditions for Inverse Property Expressions
if then exists z ∈ IR
p ∈ IP z , p 〉 ∈ IEXT(I(owl:inverseOf))

8 Changes from OWL Full (Informative)

Editor's Note: List should be categorized (Bugs, compatible and incompatible changes, etc.
Editor's Note: New features should also be mentioned (language features, datatypes with facets, etc.

This section lists significant differences between OWL 2 Full and the original version of OWL Full [OWL Full].

  • Resource Identifiers: All references to the term "URI" have been replaced by the term "IRI" [RFC 3987], following the rest of the OWL 2 documents. This is a backwards-compatible deviation from the RDF Semantics and OWL Full, which used the term URI according to [RFC 2396].
  • Role of the comprehension conditions: The "comprehension conditions" are not part of the normative set of semantic conditions anymore, though they are still listed in the document. Using them as such would lead to inconsistency of OWL 2 Full.
  • Form of the correspondence theorem: No comprehension conditions are used anymore to generally provide the existence of individuals representing class expressions. Instead, a notion of "balanced entailments" has been introduced, where OWL 2 DL entailments are effectively transformed into semantically equivalent entailments, which are also OWL 2 Full entailments. Annotations, deprecation statements and statements containing ontology properties are not allowed to occur in the conclusions of entailments.
  • "Axiomatic" Semantic Conditions: OWL Full did not specify the domain and the range for some properties, for example not for owl:inverseOf. OWL 2 Full now specifies the domain and range for every property in the OWL 2 Full vocabulary by means of certain semantic conditions. In addition, an informative section has been added to provide a notion of "axiomatic triples" for OWL 2 Full.
  • Imports closure definition: There is no such definition anymore in OWL 2 Full, since, unlike OWL 1 Full, it is not used in the document anywhere.
  • New Section on syntax: The new section called "Ontologies" determines the syntax of OWL 2 Full.
  • Changed semantic conditions for data value enumerations: The semantic condition for enumerations of data values (IRI reference owl:oneOf) has been restricted to non-empty lists of data values. This prevents owl:Nothing from unintendendly becoming a datatype, see [email].
  • Changed semantic conditions for data ranges: A more specific semantics has been given to the IRI reference owl:DataRange by making it an equivalent class to rdfs:Datatype. An analysis of the situation in OWL Full was given in [email].
  • Added missing semantic conditions for n-ary axioms: There was an error in OWL Full in that missed semantic conditions for specifying the complete semantics of axioms based on the IRI reference owl:AllDifferent. The missing semantic conditions have been added in OWL 2 Full.
  • Changed semantic conditions for "sequence-based" language constructs: The semantic conditions for unions, intersections and enumerations had an error in their definitions, leading to inconsistency of OWL Full [Issue 120]. The semantic conditions have been fixed in OWL 2 Full by changing the form of the semantic conditions.
  • Terminological changes:
    • The names "RI", "PI", "CI", "EXTI", "CEXTI", "SI", "LI" and "LVI" have been changed to match the corresponding entities defined in the RDF Semantics [RDF Semantics], namely "IR", "IP", "IC", "IEXT", "ICEXT", "IS", "IL" and "LV", respectively. This better enables the use of the RDF-Based Semantics document as an incremental extension of the RDF Semantics document. Not changed were names that only occurred in the OWL Full document, such as "IX" or "IODP".
    • All uses of the IRI reference mapping "IS" have been replaced by the more general interpretation mapping "I", following the RDF Semantics document [RDF Semantics].
    • Several names for class extensions have been removed, such as "IAD" for the extension of owl:AllDifferent. The remaining names are those of the basic "parts" of the OWL 2 Full universe, and there are useful shortnames for sequences and non-negative numbers.
    • What has been called "boolean combinations" in OWL 1 Full is now called "boolean connectives" in order to better match the terminology used in the rest of the OWL 2 specification.
  • Deprecated IRI references: The following vocabulary IRI references have been deprecated as of OWL 2 by the working group, and SHOULD NOT be used in new ontologies anymore:
    • owl:DataRange

9 Appendix: Proofs for the Theorems (Informative)

This appendix provides proofs for the different theorems in this document.

9.1 Proof for the OWL 2 Balancing Lemma

Editor's Note: Adjust the proof to the new definition of balancing and the new form of the balancing lemma.

This is a proof for Theorem 7.1 (OWL 2 Balancing Lemma), stated in Section 7.2.

Without loss of generality, one can assume that G1 and G2 have no common blank nodes. Otherwise, a preprocessing step will substitute all blank nodes in G1 for fresh blank nodes that do not occur in G2.

Since G2 is an OWL 2 DL ontologies in RDF graph form, the canonical parsing process for computing the reverse OWL 2 RDF mapping, as defined in [OWL 2 RDF Mapping], can be applied to G2 to uniquely identify all the subgraphs that correspond to the different forms of entitiy declarations and expressions mentioned in Definition 7.1.

The resulting RDF graph is constructed as follows: The initial version of the result graph G1*, is a copy of G1. Now, the following steps are performed on every subgraph gG2 that has been identified by the adapted canonical parsing process:

  • If g corresponds to an entity declaration, then g is copied unchanged to G1*.
  • If g corresponds to a property expression with root blank node x, then g together with the RDF triple "x owl:equivalentProperty x" is added to G1*.
  • If g corresponds to a class expression with root blank node x, then g together with the RDF triple "x owl:equivalentClass x" is added to G1*.
  • If g corresponds to a data range expression with root blank node x, then:
    • If g is part of some data property restriction expression, then nothing needs to be done, since this case is covered by the treatment of class expressions;
    • Otherwise, g is part of at least one data property range axiom. One such property p is chosen randomly, and the RDF encoding r of a universal property restriction expression on property p is created for the datarange expression rooted by node x. Let the RDF graph r have fresh root blank node y. r together with the RDF triple "y owl:equivalentClass y" is added to G1*.

Property 1) of the theorem results from the fact that G1 is an OWL 2 DL ontology in RDF graph form, and G1* differs from G1 only by additional subgraphs that can be mapped by the reverse OWL 2 RDF mapping to either an entity declaration or a valid OWL 2 DL axiom in Functional Syntax. Since the global syntactic restrictions on OWL 2 DL ontologies are mutually met by both original ontologies, and since only declarations and expressions that already exist in G2 are added to G1, G1* cannot hurt the global syntactic restrictions. Property 2) again follows from the premise that the global syntactic restrictions on OWL 2 DL ontologies are mutually met by both original ontologies. Property 3) holds due to the fact that G1* differs from G1 only by having additional entity declarations that are not interpreted by the OWL 2 Direct Semantics, and by having additional axioms that are tautologies w.r.t. the OWL 2 Direct Semantics. Property 4) is true by construction, and since all the premises of Definition 7.1 are met for G1* and G2. Finally, an algorithm exists for the construction of G1*, since the canonical parsing process for computing the reverse RDF mapping is actually an algorithm, and for all the other steps described above it is obvious that they can be performed algorithmically. Q.E.D.

9.2 Proof Sketch for the OWL 2 Correspondence Theorem

This is a proof sketch for Theorem 7.2 (OWL 2 Correspondence Theorem), stated in Section 7.3.

Editor's Note: Adjust the proof to the new form of the correspondence theorem, and the new balancing definition and lemma.
Editor's Note: Ongoing Refinement: The editor intends to further refine the proof sketch for the correspondence theorem until the document becomes a Proposed Recommendation. Both the correspondence theorem and its proof are non-normative parts of the OWL 2 Full specification. Hence, changes to the proof will not affect the design of OWL 2 Full, and will therefore not require a new Last Call working draft. Since the proof is quite complex, trying to complete it before the publication of a Last Call working draft would seriously delay this publication without justification.

Assume that the premises of the theorem hold. Let I be an OWL 2 Full interpretation w.r.t. the OWL 2 Full datatype map D of a vocabulary VI that covers all the names (IRI references and literals) occurring in the RDF graphs G1 and G2, and let I OWL 2 Full satisfy G1. It will be shown that I OWL 2 Full satisfies G2.

As a first step, an OWL 2 Direct interpretation J w.r.t. the OWL 2 Direct datatype map F(D) will be constructed for a vocabulary VJ that covers all the names (IRI references and literals) occurring in the OWL 2 DL ontologies in Functional Syntax form F(G1) and F(G2). J will be defined in a way such that it closely corresponds to I on those parts of the vocabularies VI and VJ that cover G1 and G2, and F(G1) and F(G2), respectively.

G1 and G2 are OWL 2 DL ontologies in RDF graph form that are mapped by the reverse RDF mapping to F(G1) and F(G2), respectively. From this follows that the same literals are used in both G1 and F(G1), and in both G2 and F(G2), respectively, and that there are entity declarations in F(G1) and F(G2) for every non-builtin IRI reference occurring in G1 and G2, respectively. For each entity declaration of the form Declaration(T(u)) in F(G1) and F(G2), where T is the entity type for some IRI reference u, a typing triple of the form u rdf:type t exists in G1 or G2, respectively, where t denotes the class representing the part of the OWL 2 Full universe that corresponds to T; and vice versa.

Since G1 is OWL 2 balanced w.r.t. G2, all the entity declarations of F(G2) are also contained in F(G1), and therefore all the typing triples of G2 that correspond to some entity declaration in F(G2) are also contained in G1. Since I OWL 2 Full satisfies G1, all these "declaring" typing triples are OWL 2 Full satisfied by I, and thus all non-builtin IRI references in G1 and G2 are actually instances of their declared parts of the OWL 2 Full universe.

Based on these observations, the OWL 2 Direct interpretation J and its vocabulary VJ for the datatype map F(D) can now be defined.

The vocabulary VJ := ( VC , VOP , VDP , VI , VDT , VLT , VFA ) is defined as follows.

  • The set VC of class names contains all IRI references that are declared as classes in F(G1).
  • The set VOP of object property names contains all IRI references that are declared as object properties in F(G1).
  • The set VDP of data property names contains all IRI references that are declared as data properties in F(G1).
  • The set VI of individual names contains all IRI references that are declared as named individuals in F(G1).

The sets VDT of datatype names, VLT of literals, and VFA of facet-literal pairs are defined according to Section 2.1 of [OWL 2 Direct Semantics] w.r.t. the datatype map F(D).

The interpretation J := ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) is defined as follows. The object and data domains of J are identified with the universe IR and the set of data values LV of I, respectively, i.e., ΔInt := IR and ΔD := LV. The datatype interpretation function ⋅ DT, the literal interpretation function ⋅ LT, and the facet interpretation function ⋅ FA are defined according to Section 2.2 of [OWL 2 Direct Semantics]. For every non-builtin IRI reference u occurring in F(G1):

  • If u is declared as a named individual, then set uI := I(u), since G1 contains the triple "u rdf:type owl:NamedIndividual", i.e., I(u) ∈ IR.
  • If u is declared as a class, then set uC := ICEXT(I(u)), since the graphs contain the triple "u rdf:type owl:Class", i.e., I(u) ∈ IC.
  • If u is declared as an object property, then set uOP := IEXT(I(u)), since the graphs contain the triple "u rdf:type owl:ObjectProperty", i.e., I(u) ∈ IP.
  • If u is declared as a data property, then set uDP := IEXT(I(u)), since the graphs contain the triple "u rdf:type owl:DatatypeProperty", i.e., I(u) ∈ IODP.

Note that G1 may also contain declarations of annotation properties, but they will not be interpreted by the OWL 2 Direct Semantics and are therefore ignored here. This will not lead to problems, since G2 does not contain any annotations.

Further, note that the definition of J is compatible with the concept of a non-separated vocabulary in OWL 2 DL (also called "punning", see Section 5.9 of [OWL 2 Specification]). Since G1 and G2 are OWL 2 DL ontologies in RDF graph form, it is allowed that the same IRI reference u is declared to be all of an individual name, and a class name, and either an object property name or a data property name. According to I, the IRI reference u will always denote the same individual in the universe IR, where I(u) will be both a class and a property. Under J, however, the individual name u will denote an individual, the class name u will denote a subset of ΔInt, and the property name u will denote a subset of ΔInt × ΔInt.

Literals occurring in G1 and G2 are mapped by the OWL 2 RDF mapping to the same literals in the corresponding interpreted language constructs of F(G1) and F(G2), which comprise data enumerations, has-value restrictions with a data value, cardinality restrictions, datatype restrictions, data property assertions, and negative data property assertions. Also, the semantics of literals is strictly analog for both OWL 2 Full and the OWL 2 Direct Semantics. Therefore, literals need no further treatment in this proof.

Based on the premise that I OWL 2 Full satisfies G1, it has to be shown that J OWL 2 Direct satisfies F(G1). For this to hold it will be sufficient to show that J OWL 2 Direct satisfies every axiom occurring in F(G1). Let A be an axiom occurring in F(G1), and let gA be the subgraph of G1 that is mapped to A by the reverse OWL 2 RDF mapping. It is possible to prove that J OWL 2 Direct satisfies A by showing that the semantic meaning, which is given to A by the OWL 2 Direct Semantics, is compatible with the semantic relationship that, according to J, holds between the denotations of the names occurring in A. The basic idea is as follows:

Since I OWL 2 Full satisfies G1, all the triples occuring in gA are OWL 2 Full satisfied by I. Also, since I is an OWL 2 Full interpretation, all the OWL 2 Full semantic conditions are met by I. Hence, the left-to-right directions of all the semantic conditions that are "matched" by the triples in gA will apply. This will reveal certain semantic relationships that, according to I, hold between the denotations of the names occurring in gA. These semantic relationships are, roughly speaking, the semantic consequences of the axiom that is encoded by the triples in gA.

Since the denotations w.r.t. J of all the names occurring in A have been defined in terms of the denotations and class and property extensions w.r.t. I of the same names occuring in gA, and since the semantic meaning of the axiom A w.r.t. the OWL 2 Direct Semantics turns out to be fully covered by the semantic consequences of the subgraph gA w.r.t. OWL 2 Full, one can eventually show that J OWL 2 Direct satisfies A.

A special note is necessary for anonymous individuals occurring in an assertion A. These have the form of the same blank node b both in A and in gA. Both OWL 2 Full and the OWL 2 Direct Semantics treat blank nodes as existential variables in an ontology. Since I satisfies gA, b can be mapped to an individual x in IR such that gA becomes true under I (see Section 1.5 in [RDF Semantics] for the precise definition on how blank nodes are treated in RDF based languages). The same mapping from b to x can also be used for J in order to OWL 2 Direct satisfy A.

This basic idea is now demostrated in more detail for a single example axiom A in F(G1), which can be taken as a hint on how a complete proof could be constructed in principle. A complete proof would need to take every language feature of OWL 2 into account, as well as additional aspects such as datatype maps and facets. As in the example below, such a proof can make use of the observation that the definitions of the OWL 2 Direct Semantics and the OWL 2 Full semantics for all the different language features of OWL 2 are actually closely aligned.

Let A = SubClassOf(ex:c1 UnionOf(ex:c2 ex:c3)) for IRI references ex:c1, ex:c2 and ex:c3 that are declared to be classes elsewhere in F(G1).

Due to the reverse OWL 2 RDF Mapping, gA has the form

gA = {

ex:c1 rdfs:subClassOf _:x .
_:x rdf:type owl:Class .
_:x owl:unionOf (SEQ ex:c2 ex:c3) .

}

Since I is an OWL 2 Full interpretation, it meets all the OWL 2 Full semantic conditions. Since I OWL 2 Full satisfies G1, all the triples in gA are OWL 2 Full satisfied, and this triggers the left-to-right directions of the semantic conditions for subclass axioms (rdfs:subClassOf) and union class expressions (owl:unionOf). This reveals that the denotations of the names in gA are actually classes

I(ex:c1) ∈ IC ,
I(ex:c2) ∈ IC ,
I(ex:c3) ∈ IC ,

and that the following semantic relationship holds between the extensions of these classes:

ICEXT(I(ex:c1)) ⊆ ICEXT(I(ex:c2)) ∪ ICEXT(I(ex:c3)) .

From applying the definition of J follows that the following semantic relationship, w.r.t. J, holds between the denotations of the class names occurring in A:

(ex:c1C ⊆ (ex:c2C ∪ (ex:c3C .

This semantic relationship equals the semantic meaning of the axiom A = SubClassOf(ex:c1 UnionOf(ex:c2 ex:c3)) w.r.t. the OWL 2 Direct Semantics. Hence, J OWL 2 Direct satisfies A.

Since J OWL 2 Direct satisfies F(G1), and since F(G1) OWL 2 Direct entails F(G2), it follows that J OWL 2 Direct satisfies F(G2).

The next step will be to show that I OWL 2 Full satisfies G2. For this to hold, I needs to OWL 2 Full satisfy all the triples occurring in G2, taking into account the premise that an OWL 2 Full interpretation is required to meet all the OWL 2 Full semantic conditions. Since G2 is an OWL 2 DL ontology in RDF graph form that does not contain annotations, deprecation statements, statements with ontology properties and ontology headers, F(G2) only consists of entity declarations and axioms. Further, since G2 is an OWL 2 DL ontology in RDF graph form, every triple occuring in G2 belongs to some subgraph of G2 that is mapped by the reverse OWL 2 RDF mapping to one of the entity declarations or axioms contained in F(G2).

For entity declarations, let A be an entity declaration in F(G2), and let gA be the corresponding subgraph of G2. Since G1 is OWL 2 balanced w.r.t. G2, A occurs in F(G1), and hence gA is a subgraph of G1. Since I OWL 2 Full satisfies G1, I in particular OWL 2 Full satisfies gA.

For axioms, let A be an axiom in F(G2), and let gA be the corresponding subgraph of G2. It is possible to prove that I OWL 2 Full satisfies gA, by showing that all the premises for the right-to-left hand side of the particular semantic conditions, which are associated with the sort of axiom represented by gA, are met. This will allow to apply the semantic condition, from which will follow that all the triples in gA are OWL 2 Full satisfied by I. The premises of the semantic condition generally require that the denotations of all the non-builtin names in gA are contained in the appropriate part of the OWL 2 Full universe, and that the semantic relationship that is expressed on the right hand side of the semantic condition actually holds between the denotations of all these names w.r.t. I. Special care has to be taken regarding the blank nodes occurring in gA. The basic idea is as follows:

For every non-builtin IRI reference u occurring in gA, u also occurs in A, and, therefore, there are one or more entity declarations in F(G2), each being of the form E := "Declaration(T(u))" for some entity type T. From the reverse RDF mapping follows that for each such declaration E a typing triple e exists in G2, being of the form e := "u rdf:type t", where t is the name of a class representing the part of the OWL 2 Full universe corresponding to the entity type T. It has already been shown that for E being an entity declaration in F(G2), and e being the corresponding subgraph in G2, I OWL 2 Full satisfies e. Hence, I(u) is a resource contained in the appropriate part of the OWL 2 Full universe.

Further, since J OWL 2 Direct satisfies F(G2), J OWL 2 Direct satisfies A. Therefore, the semantic relationship that is represented by A according to the OWL 2 Direct Semantics actually holds between the denotations of the names occurring in A w.r.t. J. Since the denotations of these names w.r.t. J have been defined in terms of the denotations and class and property extensions w.r.t. I of the same names in G2, by applying the definition of J it will turn out that the analog relationship also holds between the denotations of the same names occurring in gA.

Finally, for the blank nodes occurring in gA, it becomes clear from the fact that G2 is an OWL DL ontology in RDF graph form that only certain kinds of subgraphs of gA can occur having blank nodes.

  • Case 1: A blank node corresponds to some anonymous individual in A (for A being one of a class assertion, object property assertion or data property assertion, according to Sections 5.6, 9.5 and 11.2 in [OWL 2 Specification]). The same blank node is used in A, and J interprets it as an existential variable. This renders the semantic relationship that is expressed by A into an existential assertion. After applying the definition of J, the analog existential assertion holds w.r.t. I, with the same blank node as the same existential variable in gA.
  • Case 2: A blank node is the "root" node of the multi-triple RDF encoding gA of A (for gA being an n-ary axiom from Section 5.11, or a negative property assertion from Section 5.15). The right-to-left direction of the semantic condition for this kind of axiom is of a form that the triples in gA containing the blank node will be OWL 2 Full satisfied after all the premises of the semantic condition are met.
  • Case 3: A blank node is the "root" node of the multi-triple RDF encoding gE of an expression in A (for gE being either a sequence, or one of a boolean connective from Section 5.4, an enumeration from Section 5.5, a property restriction from Section 5.6, or a datatype restriction from Section 5.7). Since G1 is OWL 2 balanced w.r.t. G2, gE also occurs in G1. Since I OWL 2 Full satisfies G1, gE is OWL 2 Full satisfied, either, taking into account that blank nodes are existential variables. Hence, the left-to-right direction of the respective semantic condition for the particular sort of expression can be applied. This can be done for all the expressions occurring in gA, and gA can be seen as a directed acyclic graph with the triples encoding the actual axiom on top, and the different component expressions being connected via blank nodes. Eventually, one can see that all the premises of the right-to-left direction of the semantic condition for the axiom encoded by gA hold.

This basic idea is now demostrated in more detail for a single example axiom A in F(G2), which can be taken as a hint on how a complete proof could be constructed in principle. A complete proof would need to take every language feature of OWL 2 into account, as well as additional aspects such as datatype maps and facets. As in the example below, such a proof can make use of the observation that the definitions of the OWL 2 Direct Semantics and the OWL 2 Full semantics for all the different language features of OWL 2 are actually closely aligned.

Let A = SubClassOf(ex:c1 UnionOf(ex:c2 ex:c3)) for IRI references ex:c1, ex:c2 and ex:c3 that are declared to be classes elsewhere in F(G2).

Due to the reverse OWL 2 RDF Mapping, gA has the form

gA = {

ex:c1 rdfs:subClassOf _:x .
_:x rdf:type owl:Class .
_:x owl:unionOf (SEQ ex:c2 ex:c3) .

}

The entity declarations for the class names ex:c1, ex:c2 and ex:c3 occurring in both A and gA correspond to typing triples

ex:c1 rdf:type owl:Class,
ex:c2 rdf:type owl:Class and
ex:c3 rdf:type owl:Class

in G2, respectively. Based on the premise that G1 is OWL 2 balanced w.r.t. G2, all these typing triples are OWL 2 Full satisfied by I. Hence, all the IRI references denote classes:

I(ex:c1) ∈ IC ,
I(ex:c2) ∈ IC and
I(ex:c3) ∈ IC

Since J OWL 2 Direct satisfies A, the following semantic relationship holds between the denotations of the class names in A w.r.t. J:

(ex:c1C ⊆ (ex:c2C ∪ (ex:c3C .

Applying the definition of J results in the following semantic relationship w.r.t. I that holds between the denotations of the names in gA:

ICEXT(I(ex:c1)) ⊆ ICEXT(I(ex:c2)) ∪ ICEXT(I(ex:c3))

The subgraph gE of gA, given by

gE := {

_:x rdf:type owl:Class .
_:x owl:unionOf (SEQ c2 c3) .

}

corresponds to a union class expression in A. Since G1 is OWL 2 balanced w.r.t. G2, gE is also a subgraph of G1 (it will be assumed that the same blank nodes are used in both instances of gE in order to simplify the argument). Since both G1 and G2 are OWL 2 DL ontologies in RDF graph form, the blank nodes occurring in gE do not occur outside of gE, neither in G1 nor in G2.

Since I OWL 2 Full satisfies G1, according to the semantic conditions for RDF graphs with blank nodes (see Section 1.5 of [RDF Semantics]), a mapping B from blank(gE) to IR exists, where blank(gE) is the set of all blank nodes in gE, such that the extended interpretation I+B OWL 2 Full satisfies all the triples in gE. An analog argument holds for all the blank nodes occurring in the sequence expression (SEQ c2 c3).

This allows to apply the left-to-right direction of the semantic condition for union class expressions (owl:unionOf), providing:

[I+B](_:x) ∈ IC ,
ICEXT([I+B](_:x)) = ICEXT(I(ex:c2)) ∪ ICEXT(I(ex:c3))

Together with the intermediate results from above, it follows:

I(ex:c1) ∈ IC ,
[I+B](_:x) ∈ IC ,
ICEXT(I(ex:c1)) ⊆ ICEXT([I+B](_:x))

Therefore, all the premises are met to apply the right-to-left direction of the semantic condition of subclass axioms (rdfs:subClassOf), which results in

I(ex:cl) , [I+B](_:x) 〉 ∈ IEXT(I(rdfs:subClassOf)) .

So, the triple

ex:c1 rdfs:subClassOf _:x

is OWL 2 Full satisfied by I+B, where "_:x" is the same blank node as the root blank node of the union class expression in gA.

Hence, w.r.t. existential blank node semantics, I OWL 2 Full satisfies all the triples in gA.

To conclude, for every OWL 2 Full interpretation I that OWL 2 Full satisfies G1 it turns out that I also OWL 2 Full satisfies G2. Hence, G1 OWL 2 Full entails G2. Q.E.D.

10 Acknowledgments

The starting point for the development of OWL 2 was the OWL1.1 member submission, itself a result of user and developer feedback, and in particular of information gathered during the OWL Experiences and Directions (OWLED) Workshop series. The working group also considered postponed issues from the WebOnt Working Group.

This document has been produced by the OWL Working Group (see below), and its contents reflect extensive discussions within the Working Group as a whole. The editors extend special thanks to Jie Bao (RPI), Peter F. Patel-Schneider (Bell Labs Research, Alcatel-Lucent) and Zhe Wu (Oracle Corporation) for their thorough reviews.

The regular attendees at meetings of the OWL Working Group at the time of publication of this document were: Jie Bao (RPI), Diego Calvanese (Free University of Bozen-Bolzano), Bernardo Cuenca Grau (Oxford University Computing Laboratory), Martin Dzbor (Open University), Achille Fokoue (IBM Corporation), Christine Golbreich (Université de Versailles St-Quentin and LIRMM), Sandro Hawke (W3C/MIT), Ivan Herman (W3C/ERCIM), Rinke Hoekstra (University of Amsterdam), Ian Horrocks (Oxford University Computing Laboratory), Elisa Kendall (Sandpiper Software), Markus Krötzsch (FZI), Carsten Lutz (Universität Bremen), Deborah L. McGuinness (RPI), Boris Motik (Oxford University Computing Laboratory), Jeff Pan (University of Aberdeen), Bijan Parsia (University of Manchester), Peter F. Patel-Schneider (Bell Labs Research, Alcatel-Lucent), Sebastian Rudolph (FZI), Alan Ruttenberg (Science Commons), Uli Sattler (University of Manchester), Michael Schneider (FZI), Mike Smith (Clark & Parsia), Evan Wallace (NIST), Zhe Wu (Oracle Corporation), and Antoine Zimmermann (DERI Galway). We would also like to thank past members of the working group: Jeremy Carroll, Jim Hendler, and Vipul Kashyap.

11 References

[CURIE]
CURIE Syntax 1.0: A syntax for expressing Compact URIs. M. Birbeck and S. McCarron, Editors, W3C Candidate Recommendation, 16 January 2009, http://www.w3.org/TR/2009/CR-curie-20090116.
[OWL 2 Direct Semantics]
OWL 2 Web Ontology Language: Direct Semantics. Boris Motik, Peter F. Patel-Schneider, and Bernardo Cuenca Grau, eds., 2009.
[OWL 2 RDF Mapping]
OWL 2 Web Ontology Language: Mapping to RDF Graphs. Peter F. Patel-Schneider and Boris Motik, eds., 2009.
[OWL 2 Specification]
OWL 2 Web Ontology Language: Structural Specification and Functional-Style Syntax. Boris Motik, Peter F. Patel-Schneider, and Bijan Parsia, eds., 2009.
[OWL 1 RDF-Compatible Semantics]
OWL Web Ontology Language: Semantics and Abstract Syntax, Section 5. RDF-Compatible Model-Theoretic Semantics. Peter F. Patel-Schneider, Patrick Hayes, and Ian Horrocks, eds., W3C Recommendation, 10 February 2004.
[RDF Concepts]
Resource Description Framework (RDF): Concepts and Abstract Syntax. Graham Klyne and Jeremy J. Carroll, eds. W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-concepts-20040210/. Latest version available as http://www.w3.org/TR/rdf-concepts/.
[RDF Semantics]
RDF Semantics. Patrick Hayes, ed., W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-rdf-mt-20040210/. Latest version available as http://www.w3.org/TR/rdf-mt/.
[RDF:PLAINLITERAL]
rdf:PlainLiteral: A Datatype for RDF Plain Literals. Jie Bao, Axel Polleres, and Boris Motik, eds., 2009.
[RFC 2119]
RFC 2119: Key words for use in RFCs to Indicate Requirement Levels. Network Working Group, S. Bradner. IETF, March 1997, http://www.ietf.org/rfc/rfc2119.txt
[RFC 2396]
RFC 2396 - Uniform Resource Identifiers (URI): Generic Syntax. T. Berners-Lee, R. Fielding, U.C. Irvine and L. Masinter. IETF, August 1998.
[RFC 3987]
RFC 3987: Internationalized Resource Identifiers (IRIs). M. Duerst and M. Suignard. IETF, January 2005, http://www.ietf.org/rfc/rfc3987.txt

12 Changelog

Editor's Note: MOVE THIS LIST TO "CHANGES WIKI PAGE" BEFORE PUBLICATION.

This section lists significant changes since the Second Public Working Draft.

  • The "Introduction" section has been revised.
  • All references to the term "URI" have been replaced by the term "IRI" [RFC 3987], following the rest of the OWL 2 documents. This is a backwards-compatible deviation from the RDF Semantics, which used the term URI according to [RFC 2396].
  • All occurrences of the term "IRI" have been replaced by the term "IRI reference", following the RDF Semantics spec.
  • Completed the "Changes from OWL Full" section.
  • The rendering of the formulae is now more similar to that in the Direct Semantics [OWL 2 Direct Semantics].
  • Correspondence Theorem now WLOG talks about single graphs on the LHS and RHS of entailments (no import closedness mentioned anymore).
  • The Correspondence Theorem, in addition to annotations, does not allow deprecation statements, ontology headers and statements containing ontology properties to occur in the conclusions of entailments. None of these kinds of statements have semantic meaning in OWL 2 DL.
  • Swapped "Ontologies" section (now 2) and "Vocabulary" section (now 3).
  • Made sup-section "Changes from OWL Full" into a toplevel section
  • Made Section "Relationship to OWL 2 DL" into an informative section
  • In correspondence theorem, distinction between datatype maps for OWL 2 Full and OWL 2 DL.
  • Restructured the "Interpretations" section.
  • Better alignment of the definitions of datatype facet spaces with OWL 2 DL. This needed significant changes to the "Interpretations" section, including the definition of a "OWL 2 datatype map", as well as to the semantic condition and the comprehension conditions for datatype restrictions.
  • Revised the descriptions of the comprehension conditions tables.
  • Added table of used namespaces in "Vocabulary" section.
  • Per the warning in an "at-risk" comment, the name of owl:dateTime has been change to xsd:dateTimeStamp to conform to the name that will be part of XML Schema.
  • The RDF Semantics term "datatype value" has been substituted by "data value", in accordance with the rest of the OWL 2 spec.
  • The "informative" mark has been removed from the Introduction section.
  • The correspondence theorem has been changed: It is not based on the comprehension conditions anymore, but on the new notion of "balanced entailments".
  • The comprehension conditions have been moved to the end of the section on DL-relationship.
  • The semantic condition and the comprehension conditions of datatype restrictions have been revised.
  • Added comprehension conditions for inverse property expressions.
  • Revised "Differences to Direct Semantics" section, and extended it by the issue of uninterpreted constructs.
  • Constructed proof sketch for Correspondence Theorem (might need further editing in the future)
  • Explanatation of D-interpretations has been extended by further semantic conditions from the RDF Semantics spec.
  • Bugfix: sequence expressions now defined for zero elements (as in OWL 1 Full).
  • Bugfix: explicitly mention that plain literals are also contained in the set LV of a D-interpretation (as in OWL 1 Full).
  • Renamed "comprehension principles" into "comprehension conditions" as in OWL 1 Full.
  • Added definition of "OWL 2 Full Satisfaction".
  • Changed terminology: "boolean class expressions" are now called "boolean connectives" to better match the rest of the OWL 2 specification.
  • Complete rewrite of "Ontologies" section: Mainly about syntax now.
  • Revised intro text of "Semantic Conditions" section.
  • Revised layout of complex tables.
  • Changed semantic condition for owl:datatypeComplementOf from an "iff" condition into an "if-then" condition, since this is sufficient for proving the correspondence theorem.
  • Added appendix for proofs of theorems in this document.
  • Splitted "Axiomatic Triples" section into subsections.
  • Changed use of term "lexical value" to "lexical form" according to WG Resolution on LC Comment 16 ("lexical value").
  • Changed RDF encoding of sub property chain axioms to single triple form according to WG Resolution with addendum on LC Comment 34 (TQ / "Property chain inclusion axioms").