Difference between revisions of "RDF-Based Semantics"
(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: | + | | 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 | ||
− | |||
− | |||
''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>). | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
<div id="tab-semcond-properties" class="center"> | <div id="tab-semcond-properties" class="center"> | ||
Line 1,757: | Line 1,747: | ||
| ⊆ IX × IX | | ⊆ IX × IX | ||
|- | |- | ||
− | | <span class="name">owl: | + | | <span class="name">owl:propertyChainAxiom</span> |
| ∈ IP | | ∈ IP | ||
− | | ⊆ | + | | ⊆ IP × 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 | + | 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>. | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
''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> | ||
|- | |- | ||
− | ! | + | ! colspan="3" style="text-align: center" | if ''s'' sequence of ''p<sub>1</sub>'' , … , ''p<sub>n</sub>'' ∈ IR then |
− | + | ||
|- | |- | ||
− | | | + | | ⟨ ''p'' , ''s'' ⟩ ∈ IEXT(''I''(<span class="name">owl:propertyChainAxiom</span>)) |
− | + | ! rowspan="1" style="text-align: center" | iff | |
− | + | | ''p'' ∈ IP ,<br/>''p<sub>1</sub>'' , … , ''p<sub>n</sub>'' ∈ IP ,<br/>∀ ''y<sub>0</sub>'' , … , ''y<sub>n</sub>'' : ⟨ ''y<sub>0</sub>'' , ''y<sub>1</sub>'' ⟩ ∈ IEXT(''p<sub>1</sub>'') and … and ⟨ ''y<sub>n-1</sub>'' , ''y<sub>n</sub>'' ⟩ ∈ IEXT(''p<sub>n</sub>'') implies ⟨ ''y<sub>0</sub>'' , ''y<sub>n</sub>'' ⟩ ∈ IEXT(''p'') | |
− | ! | + | |
− | + | ||
− | + | ||
− | + | ||
− | + | ||
|- | |- | ||
|} | |} | ||
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 | + | * ''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 [[#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__
- 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
- 1 Introduction (Informative)
- 2 Ontologies
- 3 Vocabulary
- 4 Interpretations
- 5 Semantic Conditions
- 5.1 Semantic Conditions for the Parts of the Universe
- 5.2 Semantic Conditions for Classes
- 5.3 Semantic Conditions for Properties
- 5.4 Semantic Conditions for Boolean Connectives
- 5.5 Semantic Conditions for Enumerations
- 5.6 Semantic Conditions for Property Restrictions
- 5.7 Semantic Conditions for Datatype Restrictions
- 5.8 Semantic Conditions for the RDFS Vocabulary
- 5.9 Semantic Conditions for Sub Property Chains
- 5.10 Semantic Conditions for Equivalence and Disjointness Axioms
- 5.11 Semantic Conditions for N-ary Axioms
- 5.12 Semantic Conditions for Inverse Property Axioms
- 5.13 Semantic Conditions for Property Characteristics
- 5.14 Semantic Conditions for Keys
- 5.15 Semantic Conditions for Negative Property Assertions
- 6 Axiomatic Triples (Informative)
- 7 Relationship to OWL 2 DL (Informative)
- 7.1 Differences to the OWL 2 Direct Semantics
- 7.2 Balancing
- 7.3 Correspondence Theorem
- 7.4 Comprehension Conditions
- 7.4.1 Comprehension Conditions for Sequences
- 7.4.2 Comprehension Conditions for Boolean Class Connectives
- 7.4.3 Comprehension Conditions for Enumerations
- 7.4.4 Comprehension Conditions for Property Restrictions
- 7.4.5 Comprehension Conditions for Datatype Restrictions
- 7.4.6 Comprehension Conditions for Inverse Property Expressions
- 8 Changes from OWL Full (Informative)
- 9 Appendix: Proofs for the Theorems (Informative)
- 10 Acknowledgments
- 11 References
- 12 Changelog
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 a_{1} has a relationship to another individual a_{2} based on a given property p, exactly if the pair 〈 a_{1} , a_{2} 〉 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.
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.
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].
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].
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).
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.
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.
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
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 a_{1} , … , a_{n} ∈ S" 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 z_{1} ∈ IR , … , z_{n} ∈ IR, such that
s = z_{1} ,
a_{1} ∈ S ,
〈 z_{1} , a_{1} 〉 ∈ IEXT(I(rdf:first)) ,
〈 z_{1} , z_{2} 〉 ∈ IEXT(I(rdf:rest)) ,
… ,
a_{n} ∈ S,
〈 z_{n} , a_{n} 〉 ∈ IEXT(I(rdf:first)) ,
〈 z_{n} , 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:c_{1} owl:unionOf (SEQ ex:c_{2} ex:c_{3})
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:c_{1} with the union of the classes denoted by ex:c_{2} and ex:c_{3}. 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:c_{1} ex:c_{2})
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.
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.
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)) ⊆ S_{1} × S_{2}", for a property name p and sets S_{1} and S_{2}, and given an RDF triple of the form "s p o" one can deduce that I(s) ∈ S_{1} and I(o) ∈ S_{2} 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).
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.
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 d_{1} , … , d_{n} ∈ IDC , n ≥ 1 , 〈 z , s 〉 ∈ IEXT(I(owl:intersectionOf)) |
z ∈ IDC | ||
if s sequence of c_{1} , … , c_{n} ∈ IR then | |||
〈 z , s 〉 ∈ IEXT(I(owl:intersectionOf)) | iff | z , c_{1} , … , c_{n} ∈ IC , ICEXT(z) = ICEXT(c_{1}) ∩ … ∩ ICEXT(c_{n}) | |
if | then | ||
s sequence of d_{1} , … , d_{n} ∈ IDC , n ≥ 1 , 〈 z , s 〉 ∈ IEXT(I(owl:unionOf)) |
z ∈ IDC | ||
if s sequence of c_{1} , … , c_{n} ∈ IR then | |||
〈 z , s 〉 ∈ IEXT(I(owl:unionOf)) | iff | z , c_{1} , … , c_{n} ∈ IC , ICEXT(z) = ICEXT(c_{1}) ∪ … ∪ ICEXT(c_{n}) |
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.
if | then | ||
---|---|---|---|
s sequence of v_{1} , … , v_{n} ∈ LV , n ≥ 1 , 〈 z , s 〉 ∈ IEXT(I(owl:oneOf)) |
z ∈ IDC | ||
if s sequence of a_{1} , … , a_{n} ∈ IR then | |||
〈 z , s 〉 ∈ IEXT(I(owl:oneOf)) | iff | z ∈ IC , ICEXT(z) = { a_{1} , … , a_{n} } |
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.
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 p_{1} , … , p_{n} ∈ IR , 〈 z , d 〉 ∈ IEXT(I(owl:allValuesFrom)) , 〈 z , s 〉 ∈ IEXT(I(owl:onProperties)) |
p_{1} , … , p_{n} ∈ IODP , d ∈ IDC , ICEXT(z) = { x | ∀ y_{1} , … , y_{n} ∈ LV : 〈 x , y_{k} 〉 ∈ IEXT(p_{k}) for each 1 ≤ k ≤ n implies 〈 y_{1} , … , y_{n} 〉 ∈ 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 p_{1} , … , p_{n} ∈ IR , 〈 z , d 〉 ∈ IEXT(I(owl:someValuesFrom)) , 〈 z , s 〉 ∈ IEXT(I(owl:onProperties)) |
p_{1} , … , p_{n} ∈ IODP , d ∈ IDC , ICEXT(z) = { x | ∃ y_{1} , … , y_{n} ∈ LV : 〈 x , y_{k} 〉 ∈ IEXT(p_{k}) for each 1 ≤ k ≤ n and 〈 y_{1} , … , y_{n} 〉 ∈ 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.
if | then |
---|---|
s sequence of z_{1} , … , z_{n} ∈ IR , f_{1} , … , f_{n} ∈ IP , 〈 z , d 〉 ∈ IEXT(I(owl:onDatatype)) , 〈 z , s 〉 ∈ IEXT(I(owl:withRestrictions)) , 〈 z_{1} , v_{1} 〉 ∈ IEXT(f_{1}) , … , 〈 z_{n} , v_{n} 〉 ∈ IEXT(f_{n}) |
z , d ∈ IDC , f_{1} , … , f_{n} ∈ IODP , v_{1} , … , v_{n} ∈ LV , 〈 f_{1} , v_{1} 〉 , … , 〈 f_{n} , v_{n} 〉 ∈ IFS(d) , ICEXT(z) = ICEXT(d) ∩ IF2V(d)(〈 f_{1} , v_{1} 〉) ∩ … ∩ IF2V(d)(〈 f_{n} , v_{n} 〉) |
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.
〈 c_{1} , c_{2} 〉 ∈ IEXT(I(rdfs:subClassOf)) | iff | c_{1} , c_{2} ∈ IC , ICEXT(c_{1}) ⊆ ICEXT(c_{2}) |
---|---|---|
〈 p_{1} , p_{2} 〉 ∈ IEXT(I(rdfs:subPropertyOf)) | p_{1} , p_{2} ∈ IP , IEXT(p_{1}) ⊆ IEXT(p_{2}) | |
〈 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.
if s sequence of p_{1} , … , p_{n} ∈ IR then | ||
---|---|---|
〈 p , s 〉 ∈ IEXT(I(owl:propertyChainAxiom)) | iff | p ∈ IP , p_{1} , … , p_{n} ∈ IP , ∀ y_{0} , … , y_{n} : 〈 y_{0} , y_{1} 〉 ∈ IEXT(p_{1}) and … and 〈 y_{n-1} , y_{n} 〉 ∈ IEXT(p_{n}) implies 〈 y_{0} , y_{n} 〉 ∈ 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.
〈 a_{1} , a_{2} 〉 ∈ IEXT(I(owl:sameAs)) | iff | a_{1} = a_{2} |
---|---|---|
〈 a_{1} , a_{2} 〉 ∈ IEXT(I(owl:differentFrom)) | a_{1} ≠ a_{2} | |
〈 c_{1} , c_{2} 〉 ∈ IEXT(I(owl:equivalentClass)) | c_{1} , c_{2} ∈ IC , ICEXT(c_{1}) = ICEXT(c_{2}) | |
〈 c_{1} , c_{2} 〉 ∈ IEXT(I(owl:disjointWith)) | c_{1} , c_{2} ∈ IC , ICEXT(c_{1}) ∩ ICEXT(c_{2}) = ∅ | |
〈 p_{1} , p_{2} 〉 ∈ IEXT(I(owl:equivalentProperty)) | p_{1} , p_{2} ∈ IP , IEXT(p_{1}) = IEXT(p_{2}) | |
〈 p_{1} , p_{2} 〉 ∈ IEXT(I(owl:propertyDisjointWith)) | p_{1} , p_{2} ∈ IP , IEXT(p_{1}) ∩ IEXT(p_{2}) = ∅ | |
if s sequence of c_{1} , … , c_{n} ∈ IR then | ||
〈 c , s 〉 ∈ IEXT(I(owl:disjointUnionOf)) | iff | c , c_{1} , … , c_{n} ∈ IC , ICEXT(c) = ICEXT(c_{1}) ∪ … ∪ ICEXT(c_{n}) , ICEXT(c_{j}) ∩ ICEXT(c_{k}) = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
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.
if | then |
---|---|
s sequence of a_{1} , … , a_{n} ∈ IR , z ∈ ICEXT(I(owl:AllDifferent)) , 〈 z , s 〉 ∈ IEXT(I(owl:distinctMembers)) |
a_{j} ≠ a_{k} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
if | then exists z ∈ IR |
s sequence of a_{1} , … , a_{n} ∈ IR , a_{j} ≠ a_{k} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
z ∈ ICEXT(I(owl:AllDifferent)) , 〈 z , s 〉 ∈ IEXT(I(owl:distinctMembers)) |
if | then |
s sequence of a_{1} , … , a_{n} ∈ IR , z ∈ ICEXT(I(owl:AllDifferent)) , 〈 z , s 〉 ∈ IEXT(I(owl:members)) |
a_{j} ≠ a_{k} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
if | then exists z ∈ IR |
s sequence of a_{1} , … , a_{n} ∈ IR , a_{j} ≠ a_{k} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
z ∈ ICEXT(I(owl:AllDifferent)) , 〈 z , s 〉 ∈ IEXT(I(owl:members)) |
if | then |
s sequence of c_{1} , … , c_{n} ∈ IR , z ∈ ICEXT(I(owl:AllDisjointClasses)) , 〈 z , s 〉 ∈ IEXT(I(owl:members)) |
c_{1} , … , c_{n} ∈ IC , ICEXT(c_{j}) ∩ ICEXT(c_{k}) = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
if | then exists z ∈ IR |
s sequence of c_{1} , … , c_{n} ∈ IC , ICEXT(c_{j}) ∩ ICEXT(c_{k}) = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
z ∈ ICEXT(I(owl:AllDisjointClasses)) , 〈 z , s 〉 ∈ IEXT(I(owl:members)) |
if | then |
s sequence of p_{1} , … , p_{n} ∈ IR , z ∈ ICEXT(I(owl:AllDisjointProperties)) , 〈 z , s 〉 ∈ IEXT(I(owl:members)) |
p_{1} , … , p_{n} ∈ IP , IEXT(p_{j}) ∩ IEXT(p_{k}) = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
if | then exists z ∈ IR |
s sequence of p_{1} , … , p_{n} ∈ IP , IEXT(p_{j}) ∩ IEXT(p_{k}) = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
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.
〈 p_{1} , p_{2} 〉 ∈ IEXT(I(owl:inverseOf)) | iff | p_{1} , p_{2} ∈ IP , IEXT(p_{1}) = { 〈 x , y 〉 | 〈 y , x 〉 ∈ IEXT(p_{2}) } |
---|
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.
p ∈ ICEXT(I(owl:FunctionalProperty)) | iff | p ∈ IP , ∀ x , y_{1} , y_{2} : 〈 x , y_{1} 〉 ∈ IEXT(p) and 〈 x , y_{2} 〉 ∈ IEXT(p) implies y_{1} = y_{2} |
---|---|---|
p ∈ ICEXT(I(owl:InverseFunctionalProperty)) | p ∈ IP , ∀ x_{1} , x_{2} , y : 〈 x_{1} , y 〉 ∈ IEXT(p) and 〈 x_{2} , y 〉 ∈ IEXT(p) implies x_{1} = x_{2} | |
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.
if s sequence of p_{1} , … , p_{n} ∈ IR then | ||
---|---|---|
〈 c , s 〉 ∈ IEXT(I(owl:hasKey)) | iff | c ∈ IC , p_{1} , … , p_{n} ∈ IP , ∀ x , y , z_{1} , … , z_{n} : if x ∈ ICEXT(c) and y ∈ ICEXT(c) and for each 1 ≤ k ≤ n 〈 x , z_{k} 〉 ∈ IEXT(p_{k}) and 〈 y , z_{k} 〉 ∈ IEXT(p_{k}) 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 a_{1} does not stand in a relationship p with another individual a_{2}. 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.
if | then |
---|---|
〈 z , a_{1} 〉 ∈ IEXT(I(owl:sourceIndividual)) , 〈 z , p 〉 ∈ IEXT(I(owl:assertionProperty)) , 〈 z , a_{2} 〉 ∈ IEXT(I(owl:targetIndividual)) |
〈 a_{1} , a_{2} 〉 ∉ IEXT(p) |
if | then exists z ∈ IR |
a_{1} ∈ IR , p ∈ IP , a_{2} ∈ IR , 〈 a_{1} , a_{2} 〉 ∉ IEXT(p) |
〈 z , a_{1} 〉 ∈ IEXT(I(owl:sourceIndividual)) , 〈 z , p 〉 ∈ IEXT(I(owl:assertionProperty)) , 〈 z , a_{2} 〉 ∈ 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 "S_{1} ⊆ S_{2}" for some sets S_{1} and S_{2}, then this corresponds to some RDF triple C_{1} owl:subClassOf C_{2}, where C_{1} and C_{2} are the IRI references of some classes with ICEXT(I(C_{1})) = S_{1} and ICEXT(I(C_{2})) = S_{2}, 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)) ⊆ S_{1} × S_{2}" for some sets S_{1} and S_{2}, then this entry corresponds to some RDF triples of the forms "E rdfs:domain C_{1}" and "E rdfs:range C_{2}", where C_{1} and C_{2} are the IRI references of some classes with ICEXT(I(C_{1})) = S_{1} and ICEXT(I(C_{2})) = S_{2}, 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)
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 G_{1} and G_{2}, will result in a new pair of RDF graphs G_{1}^{*} and G_{2}^{*}, that again are OWL 2 DL ontologies in RDF graph form. The semantic meaning of G_{1}^{*} will equals that of G_{1} under the OWL 2 Direct Semantics, and likewise for G_{2}^{*} compared to G_{2}. Hence, G_{1}^{*} will OWL 2 Direct entail G_{2}^{*} if and only if G_{1} OWL 2 Direct entails G_{2}.
Nevertheless, the new RDF graphs G_{1}^{*} and G_{2}^{*}, which result from the ontology balancing process, will generally differ syntactically from the original RDF graphs G_{1} and G_{2}. 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 G_{1}^{*} OWL 2 Full entails G_{2}^{*} whenever G_{1} OWL 2 Direct entails G_{2}. 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.
7.1 Differences to the OWL 2 Direct Semantics
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 G_{1} and G_{2}:
G_{1} := {
(1) ex:c1 rdf:type owl:Class .
(2) ex:c2 rdf:type owl:Class .
(3) ex:c1 rdfs:subClassOf ex:c2 .
}
G_{2} := {
(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 G_{1} and G_{2} are OWL 2 DL ontologies in RDF graph form, and it is easy to verify that G_{1} OWL 2 Direct entails G_{2}. For this to hold, the typing triples (1) and (2) in G_{1} and (1), (2) and (3) in G_{2} 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 G_{2} does not have a semantic meaning under the OWL 2 Direct Semantics.
However, all the typing triples and the annotation in G_{2} are actually interpreted by OWL 2 Full. Since the typing triple (3) and the annotation triple (4) of G_{2} do not also occur in G_{1}, there are OWL 2 Full interpretations that satisfy G_{1} but not the triples (3) and (4). Hence, G_{1} does not OWL 2 Full entail G_{2}.
This problem can be overcome by copying the triples (3) and (4) to G_{1}, leading to the new graph G_{1a}
G_{1a} := {
(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 G_{1a} 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 G_{1}, i.e., G_{1a} and G_{1} are semantically equivalent. From this follows that G_{1a} OWL 2 Direct entails G_{2} if and only if G_{1} OWL 2 Direct entails G_{2}. However, the situation has changed for OWL 2 Full, since the triples (3) and (4) of G_{2} are now satisfied by every OWL 2 Full interpretation that satisfies G_{1a}.
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, G_{1a} OWL 2 Direct entails G_{2}. However, in OWL 2 Full this entailment does not hold. This is mainly due to triple (6) in G_{2}, 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 G_{2} 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 G_{2} 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 G_{2} 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 G_{1a}, resulting in the new graph G_{1b}
G_{1b} := {
(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 G_{2} 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 G_{1a}. 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 G_{1b} (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 G_{1b} 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., G_{1b} and G_{1a} are semantically equivalent. From this follows that G_{1b} OWL 2 Direct entails G_{2} if and only if G_{1a} OWL 2 Direct entails G_{2}. However, the situation has changed for OWL 2 Full, since all the triples of G_{2} are now satisfied by every OWL 2 Full interpretation that satisfies G_{1b}. As the added tautological axiom has been build from the encoding of the union class expression consisting of the triples (6) and (5) in G_{2}, and since this subgraph consists of the original blank node, the existence of the missing individual in G_{2} is finally ensured (and in addition, the existence of the list in triple (6) of G_{2} 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, G_{1} and G_{2}, to receive a semantically equivalent OWL 2 Direct entailment consisting again of two OWL 2 DL ontologies in RDF graph form, G_{1b} and G_{2}, for which it is ensured that G_{1b} OWL 2 Full entails G_{2}, either. Section 7.2 will generalize this idea of "balancing" to arbitrary OWL 2 Direct entailment queries.
7.2 Balancing
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 〈 G_{1} , G_{2} 〉 is called OWL 2 balanced, iff G_{1} and G_{2} are OWL 2 DL ontologies in RDF graph form, with F(G_{1}) and F(G_{2}) 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 G_{1} and G_{2}, respectively, such that all the following additional conditions hold:
- F(G_{1}) and F(G_{2}) mutually meet the global syntactic restrictions on OWL 2 DL ontologies as specified in [OWL 2 Specification].
- G_{2} 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 G_{2} is also a subgraph of G_{1}, provided that g is the RDF encoding of:
- an ontology header (Table 4 in [OWL 2 RDF Mapping]), or
- an entity declaration (Table 7 in [OWL 2 RDF Mapping]), or
- a property expression (Table 11 in [OWL 2 RDF Mapping]), or
- a class expression (Tables 13 and 15 in [OWL 2 RDF Mapping]), or
- a data range expression (Tables 12 and 14 in [OWL 2 RDF Mapping]).
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 〈 G_{1}^{*} , G_{2}^{*} 〉, where G_{1}^{*} and G_{2}^{*} are OWL 2 DL ontologies in RDF graph form, with F(G_{1}^{*}) and F(G_{2}^{*}) 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 G_{1}^{*} and G_{2}^{*}, respectively, such that F(G_{1}^{*}) and F(G_{2}^{*}) 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 〈 G_{1} , G_{2} 〉, where G_{1} and G_{2} are OWL 2 DL ontologies in RDF graph form, with F(G_{1}) and F(G_{2}) being the corresponding OWL 2 DL ontologies in Functional Syntax form that result from applying the reverse OWL 2 RDF mapping to G_{1} and G_{2}, 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 〈 G_{1} , G_{2} 〉 is OWL 2 balanced according to Definition 7.1.
- F(G_{1}) OWL 2 Direct entails F(G_{1}^{*}) with respect to F(D), and F(G_{1}^{*}) OWL 2 Direct entails F(G_{1}) with respect to F(D).
- F(G_{2}) OWL 2 Direct entails F(G_{2}^{*}) with respect to F(D), and F(G_{2}^{*}) OWL 2 Direct entails F(G_{2}) with respect to F(D).
Proof: See Appendix 9.1.
7.3 Correspondence Theorem
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 G_{1}^{*} and G_{2}^{*} be RDF graphs that are OWL 2 DL ontologies in RDF graph form, with F(G_{1}^{*}) and F(G_{2}^{*}) 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 G_{1}^{*} and G_{2}^{*}, respectively, such that F(G_{1}^{*}) and F(G_{2}^{*}) mutually meet the global syntactic restrictions on OWL 2 DL ontologies as specified in [OWL 2 Specification].
Then, there exist RDF graphs G_{1} and G_{2} that are OWL 2 DL ontologies in RDF graph form, with F(G_{1}) and F(G_{2}) being the corresponding OWL 2 DL ontologies in Functional Syntax form that result from applying the reverse OWL 2 RDF mapping to G_{1} and G_{2}, respectively, such that all the following conditions hold:
- F(G_{1}) and F(G_{2}) mutually meet the global syntactic restrictions on OWL 2 DL ontologies.
- F(G_{1}) OWL 2 Direct entails F(G_{2}) with respect to F(D), if and only if F(G_{1}^{*}) OWL 2 Direct entails F(G_{2}^{*}) with respect to F(D).
- If F(G_{1}) OWL 2 Direct entails F(G_{2}) with respect to F(D), then G_{1} OWL 2 Full entails G_{2} with respect to D.
Proof Sketch: See Appendix 9.2.
Some technical notes:
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.
Let D be an OWL 2 Full datatype map according to definition 4.1. The corresponding OWL 2 Direct datatype map F(D) := ( N_{DT} , N_{LS} , N_{FS} , ⋅ ^{DT} , ⋅ ^{LS} , ⋅ ^{FS} ) is given as follows.
- The set of datatypes N_{DT} 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 N_{LS}(ddd) := LS(d), for each IRI reference ddd ∈ N_{DT} and datatype d, where 〈 ddd , d 〉 ∈ D.
- The facet space N_{FS}(ddd) := FS(d), for each IRI reference ddd ∈ N_{DT} and datatype d, where 〈 ddd , d 〉 ∈ D.
- The value space (ddd) ^{DT} := VS(d), for each IRI reference ddd ∈ N_{DT} and datatype d, where 〈 ddd , d 〉 ∈ D.
- The data value (〈 a , ddd 〉) ^{LS} := L2V(d)(a), for each IRI reference ddd ∈ N_{DT} and datatype d, where 〈 ddd , d 〉 ∈ D, and for each lexical form a ∈ N_{LS}(ddd).
- The interpretation of the facet-value pair (〈 F , v 〉) ^{FS} := F2V(d)(〈 F , v 〉), for each IRI reference ddd ∈ N_{DT} and datatype d, where 〈 ddd , d 〉 ∈ D, and for each facet-value pair 〈 F , v 〉 ∈ N_{FS}(ddd).
7.4 Comprehension Conditions
The method given in Section 7.2 to balance a graph G_{1} with respect to another graph G_{2} has been defined only for cases, in which G_{1} and G_{2} 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 G_{1} and G_{2}, 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.
if | then exists z_{1} , … , z_{n} ∈ IR |
---|---|
a_{1} , … , a_{n} ∈ IR | 〈 z_{1} , a_{1} 〉 ∈ IEXT(I(rdf:first)) , 〈 z_{1} , z_{2} 〉 ∈ IEXT(I(rdf:rest)) , … , 〈 z_{n} , a_{n} 〉 ∈ IEXT(I(rdf:first)) , 〈 z_{n} , 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.
if | then exists z ∈ IR |
---|---|
c ∈ IC | 〈 z , c 〉 ∈ IEXT(I(owl:complementOf)) |
d ∈ IDC | 〈 z , d 〉 ∈ IEXT(I(owl:datatypeComplementOf)) |
s sequence of c_{1} , … , c_{n} ∈ IC | 〈 z , s 〉 ∈ IEXT(I(owl:intersectionOf)) |
s sequence of c_{1} , … , c_{n} ∈ 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.
if | then exists z ∈ IR |
---|---|
s sequence of a_{1} , … , a_{n} ∈ 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].
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 p_{1} , … , p_{n} ∈ 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 p_{1} , … , p_{n} ∈ 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.
if | then exists z ∈ IR , s sequence of z_{1} , … , z_{n} ∈ IR |
---|---|
d ∈ IDC , f_{1} , … , f_{n} ∈ IODP , v_{1} , … , v_{n} ∈ LV , 〈 f_{1} , v_{1} 〉 , … , 〈 f_{n} , v_{n} 〉 ∈ IFS(d) |
〈 z , d 〉 ∈ IEXT(I(owl:onDatatype)) , 〈 z , s 〉 ∈ IEXT(I(owl:withRestrictions)) , 〈 z_{1} , v_{1} 〉 ∈ IEXT(f_{1}) , … , 〈 z_{n} , v_{n} 〉 ∈ IEXT(f_{n}) |
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.
if | then exists z ∈ IR |
---|---|
p ∈ IP | 〈 z , p 〉 ∈ IEXT(I(owl:inverseOf)) |
8 Changes from OWL Full (Informative)
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 "R_{I}", "P_{I}", "C_{I}", "EXT_{I}", "CEXT_{I}", "S_{I}", "L_{I}" and "LV_{I}" 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
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 G_{1} and G_{2} have no common blank nodes. Otherwise, a preprocessing step will substitute all blank nodes in G_{1} for fresh blank nodes that do not occur in G_{2}.
Since G_{2} 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 G_{2} 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 G_{1}^{*}, is a copy of G_{1}. Now, the following steps are performed on every subgraph g ⊆ G_{2} that has been identified by the adapted canonical parsing process:
- If g corresponds to an entity declaration, then g is copied unchanged to G_{1}^{*}.
- 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 G_{1}^{*}.
- 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 G_{1}^{*}.
- 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 G_{1}^{*}.
Property 1) of the theorem results from the fact that G_{1} is an OWL 2 DL ontology in RDF graph form, and G_{1}^{*} differs from G_{1} 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 G_{2} are added to G_{1}, G_{1}^{*} 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 G_{1}^{*} differs from G_{1} 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 G_{1}^{*} and G_{2}. Finally, an algorithm exists for the construction of G_{1}^{*}, 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.
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 V_{I} that covers all the names (IRI references and literals) occurring in the RDF graphs G_{1} and G_{2}, and let I OWL 2 Full satisfy G_{1}. It will be shown that I OWL 2 Full satisfies G_{2}.
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 V_{J} that covers all the names (IRI references and literals) occurring in the OWL 2 DL ontologies in Functional Syntax form F(G_{1}) and F(G_{2}). J will be defined in a way such that it closely corresponds to I on those parts of the vocabularies V_{I} and V_{J} that cover G_{1} and G_{2}, and F(G_{1}) and F(G_{2}), respectively.
G_{1} and G_{2} are OWL 2 DL ontologies in RDF graph form that are mapped by the reverse RDF mapping to F(G_{1}) and F(G_{2}), respectively. From this follows that the same literals are used in both G_{1} and F(G_{1}), and in both G_{2} and F(G_{2}), respectively, and that there are entity declarations in F(G_{1}) and F(G_{2}) for every non-builtin IRI reference occurring in G_{1} and G_{2}, respectively. For each entity declaration of the form Declaration(T(u)) in F(G_{1}) and F(G_{2}), where T is the entity type for some IRI reference u, a typing triple of the form u rdf:type t exists in G_{1} or G_{2}, respectively, where t denotes the class representing the part of the OWL 2 Full universe that corresponds to T; and vice versa.
Since G_{1} is OWL 2 balanced w.r.t. G_{2}, all the entity declarations of F(G_{2}) are also contained in F(G_{1}), and therefore all the typing triples of G_{2} that correspond to some entity declaration in F(G_{2}) are also contained in G_{1}. Since I OWL 2 Full satisfies G_{1}, all these "declaring" typing triples are OWL 2 Full satisfied by I, and thus all non-builtin IRI references in G_{1} and G_{2} 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 V_{J} for the datatype map F(D) can now be defined.
The vocabulary V_{J} := ( V_{C} , V_{OP} , V_{DP} , V_{I} , V_{DT} , V_{LT} , V_{FA} ) is defined as follows.
- The set V_{C} of class names contains all IRI references that are declared as classes in F(G_{1}).
- The set V_{OP} of object property names contains all IRI references that are declared as object properties in F(G_{1}).
- The set V_{DP} of data property names contains all IRI references that are declared as data properties in F(G_{1}).
- The set V_{I} of individual names contains all IRI references that are declared as named individuals in F(G_{1}).
The sets V_{DT} of datatype names, V_{LT} of literals, and V_{FA} 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(G_{1}):
- If u is declared as a named individual, then set u^{I} := I(u), since G_{1} contains the triple "u rdf:type owl:NamedIndividual", i.e., I(u) ∈ IR.
- If u is declared as a class, then set u^{C} := 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 u^{OP} := 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 u^{DP} := IEXT(I(u)), since the graphs contain the triple "u rdf:type owl:DatatypeProperty", i.e., I(u) ∈ IODP.
Note that G_{1} 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 G_{2} 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 G_{1} and G_{2} 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 G_{1} and G_{2} are mapped by the OWL 2 RDF mapping to the same literals in the corresponding interpreted language constructs of F(G_{1}) and F(G_{2}), 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 G_{1}, it has to be shown that J OWL 2 Direct satisfies F(G_{1}). For this to hold it will be sufficient to show that J OWL 2 Direct satisfies every axiom occurring in F(G_{1}). Let A be an axiom occurring in F(G_{1}), and let g_{A} be the subgraph of G_{1} 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 G_{1}, all the triples occuring in g_{A} 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 g_{A} will apply. This will reveal certain semantic relationships that, according to I, hold between the denotations of the names occurring in g_{A}. These semantic relationships are, roughly speaking, the semantic consequences of the axiom that is encoded by the triples in g_{A}.
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 g_{A}, 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 g_{A} 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 g_{A}. Both OWL 2 Full and the OWL 2 Direct Semantics treat blank nodes as existential variables in an ontology. Since I satisfies g_{A}, b can be mapped to an individual x in IR such that g_{A} 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(G_{1}), 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(G_{1}).
Due to the reverse OWL 2 RDF Mapping, g_{A} has the form
g_{A} = {
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 G_{1}, all the triples in g_{A} 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 g_{A} 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:c1) ^{C} ⊆ (ex:c2) ^{C} ∪ (ex:c3) ^{C} .
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(G_{1}), and since F(G_{1}) OWL 2 Direct entails F(G_{2}), it follows that J OWL 2 Direct satisfies F(G_{2}).
The next step will be to show that I OWL 2 Full satisfies G_{2}. For this to hold, I needs to OWL 2 Full satisfy all the triples occurring in G_{2}, taking into account the premise that an OWL 2 Full interpretation is required to meet all the OWL 2 Full semantic conditions. Since G_{2} 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(G_{2}) only consists of entity declarations and axioms. Further, since G_{2} is an OWL 2 DL ontology in RDF graph form, every triple occuring in G_{2} belongs to some subgraph of G_{2} that is mapped by the reverse OWL 2 RDF mapping to one of the entity declarations or axioms contained in F(G_{2}).
For entity declarations, let A be an entity declaration in F(G_{2}), and let g_{A} be the corresponding subgraph of G_{2}. Since G_{1} is OWL 2 balanced w.r.t. G_{2}, A occurs in F(G_{1}), and hence g_{A} is a subgraph of G_{1}. Since I OWL 2 Full satisfies G_{1}, I in particular OWL 2 Full satisfies g_{A}.
For axioms, let A be an axiom in F(G_{2}), and let g_{A} be the corresponding subgraph of G_{2}. It is possible to prove that I OWL 2 Full satisfies g_{A}, 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 g_{A}, are met. This will allow to apply the semantic condition, from which will follow that all the triples in g_{A} 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 g_{A} 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 g_{A}. The basic idea is as follows:
For every non-builtin IRI reference u occurring in g_{A}, u also occurs in A, and, therefore, there are one or more entity declarations in F(G_{2}), 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 G_{2}, 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(G_{2}), and e being the corresponding subgraph in G_{2}, 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(G_{2}), 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 G_{2}, 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 g_{A}.
Finally, for the blank nodes occurring in g_{A}, it becomes clear from the fact that G_{2} is an OWL DL ontology in RDF graph form that only certain kinds of subgraphs of g_{A} 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 g_{A}.
- Case 2: A blank node is the "root" node of the multi-triple RDF encoding g_{A} of A (for g_{A} 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 g_{A} 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_{E} of an expression in A (for g_{E} 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 G_{1} is OWL 2 balanced w.r.t. G_{2}, g_{E} also occurs in G_{1}. Since I OWL 2 Full satisfies G_{1}, g_{E} 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_{A}, and g_{A} 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_{A} hold.
This basic idea is now demostrated in more detail for a single example axiom A in F(G_{2}), 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(G_{2}).
Due to the reverse OWL 2 RDF Mapping, g_{A} has the form
g_{A} = {
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 g_{A} correspond to typing triples
ex:c1 rdf:type owl:Class,
ex:c2 rdf:type owl:Class and
ex:c3 rdf:type owl:Class
in G_{2}, respectively. Based on the premise that G_{1} is OWL 2 balanced w.r.t. G_{2}, 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:c1) ^{C} ⊆ (ex:c2) ^{C} ∪ (ex:c3) ^{C} .
Applying the definition of J results in the following semantic relationship w.r.t. I that holds between the denotations of the names in g_{A}:
ICEXT(I(ex:c1)) ⊆ ICEXT(I(ex:c2)) ∪ ICEXT(I(ex:c3))
The subgraph g_{E} of g_{A}, given by
g_{E} := {
_:x rdf:type owl:Class .
_:x owl:unionOf (SEQ c2 c3) .
}
corresponds to a union class expression in A. Since G_{1} is OWL 2 balanced w.r.t. G_{2}, g_{E} is also a subgraph of G_{1} (it will be assumed that the same blank nodes are used in both instances of g_{E} in order to simplify the argument). Since both G_{1} and G_{2} are OWL 2 DL ontologies in RDF graph form, the blank nodes occurring in g_{E} do not occur outside of g_{E}, neither in G_{1} nor in G_{2}.
Since I OWL 2 Full satisfies G_{1}, according to the semantic conditions for RDF graphs with blank nodes (see Section 1.5 of [RDF Semantics]), a mapping B from blank(g_{E}) to IR exists, where blank(g_{E}) is the set of all blank nodes in g_{E}, such that the extended interpretation I+B OWL 2 Full satisfies all the triples in g_{E}. 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 g_{A}.
Hence, w.r.t. existential blank node semantics, I OWL 2 Full satisfies all the triples in g_{A}.
To conclude, for every OWL 2 Full interpretation I that OWL 2 Full satisfies G_{1} it turns out that I also OWL 2 Full satisfies G_{2}. Hence, G_{1} OWL 2 Full entails G_{2}. 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
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").