W3C

OWL 2 Web Ontology Language:
RDF-Based Semantics

W3C Editor's Draft 22 September 2008

This version:
http://www.w3.org/2007/OWL/draft/ED-owl2-rdf-based-semantics-20080922/
Latest editor's draft:
http://www.w3.org/2007/OWL/draft/owl2-rdf-based-semantics/
Authors:
Michael Schneider, FZI Research Center for Information Technology

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

Abstract

OWL 2 extends the W3C OWL Web Ontology Language with a small but useful set of features that have been requested by users, for which effective reasoning algorithms are now available, and that OWL tool developers are willing to support. The new features include extra syntactic sugar, additional property and qualified cardinality constructors, extended datatype support, simple metamodelling, and extended annotations.
This document provides the RDFS-compatible model-theoretic semantics for OWL 2, called "OWL 2 Full".

Status of this Document

May Be Superseded

This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current W3C publications and the latest revision of this technical report can be found in the W3C technical reports index at http://www.w3.org/TR/.

This document is being published as one of a set of 8 documents:

  1. Structural Specification and Functional-Style Syntax
  2. Model-Theoretic Semantics
  3. RDF-Based Semantics (this document)
  4. Mapping to RDF Graphs
  5. XML Serialization
  6. Profiles
  7. Conformance and Test Cases
  8. A Datatype for Internationalized Text

Please Comment By ASAP

The OWL Working Group seeks public feedback on these Working Drafts. Please send your comments to public-owl-comments@w3.org (public archive). If possible, please offer specific changes to the text that would address your concern. You may also wish to check the Wiki Version of this document for internal-review comments and changes being drafted which may address your concerns.

No Endorsement

Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.

Patents

This document was produced by a group operating under the 5 February 2004 W3C Patent Policy. W3C maintains a public list of any patent disclosures made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) must disclose the information in accordance with section 6 of the W3C Patent Policy.

Contents


Editor's Note: Hints to Reviewers:
Editor's Note: Jie Bao suggests:

Finally we will add "informative" and "normative" to each section's title, following RDF and OWL 1 traditions.

Editor's Note: Open Question: There is an open issue with OWL 2 Full's support of n-ary datatypes. I suppose that we need to introduce a new sort of extension, a "datarange extension of arity n", which associates an individual with a set of n-tuples of individuals. Affected parts of the document would be: Introduction, Interpretations, the Semantic Conditions and the Comprehension Principles for the Datatype Complement, and the Restrictions on N-ary Datatypes ("owl:onProperties"). Should this be the case, then the latter semantic conditions have to be considered broken at the moment, since n-tuples of individuals then cannot be instances of class extensions.

However, Peter Patel-Schneider has stated a different position in this email that there is no need to introduce such an additional sort of extension.

1 Introduction

This model-theoretic semantics for OWL 2, called "OWL 2 Full", is an extension of the semantics defined in the RDF Semantics, and defines the OWL 2 semantic extension of RDFS. The document presented here extends the RDF Semantics document, and therefore has to be read in conjunction with it.

OWL 2 Full is specified for the OWL 2 Full vocabulary in the form of a vocabulary interpretation, which is defined on the OWL 2 Full universe. The OWL 2 Full universe is identified with the RDFS universe, and comprises the set of all individuals. It is further divided into sub parts, namely the classes, the properties, and the interpretations of the literals, which are thus also individuals. Every class has a set of individuals associated with it, the so called "class extension", which is distinguished from the class itself. Analog, every property is associated with a "property extension", which is a binary relation, i.e. a set of pairs of individuals. The classes subsume the interpretations of the datatypes, and the properties subsume the data properties, the annotation properties, and the ontology properties. Individuals may play different roles at the same time. They can, for example, be both a class and a property, or both a data property and an annotation property.

Editor's Note: Jie Bao proposes to have some figure here visualizing the parts hierarchy and possibly the IEXT/ICEXT concept as explained in the text above.

Every RDF graph is a syntactically valid OWL 2 Full ontology, which receives its semantic meaning by applying the set of OWL 2 Full semantic conditions. For ontologies importing other ontologies, the whole imports closure of that ontology will generally have to be taken into account.

A strong relationship holds between the semantics of OWL 2 Full and OWL 2 DL, in that OWL 2 Full is, in some sense, able to reflect all logical conclusions of OWL 2 DL. The precise relationship is stated by the OWL 2 correspondence theorem.

The italicized keywords MUST, MUST NOT, SHOULD, SHOULD NOT, and MAY specify certain aspects of the normative behavior of OWL 2 tools, and are interpreted as specified in RFC 2119 [RFC 2119].

2 Vocabulary

The OWL 2 Full vocabulary is a set of URI references in the OWL namespace, owl:, which is given by the URI reference

 http://www.w3.org/2002/07/owl#

Table 2.1 lists the OWL 2 Full vocabulary, which extends the RDF and RDFS vocabulary as specified by Sections 3.1 and 4.1 of the RDF Semantics. Excluded are those URI references from the OWL namespace, which are mentioned in one of the other tables in this section.

Table 2.1: OWL 2 Full Vocabulary
owl:AllDifferent owl:AllDisjointClasses owl:AllDisjointProperties owl:allValuesFrom owl:Annotation owl:AnnotationProperty owl:assertionProperty owl:AsymmetricProperty owl:Axiom owl:backwardCompatibleWith owl:BottomDataProperty owl:BottomObjectProperty owl:cardinality owl:Class owl:complementOf owl:DataRange owl:datatypeComplementOf owl:DatatypeProperty owl:deprecated owl:DeprecatedClass owl:DeprecatedProperty owl:differentFrom owl:disjointUnionOf owl:disjointWith owl:distinctMembers owl:equivalentClass owl:equivalentProperty owl:FunctionalProperty owl:hasKey owl:hasValue owl:imports owl:incompatibleWith owl:intersectionOf owl:InverseFunctionalProperty owl:inverseOf owl:IrreflexiveProperty owl:maxCardinality owl:maxQualifiedCardinality owl:members owl:minCardinality owl:minQualifiedCardinality owl:NamedIndividual owl:NegativePropertyAssertion owl:Nothing owl:object owl:ObjectProperty owl:onClass owl:onDataRange owl:onDatatype owl:oneOf owl:onProperty owl:onProperties owl:Ontology owl:OntologyProperty owl:predicate owl:priorVersion owl:propertyChain owl:propertyDisjointWith owl:qualifiedCardinality owl:ReflexiveProperty owl:Restriction owl:sameAs owl:SelfRestriction 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 URI reference owl:DataRange has been deprecated as of OWL 2. The URI reference rdfs:Datatype should be used instead.

Table 2.2 lists the set of datatypes supported by OWL 2 Full. The interpretation of rdf:XMLLiteral is described in Section 3.1 of the RDF Semantics. The interpretation of all other datatypes is described in Section 4 of the OWL 2 DL Structural Specification.

Table 2.2: Datatypes of OWL 2 Full
xsd:anyURI xsd:base64Binary xsd:boolean xsd:byte owl:dateTime xsd:decimal xsd:double xsd:ENTITY xsd:float xsd:hexBinary xsd:ID xsd:IDREF 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:real owl:realPlus xsd:short xsd:string rdf:text xsd:token xsd:unsignedByte xsd:unsignedInt xsd:unsignedLong xsd:unsignedShort rdf:XMLLiteral

Table 2.3 lists the set of datatype facets supported by OWL 2 Full. Section 4 of the OWL 2 DL Structural Specification describes the meaning of each facet, and to which datatypes it can be applied, respectively.

Editor's Note: The facet "langPattern" currently does not have a namespace. It is currently not clear which namespace this will be. It is also not clear, whether this facet will be defined by the OWL 2 DL Structural Specification or elsewhere, for example by a distinguished document describing the datatype rdf:text.
Table 2.3: Datatype Facets of OWL 2 Full
langPattern xsd:length xsd:maxExclusive xsd:maxInclusive xsd:maxLength xsd:minExclusive xsd:minInclusive xsd:minLength xsd:pattern

3 Interpretations

OWL 2 Full provides a vocabulary interpretation and vocabulary entailment (see Section 2.1 of the RDF Semantics) for the RDF vocabulary, the RDFS vocabulary, and the OWL 2 Full vocabulary.

From the RDF Semantics, let V be a set of URI references and literals containing the RDF and RDFS vocabulary, and let D be a datatype map according to Section 5.1 of the RDF Semantics. A D-interpretation of V is a tuple

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

IR is the domain of discourse or universe, i.e., a nonempty set that contains the denotations of URI references and literals in V. IP is a subset of IR, the properties of I. LV is a subset of IR that covers at least 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" means the powerset. IS is a mapping from URI references in V to their denotations in IR. IL is a mapping from typed literals in V to their denotations in LV. The set of classes IC is defined as

  IC = { x ∈ IR | 〈x,IS(rdfs:Class)〉 ∈ IEXT(IS(rdf:type)) }.

The mapping ICEXT from IC to P(IR) associates classes with their class extension, and is defined as

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

for c ∈ IC.

As detailed in the RDF Semantics, a D-interpretation has to meet additional semantic conditions, which constrain the set of RDF graphs that are true under this interpretation. An RDF graph G is said to be satisfied by a D-interpretation I, if I(G) = true.

Definition 3.1 (OWL 2 Full Datatype Map): Let D be a datatype map as defined in Section 5.1 of the RDF Semantics. D is an OWL 2 Full datatype map, if it contains at least all datatypes listed in Table 2.2.

Definition 3.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 2. An OWL 2 Full interpretation, I = 〈 IR, IP, IEXT, IS, IL, LV 〉, of V with respect to D, is a D-interpretation of V that meets all the semantic conditions given in Section 4.

Definition 3.3 (OWL 2 Full Consistency): Let K be a collection of RDF graphs, 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 2. K is OWL 2 Full consistent with respect to D iff there is some OWL 2 Full interpretation of V with respect to D that satisfies every RDF graph in K.

Definition 3.4 (OWL 2 Full Entailment): Let K and Q be collections of RDF graphs, 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 2. K OWL 2 Full entails Q with respect to D iff every OWL 2 Full interpretation of V with respect to D that satisfies every RDF graph in K also satisfies every RDF graph in Q.

4 Semantic Conditions

The semantic conditions presented here have to be regarded in conjunction with the semantic conditions given for Simple Entailment, RDF, RDFS and D-Entailment in the RDF Semantics.

The denotations of RDF triples, which occur in the semantic conditions, are closely related to triple sets given in the RDF Mapping.

Table 4.1 on "Basic Sets" enumerates the different parts of the OWL 2 Full universe, such as the sets of classes, properties, etc., which are referred to by many semantic conditions in this section. Table 4.2 lists several "Convenient Abbreviations" for sets that are often used within semantic conditions. Table 4.3 and Table 4.4 list basic semantic conditions for the classes and the properties of the OWL 2 Full vocabulary, which can be regarded as the OWL 2 Full "axiomatic triples" (this is further explained by the introduction of these tables). The remaining tables in this section specify the OWL 2 Full semantic conditions for the different language features of OWL 2.

Most semantic conditions are "iff" conditions, which exactly specify the semantics of the respective language feature. Some language features only have "if-then" conditions in order to avoid certain semantic paradoxes and other problems with the semantics. Several language features with "iff" conditions, namely Sub Property Chains in Table 4.10, N-ary Axioms in Table 4.12, and Negative Property Assertions in Table 4.16, have a multi-triple representation in RDF, where the different triples share a common "root node" x. In order to treat this specific syntactic aspect technically, the "iff" conditions of these language features are split into two "if-then" conditions, and the right-to-left "if" condition contains an additional premise of the form "∃x ∈ IR", which has the single purpose to provide the needed "root node" x.

Conventions used in this section:

Several conventions are used when presenting logic expressions in the below tables. Having a comma between two entries in a semantic condition, as in

 c ∈ IC , p ∈ IP

means a logical "and". If no scope is given for a variable x, as in "∀x:…" or in "{x|…}", then x is unconstrained, which means that x ∈ IR. An expression of the form

 l sequence of u1,…, un ∈ S

means that u1 ∈ S,… , un ∈ S, and that there exist x1 ∈ IR,…, xn ∈ IR, such that

   IS(l) ∈ ICEXT(IS(rdf:List)),
   IS(l) = IS(x1),
   〈x1,u1〉 ∈ IEXT(IS(rdf:first)), 〈x1,x2〉 ∈ IEXT(IS(rdf:rest)),
   …,
   〈xn,un〉 ∈ IEXT(IS(rdf:first)), 〈xn,IS(rdf:nil)〉 ∈ IEXT(IS(rdf:rest)).

The semantic conditions in the tables below sometimes do not explicitly list typing statements in their consequent that one would normally expect. This may be the case if these statements can already be deduced by means of the semantic conditions given in Table 4.3 and Table 4.4, occasionally in connection with Table 4.1. For example, the semantic condition for owl:allValuesFrom restrictions in Table 4.7 does not have the statement x ∈ ICEXT(IS(owl:Restriction)) on its right hand side. The reason is that this result can already be obtained from the third column of the entry for owl:allValuesFrom in Table 4.4, which determines that IEXT(IS(owl:allValuesFrom)) ⊆ ICEXT(IS(owl:Restriction)) × IC.

Table 4.1 presents basic sets used in OWL 2 Full, their relationship to other sets, and properties of their instances.

Table 4.1: Basic Sets
Name of
Set S		 Conditions on
Set S		 Conditions on
Instances x of S		 Explanation
IR S ≠ ∅ all individuals (or resources)
LV S ⊆ IR all data values
IX S ⊆ IR all ontologies
IC S ⊆ IR ICEXT(x) ⊆ IR all classes
IDC S ⊆ IC ICEXT(x) ⊆ LV all datatypes
IP S ⊆ IR IEXT(x) ⊆ IR × IR all (object) properties
IODP S ⊆ IP IEXT(x) ⊆ IR × LV all data properties
IOAP S ⊆ IP IEXT(x) ⊆ IR × IR all annotation properties
IOXP S ⊆ IP IEXT(x) ⊆ IX × IX all ontology properties

Table 4.2 provides abbreviations for additional sets, which are used throughout this document.

Table 4.2: Convenient Abbreviations
Name of Set S Explanation
INNI The subset of LV which consists of all non-negative integers.
IFA(d) The set of all facets allowed for datatype d.
IFAV(d,f) The set of all possible values for a given facet f and a datatype d.
IFAEXT(d,f,u) The subset of the class extension of datatype d that results from applying facet f with value u.
Review comment from Baojie 08:59, 10 September 2008 (UTC)
The definitions of IFAV and IFAEXT seem rather informal.

Table 4.3 lists the classes of OWL 2 Full vocabulary (and certain classes from RDF and RDFS), together with their relationship to other classes. Not included in this table are the different datatypes, as given in Table 2.2. For a datatype URI D, IS(D) ∈ IDC, and ICEXT(IS(D)) ⊆ LV.

Informative Note: The semantic conditions given here can be regarded as the OWL 2 Full "axiomatic triples" for classes: For each URI U occurring in the first column of the table, if the second column contains an entry "IS(U) ∈ S" for some set S, then this entry corresponds to some RDF triple of the form "U rdf:type C", where C is the URI of some class with ICEXT(IS(C)) = S. In this table, S will always be either the set IC of all classes, or a subset of IC. Hence, in a corresponding RDF triple the URI C will typically be one of "rdfs:Class" or "owl:Class" (S=IC in both cases), or "rdfs:Datatype" (S=IDC). Further, for each URI U in the first column, if the third column contains an entry "ICEXT(IS(U)) ⊆ S" ("ICEXT(IS(U)) = S") for some set S, then this entry corresponds to some RDF triple of the form "U rdfs:subClassOf C" ("U owl:equivalentClass C"), where C is the URI of some class with ICEXT(IS(C)) = S. Additionally, the conditions on the sets given in Table 4.1 have to be taken into account. In particular, if an entry of Table 4.1 states S1 ⊆ S2 for some sets S1 and S2, then this corresponds to some RDF triple C1 owl:subClassOf C2, where C1 and C2 are the URIs of some classes with ICEXT(IS(C1)) = S1 and ICEEXT(IS(C2)) = S2, respectively, according to Table 4.3. Note that some of the RDF triples received in this way already follow from the RDFS Semantics. These axiomatic triples are "simple" in the following sense: For every set S mentioned in the second and the third column of the table there exists a URI C of some class in the vocabularies for RDF, RDFS or those given in Section 2, for which S = ICEXT(IS(C)).

Table 4.3: Classes
Vocabulary URI U IS(U) ICEXT(IS(U))
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:SelfRestriction ∈ IC ⊆ ICEXT(IS(owl:Restriction))
owl:SymmetricProperty ∈ IC ⊆ IP
owl:Thing ∈ IC = IR
owl:TransitiveProperty ∈ IC ⊆ IP

Table 4.4 lists the properties of the OWL 2 Full vocabulary (and certain properties from RDF and RDFS), together with their domain and range. Not included in this table are the different datatype facets, as given in Table 2.3. For a facet URI F, IS(F) ∈ IP, and IEXT(IS(F)) ⊆ IR × LV.

Informative Note: The semantic conditions given here can be regarded as the OWL 2 Full "axiomatic triples" for properties: For each URI U occurring in the first column of the table, if the second column contains an entry "IS(U) ∈ S" for some set S, then this entry corresponds to some RDF triple of the form "U rdf:type C", where C is the URI of some class with ICEXT(IS(C)) = S. In this table, S will always be either the set IP of all properties, or a subset of IP. Hence, in a corresponding RDF triple the URI C will typically be one of "rdf:Property" or "owl:ObjectProperty" (S=IP in both cases), "owl:DatatypeProperty" (S=IODP), "owl:AnnotationProperty" (S=IOAP), or "owl:OntologyProperty" (S=IOXP). Further, for each URI U in the first column, if the third column contains an entry "IEXT(IS(U)) ⊆ S1 × S2" for some sets S1 and S2, then this entry corresponds to some RDF triples of the forms "U rdfs:domain C1" and "U rdfs:range C2", where C1 and C2 are the URIs of some classes with ICEXT(IS(C1)) = S1 and ICEEXT(IS(C2)) = S2, respectively. Exceptions are the semantic conditions "IEXT(IS(owl:TopObjectProperty)) = IR × IR" and "IEXT(IS(owl:TopDataProperty)) = IR × LV", for which there are no corresponding domain and range triples. These axiomatic triples are "simple" in the following sense: For every set S mentioned in the second column of the table, and as the left or right hand side of a Cartesian product in the third column of the table there exists a URI C of some class in the vocabularies for RDF, RDFS or those given in Section 2, for which S = ICEXT(IS(C)).

Table 4.4: Properties
Vocabulary URI U IS(U) IEXT(IS(U))
owl:allValuesFrom ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × IC
owl:assertionProperty ∈ IP ⊆ ICEXT(IS(owl:NegativePropertyAssertion)) × IP
owl:backwardCompatibleWith ∈ IOXP ⊆ IX × IX
owl:BottomDataProperty ∈ IODP = ∅
owl:BottomObjectProperty ∈ IP = ∅
owl:cardinality ∈ IP ⊆ ICEXT(IS(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 × ICEXT(IS(rdf:List))
owl:disjointWith ∈ IP ⊆ IC × IC
owl:distinctMembers ∈ IP ⊆ ICEXT(IS(owl:AllDifferent)) × ICEXT(IS(rdf:List))
owl:equivalentClass ∈ IP ⊆ IC × IC
owl:equivalentProperty ∈ IP ⊆ IP × IP
owl:hasKey ∈ IP ⊆ IC × ICEXT(IS(rdf:List))
owl:hasValue ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × IR
owl:imports ∈ IOXP ⊆ IX × IX
owl:incompatibleWith ∈ IOXP ⊆ IX × IX
owl:intersectionOf ∈ IP ⊆ IC × ICEXT(IS(rdf:List))
owl:inverseOf ∈ IP ⊆ IP × IP
rdfs:isDefinedBy ∈ IOAP ⊆ IR × IR
rdfs:label ∈ IOAP ⊆ IR × LV
owl:maxCardinality ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × INNI
owl:maxQualifiedCardinality ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × INNI
owl:members ∈ IP ⊆ IR × ICEXT(IS(rdf:List))
owl:minCardinality ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × INNI
owl:minQualifiedCardinality ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × INNI
owl:object ∈ IP ⊆ IR × IR
owl:onClass ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × IC
owl:onDataRange ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × IDC
owl:onDatatype ∈ IP ⊆ IDC × IDC
owl:oneOf ∈ IP ⊆ IC × ICEXT(IS(rdf:List))
owl:onProperty ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × IP
owl:onProperties ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × ICEXT(IS(rdf:List))
owl:predicate ∈ IP ⊆ IR × IP
owl:priorVersion ∈ IOXP ⊆ IX × IX
owl:propertyChain ∈ IP ⊆ IP × ICEXT(IS(rdf:List))
owl:propertyDisjointWith ∈ IP ⊆ IP × IP
owl:qualifiedCardinality ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × INNI
owl:sameAs ∈ IP ⊆ IR × IR
rdfs:seeAlso ∈ IOAP ⊆ IR × IR
owl:someValuesFrom ∈ IP ⊆ ICEXT(IS(owl:Restriction)) × IC
owl:sourceIndividual ∈ IP ⊆ ICEXT(IS(owl:NegativePropertyAssertion)) × IR
owl:subject ∈ IP ⊆ IR × IR
owl:targetIndividual ∈ IP ⊆ ICEXT(IS(owl:NegativePropertyAssertion)) × IR
owl:targetValue ∈ IP ⊆ ICEXT(IS(owl:NegativePropertyAssertion)) × LV
owl:TopDataProperty ∈ IODP = IR × LV
owl:TopObjectProperty ∈ IP = IR × IR
owl:unionOf ∈ IP ⊆ IC × ICEXT(IS(rdf:List))
owl:versionInfo ∈ IOAP ⊆ IR × IR
owl:withRestrictions ∈ IP ⊆ IDC × ICEXT(IS(rdf:List))

Table 4.5 lists the semantic conditions for boolean combinations, which exist for building class and datatype complements, intersections, and unions of classes.

Table 4.5: Boolean Combinations
〈c,d〉 ∈ IEXT(IS(owl:complementOf)) iff c, d ∈ IC
ICEXT(c) = IR \ ICEXT(d)
〈c,d〉 ∈ IEXT(IS(owl:datatypeComplementOf)) c, d ∈ IDC,
ICEXT(c) = LV \ ICEXT(d)
if l sequence of d1,…, dn ∈ IR then
〈c,l〉 ∈ IEXT(IS(owl:intersectionOf)) iff c, d1,…, dn ∈ IC,
ICEXT(c) = ICEXT(d1) ∩…∩ ICEXT(dn)
〈c,l〉 ∈ IEXT(IS(owl:unionOf)) c, d1,…, dn ∈ IC,
ICEXT(c) = ICEXT(d1) ∪…∪ ICEXT(dn)

Table 4.6 lists the semantic conditions for enumerations, i.e. classes, which have an explicitly defined, finite set of instances. Enumerations entirely consisting of data values are datatypes.

Table 4.6: Enumerations
if then
l sequence of u1,…, un ∈ LV, n ≥ 1,
〈c,l〉 ∈ IEXT(IS(owl:oneOf))		 c ∈ IDC
if l sequence of u1,…, un ∈ IR then
〈c,l〉 ∈ IEXT(IS(owl:oneOf)) iff c ∈ IC,
ICEXT(c) = { u1,…, un }

Table 4.7 lists the semantic conditions for restriction classes, which are self restrictions, value restrictions, and (qualified) cardinality restrictions.

Table 4.7: Restrictions
if then
x ∈ ICEXT(IS(owl:SelfRestriction)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | 〈y,y〉 ∈ IEXT(p)}
〈x,c〉 ∈ IEXT(IS(owl:allValuesFrom)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | ∀z : 〈y,z〉 ∈ IEXT(p) → z ∈ ICEXT(c)}
l sequence of p1,…, pn ∈ IODP,
〈x,c〉 ∈ IEXT(IS(owl:allValuesFrom)),
〈x,l〉 ∈ IEXT(IS(owl:onProperties))		 ICEXT(x) = {y | ∀z1,…,zn : 〈y,z1〉 ∈ IEXT(p1) ∧…∧ 〈y,zn〉 ∈ IEXT(pn) → 〈z1,…,zn〉 ∈ ICEXT(c)}
〈x,c〉 ∈ IEXT(IS(owl:someValuesFrom)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | ∃z : 〈y,z〉 ∈ IEXT(p) ∧ z ∈ ICEXT(c)}
l sequence of p1,…, pn ∈ IODP,
〈x,c〉 ∈ IEXT(IS(owl:someValuesFrom)),
〈x,l〉 ∈ IEXT(IS(owl:onProperties))		 ICEXT(x) = {y | ∃z1,…,zn : 〈y,z1〉 ∈ IEXT(p1) ∧…∧ 〈y,zn〉 ∈ IEXT(pn) ∧ 〈z1,…,zn〉 ∈ ICEXT(c)}
〈x,u〉 ∈ IEXT(IS(owl:hasValue)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | 〈y,u〉 ∈ IEXT(p)}
〈x,n〉 ∈ IEXT(IS(owl:cardinality)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | #{z|〈y,z〉 ∈ IEXT(p)} = n}
〈x,n〉 ∈ IEXT(IS(owl:minCardinality)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | #{z|〈y,z〉 ∈ IEXT(p)} ≥ n}
〈x,n〉 ∈ IEXT(IS(owl:maxCardinality)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | #{z|〈y,z〉 ∈ IEXT(p)} ≤ n}
〈x,n〉 ∈ IEXT(IS(owl:qualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onClass)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | #{z|〈y,z〉 ∈ IEXT(p) ∧ z ∈ ICEXT(c)} = n}
〈x,n〉 ∈ IEXT(IS(owl:qualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onDataRange)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 p ∈ IODP,
ICEXT(x) = {y | #{z ∈ LV|〈y,z〉 ∈ IEXT(p) ∧ z ∈ ICEXT(c)} = n}
〈x,n〉 ∈ IEXT(IS(owl:minQualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onClass)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | #{z|〈y,z〉 ∈ IEXT(p) ∧ z ∈ ICEXT(c)} ≥ n}
〈x,n〉 ∈ IEXT(IS(owl:minQualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onDataRange)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 p ∈ IODP,
ICEXT(x) = {y | #{z ∈ LV|〈y,z〉 ∈ IEXT(p) ∧ z ∈ ICEXT(c)} ≥ n}
〈x,n〉 ∈ IEXT(IS(owl:maxQualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onClass)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 ICEXT(x) = {y | #{z |〈y,z〉 ∈ IEXT(p) ∧ z ∈ ICEXT(c)} ≤ n}
〈x,n〉 ∈ IEXT(IS(owl:maxQualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onDataRange)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))		 p ∈ IODP,
ICEXT(x) = {y | #{z ∈ LV|〈y,z〉 ∈ IEXT(p) ∧ z ∈ ICEXT(c)} ≤ n}

Table 4.8 lists the semantic condition for datatype restrictions, which are specified by a set of facets with their values applied to a datatype. Note that if no facet is applied to a given datatype, then the resulting datatype will be equivalent to the original datatype. Note further that the semantic condition is specified in a way that applying a facet to a datatype, for which it is not defined, or adding an illegal value to a facet/datatype combination will lead to an unsatisfiable ontology.

Table 4.8: Datatype Restrictions
if then
l sequence of y1,…, yn ∈ IR,
f1,…, fn ∈ IP,
〈c,d〉 ∈ IEXT(IS(owl:onDatatype)),
〈c,l〉 ∈ IEXT(IS(owl:withRestrictions)),
〈y1,u1〉 ∈ IEXT(f1),
…,
〈yn,un〉 ∈ IEXT(fn)		 c, d ∈ IDC,
fi ∈ IFA(d) for 1≤i≤n,
ui ∈ IFAV(d,fi) for 1≤i≤n,
ICEXT(c) = ICEXT(d) ∩ IFAEXT(d,f1,u1) ∩…∩ IFAEXT(d,fn,un)

Table 4.9 extends the semantic conditions for the RDFS vocabulary. The original semantics for RDFS, as specified in the RDF Semantics, only provide "if-then" semantic conditions, while OWL 2 Full specifies stronger "iff" semantic conditions. Note that only the additional semantic conditions are given here and that the other conditions on the RDF and RDFS vocabulary are retained.

Table 4.9: Extended Conditions for the RDFS Vocabulary
〈c,d〉 ∈ IEXT(IS(rdfs:subClassOf)) iff c, d ∈ IC,
ICEXT(c) ⊆ ICEXT(d)
〈p,q〉 ∈ IEXT(IS(rdfs:subPropertyOf)) p, q ∈ IP,
IEXT(p) ⊆ IEXT(q)
〈p,c〉 ∈ IEXT(IS(rdfs:domain)) p ∈ IP, c ∈ IC,
∀x,y : 〈x,y〉 ∈ IEXT(p) → x ∈ ICEXT(c)
〈p,c〉 ∈ IEXT(IS(rdfs:range)) p ∈ IP, c ∈ IC,
∀x,y : 〈x,y〉 ∈ IEXT(p) → y ∈ ICEXT(c)

Table 4.10 lists the semantic conditions for sub property chains.

Table 4.10: Sub Property Chains
if then
l sequence of p1,…, pn ∈ IR,
〈x,q〉 ∈ IEXT(IS(rdfs:subPropertyOf)),
〈x,l〉 ∈ IEXT(IS(owl:propertyChain))		 p1,…, pn ∈ IP,
∀y0,…,yn : 〈y0,y1〉 ∈ IEXT(p1) ∧…∧ 〈yn-1,yn〉 ∈ IEXT(pn) → 〈y0,yn〉 ∈ IEXT(q)
if then exists x ∈ IR
l sequence of p1,…, pn ∈ IP,
∀y0,…,yn : 〈y0,y1〉 ∈ IEXT(p1) ∧…∧ 〈yn-1,yn〉 ∈ IEXT(pn) → 〈y0,yn〉 ∈ IEXT(q)		 〈x,q〉 ∈ IEXT(IS(rdfs:subPropertyOf)),
〈x,l〉 ∈ IEXT(IS(owl:propertyChain))

Table 4.11 lists the semantic conditions for equal and different individuals, equivalent and disjoint classes, and equivalent and disjoint properties. Also treated here are axioms to specify disjoint unions.

Table 4.11: Equivalence and Disjointness
〈u,w〉 ∈ IEXT(IS(owl:sameAs)) iff u = w
〈u,w〉 ∈ IEXT(IS(owl:differentFrom)) u ≠ w
〈c,d〉 ∈ IEXT(IS(owl:equivalentClass)) c, d ∈ IC,
ICEXT(c) = ICEXT(d)
〈c,d〉 ∈ IEXT(IS(owl:disjointWith)) c, d ∈ IC,
ICEXT(c) ∩ ICEXT(d) = ∅
〈p,q〉 ∈ IEXT(IS(owl:equivalentProperty)) p, q ∈ IP,
IEXT(p) = IEXT(q)
〈p,q〉 ∈ IEXT(IS(owl:propertyDisjointWith)) p, q ∈ IP,
IEXT(p) ∩ IEXT(q) = ∅
if l sequence of d1,…, dn ∈ IR then
〈c,l〉 ∈ IEXT(IS(owl:disjointUnionOf)) iff c, d1,…, dn ∈ IC,
ICEXT(c) = ICEXT(d1) ∪…∪ ICEXT(dn),
ICEXT(di) ∩ ICEXT(dk) = ∅ for 1 ≤ i ≠ k ≤ n

Table 4.12 lists the semantic conditions for the n-ary versions of the axioms for different individuals, disjoint classes, and disjoint properties.

Table 4.12: N-ary Axioms
if then
l sequence of u1,…, un ∈ IR,
x ∈ ICEXT(IS(owl:AllDifferent)),
〈x,l〉 ∈ IEXT(IS(owl:distinctMembers))		 ui ≠ uk for 1 ≤ i ≠ k ≤ n
l sequence of u1,…, un ∈ IR,
x ∈ ICEXT(IS(owl:AllDifferent)),
〈x,l〉 ∈ IEXT(IS(owl:members))		 ui ≠ uk for 1 ≤ i ≠ k ≤ n
l sequence of c1,…, cn ∈ IR,
x ∈ ICEXT(IS(owl:AllDisjointClasses)),
〈x,l〉 ∈ IEXT(IS(owl:members))		 c1,…, cn ∈ IC,
ICEXT(ci) ∩ ICEXT(ck) = ∅ for 1 ≤ i ≠ k ≤ n
l sequence of p1,…, pn ∈ IR,
x ∈ ICEXT(IS(owl:AllDisjointProperties)),
〈x,l〉 ∈ IEXT(IS(owl:members))		 p1,…, pn ∈ IP,
IEXT(pi) ∩ IEXT(pk) = ∅ for 1 ≤ i ≠ k ≤ n
if then exists x ∈ IR
l sequence of u1,…, un ∈ IR,
ui ≠ uk for 1 ≤ i ≠ k ≤ n		 x ∈ ICEXT(IS(owl:AllDifferent)),
〈x,l〉 ∈ IEXT(IS(owl:distinctMembers))
l sequence of u1,…, un ∈ IR,
ui ≠ uk for 1 ≤ i ≠ k ≤ n		 x ∈ ICEXT(IS(owl:AllDifferent)),
〈x,l〉 ∈ IEXT(IS(owl:members))
l sequence of c1,…, cn ∈ IC,
ICEXT(ci) ∩ ICEXT(ck) = ∅ for 1 ≤ i ≠ k ≤ n		 x ∈ ICEXT(IS(owl:AllDisjointClasses)),
〈x,l〉 ∈ IEXT(IS(owl:members))
l sequence of p1,…, pn ∈ IP,
IEXT(pi) ∩ IEXT(pk) = ∅ for 1 ≤ i ≠ k ≤ n		 x ∈ ICEXT(IS(owl:AllDisjointProperties)),
〈x,l〉 ∈ IEXT(IS(owl:members))

Table 4.13 lists the semantic condition for inverse property axioms.

Table 4.13: Inverse Properties
〈p,q〉 ∈ IEXT(IS(owl:inverseOf)) iff p, q ∈ IP,
IEXT(p) = { 〈x,y〉 | 〈y,x〉 ∈ IEXT(q) }

Table 4.14 lists the semantic conditions for property characteristics, i.e. functionality and inverse functionality, reflexivity and irreflexivity, symmetry and asymmetry, and transitivity of properties.

Table 4.14: Property Characteristics
p ∈ ICEXT(IS(owl:FunctionalProperty)) iff p ∈ IP,
∀x,y,z : 〈x,y〉, 〈x,z〉 ∈ IEXT(p) → y = z
p ∈ ICEXT(IS(owl:InverseFunctionalProperty)) p ∈ IP,
∀x,y,z : 〈y,x〉, 〈z,x〉 ∈ IEXT(p) → y = z
p ∈ ICEXT(IS(owl:ReflexiveProperty)) p ∈ IP,
∀x : 〈x,x〉 ∈ IEXT(p)
p ∈ ICEXT(IS(owl:IrreflexiveProperty)) p ∈ IP,
∀x : 〈x,x〉 ∉ IEXT(p)
p ∈ ICEXT(IS(owl:SymmetricProperty)) p ∈ IP,
∀x,y : 〈x,y〉 ∈ IEXT(p) → 〈y,x〉 ∈ IEXT(p)
p ∈ ICEXT(IS(owl:AsymmetricProperty)) p ∈ IP,
∀x,y : 〈x,y〉 ∈ IEXT(p) → 〈y,x〉 ∉ IEXT(p)
p ∈ ICEXT(IS(owl:TransitiveProperty)) p ∈ IP,
∀x,y,z : 〈x,y〉, 〈y,z〉 ∈ IEXT(p) → 〈x,z〉 ∈ IEXT(p)

Table 4.15 lists the semantic condition for Keys.

Table 4.15: Keys
if l sequence of p1,…, pn ∈ IR then
〈c,l〉 ∈ IEXT(IS(owl:hasKey)) iff c ∈ IC,
p1,…, pn ∈ IP,
∀x,y,z1,…,zn :
 x, y ∈ ICEXT(c),
 〈x,zi〉, 〈y,zi〉 ∈ IEXT(pi), 1 ≤ i ≤ n
 → x = y

Table 4.16 lists the semantic conditions for negative property assertions.

Table 4.16: Negative Property Assertions
if then
〈x,u〉 ∈ IEXT(IS(owl:sourceIndividual)),
〈x,p〉 ∈ IEXT(IS(owl:assertionProperty)),
〈x,w〉 ∈ IEXT(IS(owl:targetIndividual))		 x ∈ ICEXT(IS(owl:NegativePropertyAssertion)),
〈u,w〉 ∉ IEXT(p)
〈x,u〉 ∈ IEXT(IS(owl:sourceIndividual)),
〈x,p〉 ∈ IEXT(IS(owl:assertionProperty)),
〈x,w〉 ∈ IEXT(IS(owl:targetValue))		 x ∈ ICEXT(IS(owl:NegativePropertyAssertion)),
p ∈ IODP,
〈u,w〉 ∉ IEXT(p)
if then exists x ∈ IR
u ∈ IR,
p ∈ IP,
w ∈ IR,
〈u,w〉 ∉ IEXT(p)		 〈x,u〉 ∈ IEXT(IS(owl:sourceIndividual)),
〈x,p〉 ∈ IEXT(IS(owl:assertionProperty)),
〈x,w〉 ∈ IEXT(IS(owl:targetIndividual))
u ∈ IR,
p ∈ IODP,
w ∈ LV,
〈u,w〉 ∉ IEXT(p)		 〈x,u〉 ∈ IEXT(IS(owl:sourceIndividual)),
〈x,p〉 ∈ IEXT(IS(owl:assertionProperty)),
〈x,w〉 ∈ IEXT(IS(owl:targetValue))

Table 4.17 lists the semantic conditions for the OWL vocabulary used for some axiom annotations and for annotations on annotations. Both these kinds of annotations employ a reified version of a triple representing either the annotated axiom or the annotated annotation. The semantic conditions below recover the triple itself from the reified version.

Editor's Note: Open Question: Table 4.17 lists two semantic conditions, which only differ in having different typing triples for owl:Axiom and owl:Annotation. Should we change this into a single semantic condition without the typing triples, i.e. where the LHS of the semantic condition only consists of the three triples for owl:subject, owl:predicate, and owl:object?

Jie Bao answers as a revision comment: "I support your Editor's Note before current Table 4.17, i.e., removing the typing triples. This will allow annotations in OWL full on any triples. So far I don't see a problem without the typing triples in inference."

Table 4.17: Reified Axioms and Annotations
if then
x in ICEXT(IS(owl:Axiom)),
〈x,u〉 ∈ IEXT(IS(owl:subject)),
〈x,p〉 ∈ IEXT(IS(owl:predicate)),
〈x,w〉 ∈ IEXT(IS(owl:object))		 〈u,w〉 ∈ IEXT(p)
x in ICEXT(IS(owl:Annotation)),
〈x,u〉 ∈ IEXT(IS(owl:subject)),
〈x,p〉 ∈ IEXT(IS(owl:predicate)),
〈x,w〉 ∈ IEXT(IS(owl:object))		 〈u,w〉 ∈ IEXT(p)

5 Ontologies

Editor's Note: Open Question: Should something be said about Ontology headers and versioning? This does not have a special semantics, and so its treatment isn't really needed technically. But maybe they should be treated for completeness?

Every well-formed RDF graph is a syntactically valid OWL 2 Full ontology, and its semantic meaning is given by the OWL 2 Full semantics.

If an OWL 2 Full ontology imports other OWL 2 Full ontologies, then one should regard the semantic meaning of the whole imports closure (see Definition 5.1) of that ontology. Note that Section 3 defines the terms "OWL 2 Full Consistency" and "OWL 2 Full Entailment" for collections of RDF graphs.

Definition 5.1 (Import Closure): Let K be a collection of RDF graphs. K is imports closed iff for every triple in any element of K of the form x owl:imports u then K contains a graph that is referred to by u. The imports closure of a collection of RDF graphs is the smallest imports closed collection of RDF graphs containing the graphs.

6 Relationship to OWL 2 DL

This section is concerned with a strong relationship that holds between the semantics of OWL 2 Full and OWL 2 DL.

One design goal of OWL 2 has been that OWL 2 Full should reflect every logical consequence of OWL 2 DL, as long as this consequence and all its premises can be represented as valid OWL 2 DL ontologies in RDF graph form. However, a fundamental semantic difference exists between OWL 2 DL and OWL 2 Full, which complicates a comparison of the semantic expressiveness of the two languages. OWL 2 DL treats classes as sets, i.e. subsets of the universe, while classes in OWL 2 Full are individuals, which have such a set associated as their class extension. Hence, under OWL 2 Full semantics, all classes are instances of the universe, but this cannot generally be assumed under OWL 2 DL semantics. An analog difference exists for properties.

An effect of this difference is that certain logical conclusions of OWL 2 DL do not become "visible" under the OWL 2 Full semantics, although they are reflected by OWL 2 Full at a set theoretical level. For example, under OWL 2 DL semantics, the RDF graph

 G1 := {
   ex:C rdf:type owl:Class .
   ex:D rdf:type owl:Class .
   ex:C rdfs:subClassOf ex:D .
 }

entails the RDF graph

 G2 := {
   ex:C rdf:type owl:Class .
   ex:D rdf:type owl:Class .
   _:x owl:intersectionOf (SEQ ex:C ex:D) .
   _:x rdfs:subClassOf ex:D .
 }.

OWL 2 Full, on the other hand, interprets G1 in a way such that the set theoretical relationship

 ICEXT(IS(ex:C)) ∩ ICEXT(IS(ex:D)) ⊆ ICEXT(IS(ex:D))

can be concluded. But since OWL 2 Full distinguishes between classes and their class extensions, G2 is not entailed, unless there exists some additional "helper" individual, which has the set

 ICEXT(IS(ex:C)) ∩ ICEXT(IS(ex:D))

as its class extension. Whether such a helper individual exists or not has no effect on the answer to the question, whether the basic logical conclusion that exists at the set theoretical level holds or not. The individual is, however needed, to represent this conclusion in the particular form given by G2.

The following subsection introduces a set of "comprehension principles", which have the purpose to provide the missing "helper" individuals. These comprehension principles are not part of the set of semantic conditions given in Section 4, and therefore do not need to be met by an OWL 2 Full interpretation as defined in Section 3. They are, however, needed for the correspondence theorem, stated in the second subsection, to hold, since the correspondence theorem compares OWL 2 Full and OWL 2 DL based on entailments.

6.1 Comprehension Principles

Table 6.1 lists the comprehension principle for lists, which provides the existence of RDF lists for each finite combination of individuals.

Table 6.1: Comprehension Principle for Lists
if then exists x1,…, xn ∈ IR
u1,…, un ∈ IR 〈x1,u1〉 ∈ IEXT(IS(rdf:first)), 〈x1,x2〉 ∈ IEXT(IS(rdf:rest)),
…,
〈xn,un〉 ∈ IEXT(IS(rdf:first)), 〈xn,IS(rdf:nil)〉 ∈ IEXT(IS(rdf:rest))

Table 6.2 lists the comprehension principles for boolean combinations, which provide the existence of classes representing the complement of each class, and the datatype complement of each datatype, and the union and intersection of each finite set of classes.

Table 6.2: Comprehension Principles for Boolean Combinations
if then exists x ∈ IR
c ∈ IC 〈x,c〉 ∈ IEXT(IS(owl:complementOf))
c ∈ IDC 〈x,c〉 ∈ IEXT(IS(owl:datatypeComplementOf))
l sequence of c1,…, cn ∈ IC 〈x,l〉 ∈ IEXT(IS(owl:unionOf))
l sequence of c1,…, cn ∈ IC 〈x,l〉 ∈ IEXT(IS(owl:intersectionOf))

Table 6.3 lists the comprehension principle for enumerations, which provides the existence of classes representing each finite set of individuals.

Table 6.3: Comprehension Principle for Enumerations
if then exists x ∈ IR
l sequence of u1,…, un ∈ IR 〈x,l〉 ∈ IEXT(IS(owl:oneOf))

Table 6.4 lists the comprehension principles for restrictions, which provide the existence of self restrictions, value restrictions, cardinality restrictions, and qualified cardinality restrictions for each property, class and individual for which such a restriction is meaningful.

Table 6.4: Comprehension Principles for Restrictions
if then exists x ∈ IR
p ∈ IP x ∈ ICEXT(IS(owl:SelfRestriction)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
c ∈ IC,
p ∈ IP		 〈x,c〉 ∈ IEXT(IS(owl:allValuesFrom)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
c ∈ IDC,
l sequence of p1,…, pn ∈ IODP		 〈x,c〉 ∈ IEXT(IS(owl:allValuesFrom)),
〈x,l〉 ∈ IEXT(IS(owl:onProperties))
c ∈ IC,
p ∈ IP		 〈x,c〉 ∈ IEXT(IS(owl:someValuesFrom)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
c ∈ IDC,
l sequence of p1,…, pn ∈ IODP		 〈x,c〉 ∈ IEXT(IS(owl:someValuesFrom)),
〈x,l〉 ∈ IEXT(IS(owl:onProperties))
u ∈ IR,
p ∈ IP		 〈x,u〉 ∈ IEXT(IS(owl:hasValue)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
n ∈ INNI,
p ∈ IP		 〈x,n〉 ∈ IEXT(IS(owl:cardinality)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
n ∈ INNI,
p ∈ IP		 〈x,n〉 ∈ IEXT(IS(owl:minCardinality)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
n ∈ INNI,
p ∈ IP		 〈x,n〉 ∈ IEXT(IS(owl:maxCardinality)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
n ∈ INNI,
c ∈ IC,
p ∈ IP		 〈x,n〉 ∈ IEXT(IS(owl:qualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onClass)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
n ∈ INNI,
c ∈ IDC,
p ∈ IODP		 〈x,n〉 ∈ IEXT(IS(owl:qualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onDataRange)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
n ∈ INNI,
c ∈ IC,
p ∈ IP		 〈x,n〉 ∈ IEXT(IS(owl:minQualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onClass)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
n ∈ INNI,
c ∈ IDC,
p ∈ IODP		 〈x,n〉 ∈ IEXT(IS(owl:minQualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onDataRange)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
n ∈ INNI,
c ∈ IC,
p ∈ IP		 〈x,n〉 ∈ IEXT(IS(owl:maxQualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onClass)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))
n ∈ INNI,
c ∈ IDC,
p ∈ IODP		 〈x,n〉 ∈ IEXT(IS(owl:maxQualifiedCardinality)),
〈x,c〉 ∈ IEXT(IS(owl:onDataRange)),
〈x,p〉 ∈ IEXT(IS(owl:onProperty))

Table 6.5 lists the comprehension principle for datatype restrictions, which provides the existence of restrictions for each datatype, and for each combination of facets and values for which such a restriction is meaningful.

Table 6.5: Comprehension Principle for Datatype Restrictions
if then exists x ∈ IR, l sequence of y1,…,yn ∈ IR
c ∈ IDC,
f1,…,fn facets,
u1,…,un ∈ LV		 〈x,c〉 ∈ IEXT(IS(owl:onDatatype)),
〈x,l〉 ∈ IEXT(IS(owl:withRestrictions)),
〈y1,u1〉 ∈ IEXT(f1),
…,
〈yn,un〉 ∈ IEXT(fn)

6.2 Correspondence Theorem

Theorem 6.1 (Correspondence Theorem): Let D be an OWL 2 Full datatype map, and let K and Q be collections of valid OWL 2 DL ontologies in RDF graph form that are imports closed, and without annotations occurring in Q. Let F(K) and F(Q) be the collections of OWL 2 DL ontologies in Functional Syntax which result from applying the Reverse RDF Mapping to K and Q, respectively. If F(K) OWL 2 DL entails F(Q) with respect to D, then K entails Q with respect to the OWL 2 Full semantics extended by the comprehension principles, and with respect to D.

Proof.

Editor's Note: TODO: The proof still needs to be constructed.

7 Differences to OWL Full

This section lists significant differences between OWL 2 Full and the original OWL Full.

Editor's Note: This section needs to be written after the document is considered to be finished (before Last Call). The following topics are suggested:

8 References

[RDF Semantics]
RDF Semantics. Patrick Hayes, Editor. W3C Recommendation 10 February 2004.
[OWL Semantics and Abstract Syntax]
OWL Web Ontology Language: Semantics and Abstract Syntax. Peter F. Patel-Schneider, Patrick Hayes, and Ian Horrocks, Editors. W3C Recommendation, 10 February 2004.
[OWL 2 RDF Mapping]
OWL 2 Web Ontology Language:Mapping to RDF Graphs Bernardo Cuenca Grau, Boris Motik, Peter F. Patel-Schneider. W3C Editor's Draft, 22 September 2008, http://www.w3.org/2007/OWL/draft/ED-owl2-mapping-to-rdf-20080922/. Latest version available at http://www.w3.org/2007/OWL/draft/owl2-mapping-to-rdf/.
[OWL 2 DL Semantics]
OWL 2 Web Ontology Language:Model-Theoretic Semantics Bernardo Cuenca Grau, Boris Motik. W3C Editor's Draft, 22 September 2008, http://www.w3.org/2007/OWL/draft/ED-owl2-semantics-20080922/. Latest version available at http://www.w3.org/2007/OWL/draft/owl2-semantics/.
[OWL 2 DL Specification]
OWL 2 Web Ontology Language:Structural Specification and Functional-Style Syntax Boris Motik, Peter F. Patel-Schneider, Ian Horrocks. W3C Editor's Draft, 22 September 2008, http://www.w3.org/2007/OWL/draft/ED-owl2-syntax-20080922/. Latest version available at http://www.w3.org/2007/OWL/draft/owl2-syntax/.
[OWL 2 Conformance and Testcases]
OWL 2 Web Ontology Language:Conformance and Test Cases Michael Smith, Ian Horrocks. W3C Editor's Draft, 22 September 2008, http://www.w3.org/2007/OWL/draft/ED-owl2-test-20080922/. Latest version available at http://www.w3.org/2007/OWL/draft/owl2-test/.
[RFC 2119]
RFC 2119: Key words for use in RFCs to Indicate Requirement Levels. Network Working Group, S. Bradner. Internet Best Current Practice, March 1997.