The normative form of this document is a compound HTML document.
Copyright © 2003 W3C^{®} (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark, document use and software licensing rules apply.
This description of OWL, the Web Ontology Language being designed by the W3C Web Ontology Working Group, contains a highlevel abstract syntax for both OWL DL and OWL Lite, sublanguages of OWL. A modeltheoretic semantics is given to provide a formal meaning for OWL ontologies written in this abstract syntax. A modeltheoretic semantics in the form of an extension to the RDF semantics is also given to provide a formal meaning for OWL ontologies as RDF graphs (OWL Full). A mapping from the abstract syntax to RDF graphs is given and the two model theories are shown to have the same consequences on OWL ontologies that can be written in the abstract syntax.
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 reporst index at http://www.w3.org/TR/.
This is a W3C Candidate Recommendation from the W3C Web Ontology Working Group produced 18 August 2003 as part of the W3C Semantic Web Activity (Activity Statement). It incorporates decisions made by the Working Group in designing the OWL Web Ontology Language. This is a W3C Candidate Recommendation produced so that implementors can have a stable target for implementation. Changes may be made to this document as the result of implementation experience. A list of current W3C Recommendations and other technical documents can be found at http://www.w3.org/TR/.
This document depends on postlastcall changes made to the RDF specification by the RDF Core Working Group. This document is current with respect to the changes made up to 7 August 2003. Further changes to the RDF specification may require changes to this document. No such changes are expected, however.
There are no patent disclosures related to this work at the time of this writing.
Comments on this document are invited and should be sent to the public mailing list publicwebontcomments@w3.org. An archive of comments is available at http://lists.w3.org/Archives/Public/publicwebontcomments/ .
This document is one part of the specification of OWL, the Web Ontology Language. The OWL Overview [OWL Overview] describes each of the different documents in the specification and how they fit together.
This document contains several interrelated normative specifications of the several styles of OWL, the Web Ontology Language being produced by the W3C Web Ontology Working Group (WebOnt). First, Section 2 contains a highlevel, abstract syntax for both OWL Lite, a subset of OWL, and OWL DL, a fuller style of using OWL but one that still places some limitations on how OWL ontologies are constructed. Eliminating these limitations results in the full OWL language, called OWL Full, which has the same syntax as RDF. The normative exchange syntax for OWL is RDF/XML [RDF Syntax]; the OWL Reference document [OWL Reference] shows how the RDF syntax is used in OWL. A mapping from the OWL abstract syntax to RDF graphs [RDF Concepts] is, however, provided in Section 4.
This document contains two formal semantics for OWL. One of these semantics, defined in Section 3, is a direct, standard modeltheoretic semantics for OWL ontologies written in the abstract syntax. The other, defined in Section 5, is a vocabulary extension of the RDF semantics [RDF MT] that provides semantics for OWL ontologies in the form of RDF graphs. Two versions of this second semantics are provided, one that corresponds more closely to the direct semantics (and is thus a semantics for OWL DL) and one that can be used in cases where classes need to be treated as individuals or other situations that cannot be handled in the abstract syntax (and is thus a semantics for OWL Full). These two versions are actually very close, only differing in how they divide up the domain of discourse.
Appendix A contains a proof that the direct and RDFScompatible semantics have the same consequences on OWL ontologies that correspond to abstract OWL ontologies that separate OWL individuals, OWL classes, OWL properties, and the RDF, RDFS, and OWL structural vocabulary. Appendix A also contains the sketch of a proof that the entailments in the RDFScompatible semantics for OWL Full include all the entailments in the RDFScompatible semantics for OWL DL. Finally a few examples of the various concepts defined in the document are presented in Appendix B.
This document is designed to be read by those interested in the technical details of OWL. It is not particularly intended for the casual reader, who should probably first read the OWL Guide [OWL Guide]. Developers of parsers and other syntactic tools for OWL will be particularly interested in Sections 2 and 4. Developers of reasoners and other semantic tools for OWL will be particulary interested in Sections 3 and 5.
The syntax for OWL in this section abstracts from exchange syntax for OWL and thus facilitates access to and evaluation of the language. This particular syntax has a framelike style, where a collection of information about a class or property is given in one large syntactic construct, instead of being divided into a number of atomic chunks (as in most Description Logics) or even being divided into even more triples (as when writing OWL as RDF graphs [RDF Concepts]). The syntax used here is rather informal, even for an abstract syntax  in general the arguments of a construct should be considered to be unordered wherever the order would not affect the meaning of the construct.
The abstract syntax is specified here by means of a version of Extended BNF, very similar to the EBNF notation used for XML [XML]. Terminals are quoted; nonterminals are bold and not quoted. Alternatives are either separated by vertical bars () or are given in different productions. Components that can occur at most once are enclosed in square brackets ([…]); components that can occur any number of times (including zero) are enclosed in braces ({…}). Whitespace is ignored in the productions here.
Names in the abstract syntax are RDF URI references, [RDF Concepts]. Often these names will be abbreviated into qualified names, using one of the following namespace names:
Namespace name  Namespace 

rdf  http://www.w3.org/1999/02/22rdfsyntaxns# 
rdfs  http://www.w3.org/2000/01/rdfschema# 
xsd  http://www.w3.org/2001/XMLSchema# 
owl  http://www.w3.org/2002/07/owl# 
The meaning of each construct in the abstract syntax is informally described when it is introduced. The formal meaning of these constructs is given in Section 3 via a modeltheoretic semantics.
While it is widely appreciated that all of the features in expressive languages such as OWL are important to some users, it is also understood that such languages may be daunting to some groups who are trying to support a tool suite for the entire language. In order to provide a simpler target for implementation, a smaller language has been defined, called OWL Lite [OWL Overview]. This smaller language was designed to provide functionality that is important in order to support Web applications, but that is missing in RDF Schema [RDF Schema]. (Note, however, that both OWL DL and OWL Lite do not provide all of the feature of RDF Schema.) The abstract syntax is expressed both for this smaller language, called the OWL Lite abstract syntax here, and also for a fuller style of OWL, called the OWL DL abstract syntax here.
The abstract syntax here is less general than the exchange syntax for OWL. In particular, it does not permit the construction of selfreferential syntactic constructs. It is also intended for use in cases where classes, properties, and individuals form disjoint collections. These are roughly the limitations required to make reasoning in OWL be decidable, and thus this abstract syntax should be thought of a syntax for OWL DL.
NOTE: OWL Lite and OWL DL closely correspond to the description logics known as SHIF(D) and SHION(D), with some limitation on how datatypes are treated. The abstract syntax for OWL Lite doesn't contain many of the common explicit constructors associated with SHIF(D), but the expressivity remains.
An OWL ontology in the abstract syntax contains a sequence of annotations, axioms, and facts. OWL ontologies can have a name. Annotations on OWL ontologies can be used to record authorship and other information associated with an ontology, including imports references to other ontologies. The main content of an OWL ontology is carried in its axioms and facts, which provide information about classes, properties, and individuals in the ontology.
ontology ::= 'Ontology(' [ ontologyID ] { directive } ')' directive ::= 'Annotation(' ontologyPropertyID ontologyID ')'  'Annotation(' annotationPropertyID URIreference ')'  'Annotation(' annotationPropertyID dataLiteral ')'  'Annotation(' annotationPropertyID individual ')'  axiom  fact
Names of ontologies are used in the abstract syntax to carry the meaning associated with publishing an ontology on the Web. Names of ontologies are used in the abstract syntax to carry the meaning associated with publishing an ontology on the Web. It is thus intended that the name of an ontology in the abstract syntax would be the URI where it could be found, although this is not part of the formal meaning of OWL. Imports annotations, in effect, are directives to retrieve a Web document and treat it as an OWL ontology. However, most aspects of the Web, including missing, unavailable, and timevarying documents, reside outside the OWL specification; all that is carried here is that a URI can be ``dereferenced'' into an OWL ontology. In several places in this document, therefore, idealizations of this operational meaning for imports are used.
Ontologies incorporate information about classes, properties, and individuals, each of which can have an identifier which is a URI reference. Some of these identifiers need to be given axioms, as detailed in Section 2.3.
datatypeID ::= URIreference classID ::= URIreference individualID ::= URIreference ontologyID ::= URIreference datavaluedPropertyID ::= URIreference individualvaluedPropertyID ::= URIreference annotationPropertyID ::= URIreference ontologyPropertyID ::= URIreference
A URI reference cannot be both a datatypeID and a classID in an ontology. A URI reference also cannot be more than one of an datavaluedPropertyID, an individualvaluedPropertyID, an annotationPropertyID, or an ontologyPropertyID in an ontology. However, a URI reference can be the identifier of a class or datatype as well as the identifier of a property as well as the identifier of an individual, although the ontology cannot then be translated into an OWL DL RDF graph.
In OWL a datatype denotes the set of data values that is the value space for the datatype. Classes denote sets of individuals. Properties relate individuals to other information, and are divided into four disjoint groups, datavalued properties, individualvalued properties, annotation properties, and ontology properties. Datavalued properties relate individuals to data values. Individualvalued properties relate individuals to other individuals. Annotation properties are used to place annotations on individuals, class names, property names, and ontology names. Ontology properties relate ontologies to other ontologies, in particular being used for importing information from other ontologies. Individual identifiers are used to refer to resources, and data literals are used to refer to data values.
There are two builtin classes in OWL, they both use URI references in the OWL namespace, i.e., names starting with http://www.w3.org/2002/07/owl#, for which the namespace name owl is used here. (Throughout this document qualified names will be used as abbreviations for URI references.) The class with identifier owl:Thing is the class of all individuals The class with identifier owl:Nothing is the empty class. Both classes are part of OWL Lite.
The following XML Schema datatypes [XML Schema Datatypes] can be used in OWL as builtin datatypes by means of the XML Schema canonical URI reference for the datatype, http://www.w3.org/2001/XMLSchema#name, where name is the local name of the datatype: xsd:string, xsd:boolean, xsd:decimal, xsd:float, xsd:double, xsd:dateTime, xsd:time, xsd:date, xsd:gYearMonth, xsd:gYear, xsd:gMonthDay, xsd:gDay, xsd:gMonth, xsd:hexBinary, xsd:base64Binary, xsd:anyURI, xsd:normalizedString, xsd:token, xsd:language, xsd:NMTOKEN, xsd:Name, xsd:NCName, xsd:integer, xsd:nonPositiveInteger, xsd:negativeInteger, xsd:long, xsd:int, xsd:short, xsd:byte, xsd:nonNegativeInteger, xsd:unsignedLong, xsd:unsignedInt, xsd:unsignedShort, xsd:unsignedByte and xsd:positiveInteger. The other builtin RDF Schema datatypes are problematic for OWL, as discussed in Section 3.4 of RDF Semantics [RDF MT]. The builtin RDF datatype, rdf:XMLLiteral, is also an OWL builtin datatype. Because there is no standard way to go from a URI reference to an XML Schema datatype in an XML Schema, there is no standard way to use userdefined XML Schema datatypes in OWL.
NOTE: The treatment of datatypes in OWL heavily depends on postlastcall changes made to RDF.
There are several builtin annotation properties in OWL, namely owl:versionInfo, rdfs:label, rdfs:comment, rdfs:seeAlso, and rdfs:isDefinedBy. In keeping with their definition in RDF, rdfs:label and rdfs:comment can only be used with data literals.
There are also several builtin ontology properties; they are owl:imports, owl:priorVersion, owl:backwardCompatibleWith, and owl:incompatibleWith. Ontology annotations that use owl:imports have the extra effect of importing the target ontology.
Many OWL constructs use annotations, which, just like annotation directives, are used to record information associated with some portion of the construct.
annotation ::= 'annotation(' annotationPropertyID URIreference ')'  'annotation(' annotationPropertyID dataLiteral ')'  'annotation(' annotationPropertyID individual ')'
There are two kinds of facts in the OWL abstract syntax.
The first kind of fact states information about a particular individual, in the form of classes that the individual belongs to plus properties and values of that individual. An individual can be given an individualID that will denote that individual, and can be used to refer to that individual. However, an individual need not be given an individualID; such individuals are anonymous (blank in RDF terms) and cannot be directly referred to elsewhere. The syntax here is set up to somewhat mirror RDF/XML syntax [RDF Syntax] without the use of rdf:nodeID.
fact ::= individual individual ::= 'Individual(' [ individualID ] { annotation } { 'type(' type ')' } { value } ')' value ::= 'value(' individualvaluedPropertyID individualID ')'  'value(' individualvaluedPropertyID individual ')'  'value(' datavaluedPropertyID dataLiteral ')'
Facts are the same in the OWL Lite and OWL DL abstract syntaxes, except for what can be a type. In OWL Lite, types can be class IDs or OWL Lite restrictions, see Section 2.3.1.2
type ::= classID  restriction
In the OWL DL abstract syntax types can be general descriptions, which include class IDs and OWL Lite restrictions as well as other constructs
type ::= description
Data literals in the abstract syntax are either plain literals or typed literals. Plain literals consist of a Unicode string in Normal Form C and an optional language tag, as in RDF plain literals [RDF Concepts]. Typed literals consist of a lexical representation and a URI reference, as in RDF typed literals [RDF Concepts], but without the optional language tag.
NOTE: A postlastcall change to RDF has removed language tags from typed literals. As these were not allowed in the abstract syntax anyway, no change is required here.
dataLiteral ::= typedLiteral  untypedLiteral typedLiteral ::= lexicalForm^^URIReference untypedLiteral ::= lexicalForm  lexicalForm@languageTag lexicalForm ::= as in RDF, a unicode string in normal form C languageTag ::= as in RDF, an XML language tag
The second kind of fact is used to make individual identifiers be the same or pairwise distinct.
fact ::= 'SameIndividual(' individualID individualID {individualID} ')'  'DifferentIndividuals(' individualID individualID {individualID} ')'
The biggest differences between the OWL Lite and OWL DL abstract syntaxes show up in the axioms, which are used to provide information about classes and properties. As it is the smaller language, OWL Lite axioms are given first, in Section 2.3.1. The OWL DL axioms are given in Section 2.3.2. OWL DL axioms include OWL Lite axioms as special cases.
Axioms are used to associate class and property identifiers with either partial or complete specifications of their characteristics, and to give other information about classes and properties. Axioms used to be called definitions, but they are not all definitions in the common sense of the term, as has been made evident in several discussions in the WG, and thus a more neutral name has been chosen.
The syntax used here is meant to look somewhat like the syntax used in some frame systems. Each class axiom in OWL Lite contains a collection of moregeneral classes and a collection of local property restrictions in the form of restriction constructs. The restriction construct gives the local range of a property, how many values are permitted, and/or a collection of required values. The class is made either equivalent to or a subset of the intersection of these moregeneral classes and restrictions. In the OWL DL abstract syntax a class axiom contains a collection of descriptions, which can be moregeneral classes, restrictions, sets of individuals, and boolean combinations of descriptions. Classes can also be specified by enumeration or be made equivalent or disjoint.
Properties can be equivalent to or subproperties of others; can be made functional, inverse functional, symmetric, or transitive; and can be given global domains and ranges. However, most information concerning properties is more naturally expressed in restrictions, which allow local range and cardinality information to be specified.
URI references used as class IDs or datatype IDs have to be differentiated, and so need an axiom, except for the builtin OWL classes and datatypes and rdfs:Literal. There can be more than one axiom for a class or datatype. Properties used in an abstract syntax ontology have to be categorized as either datavalued or individualvalued or annotation properties. Properties thus also need an axiom for this purpose, at least. If an ontology imports another ontology, the axioms in the imported ontology (and any ontologies it imports, and so on) can be used for these purposes.
In OWL Lite class axioms are used to state that a class is exactly equivalent to, for the modality complete, or a subclass of, for the modality partial, the conjunction of a collection of superclasses and OWL Lite Restrictions. It is also possible to indicate that the use of a class is deprecated.
axiom ::= 'Class(' classID ['Deprecated'] modality { annotation } { super } ')' modality ::= 'complete'  'partial' super ::= classID  restriction
In OWL Lite it is possible to state that two or more classes are equivalent.
axiom ::= 'EquivalentClasses(' classID classID { classID } ')'
Datatype axioms are simpler, only serving to say that a datatype ID is the ID of a datatype and to give annotations for the datatype.
axiom ::= 'Datatype(' datatypeID ['Deprecated'] { annotation } )'
Restrictions are used in OWL Lite class axioms to provide local constraints on properties in the class. Each allValuesFrom part of a restriction makes the constraint that all values of the property for individuals in the class must belong to the specified class or datatype. Each someValuesFrom part makes the constraint that there must be at least one value for the property that belongs to the specified class or datatype. The cardinality part says how many distinct values there are for the property for each individual in the class. In OWL Lite the only cardinalities allowed are 0 and 1.
See Section 2.3.1.3 for a limitation on which properties can have cardinality parts in restrictions.
restriction ::= 'restriction(' datavaluedPropertyID dataRestrictionComponent ')'  'restriction(' individualvaluedPropertyID individualRestrictionComponent ')' dataRestrictionComponent ::= 'allValuesFrom(' dataRange ')'  'someValuesFrom(' dataRange ')'  cardinality individualRestrictionComponent ::= 'allValuesFrom(' classID ')'  'someValuesFrom(' classID ')'  cardinality cardinality ::= 'minCardinality(0)'  'minCardinality(1)'  'maxCardinality(0)'  'maxCardinality(1)'  'cardinality(0)'  'cardinality(1)'
Properties are also specified using a framelike syntax. Datavalued properties relate individuals to data values, like integers. Individualvalued properties relate individuals to other individuals. These two kinds of properties can be given superproperties, allowing the construction of a property hierarchy. It does not make sense to have an individualvalued property be a superproperty of a datavalued property, or vice versa. Datavalued and individualvalued properties can also be given domains and ranges. A domain for a property specifies which individuals are potential subjects of statements that have the property as predicate, just as in RDFS. In OWL Lite the domains of properties are classes. There can be multiple domains, in which case only individuals that belong to all of the domains are potential subjects. A range for a property specifies which individuals or data values can be objects of statements that have the property as predicate. Again, there can be multiple ranges, in which case only individuals or data values that belong to all of the ranges are potential objects. In OWL Lite ranges for individualvalued properties are classes; ranges for datavalued properties are datatypes.
Datavalued properties can be specified as (partial) functional, i.e., given an individual, there can be at most one relationship to a data value for that individual in the property. Individualvalued properties can be specified to be the inverse of another property. Individualvalued properties can also be specified to be symmetric as well as partial functional, partial inversefunctional, or transitive.
Annotation and ontology properties are much simpler than datavalued and individualvalued properties. The only information in axioms for them is annotations.
axiom ::= 'DatatypeProperty(' datavaluedPropertyID ['Deprecated'] { annotation } { 'super(' datavaluedPropertyID ')' } ['Functional'] { 'domain(' classID' ')' } { 'range(' dataRange ')' } ')'  'ObjectProperty(' individualvaluedPropertyID ['Deprecated'] { annotation } { 'super(' individualvaluedPropertyID ')' } [ 'inverseOf(' individualvaluedPropertyID ')' ] [ 'Symmetric' ] [ 'Functional'  'InverseFunctional'  'Functional' 'InverseFunctional'  'Transitive' ] { 'domain(' classID ')' } { 'range(' classID ')' } ')'  'AnnotationProperty(' annotationPropertyID { annotation } ')'  'OntologyProperty(' ontologyPropertyID { annotation } ')' dataRange ::= datatypeID  rdfs:Literal
The following axioms make several properties be equivalent, or make one property be a subproperty of another.
axiom ::= 'EquivalentProperties(' datavaluedPropertyID datavaluedPropertyID { datavaluedPropertyID } ')'  'SubPropertyOf(' datavaluedPropertyID datavaluedPropertyID ')'  'EquivalentProperties(' individualvaluedPropertyID individualvaluedPropertyID { individualvaluedPropertyID } ')'  'SubPropertyOf(' individualvaluedPropertyID individualvaluedPropertyID ')'
The OWL DL abstract syntax has moregeneral versions of the OWL Lite class axioms where superclasses, moregeneral restrictions, and boolean combinations of these are allowed. Together, these constructs are called descriptions.
axiom ::= 'Class(' classID ['Deprecated'] modality { annotation } { description } ')' modality ::= 'complete'  'partial'
In the OWL DL abstract syntax it is also possible to make a class exactly consist of a certain set of individuals, as follows.
axiom ::= 'EnumeratedClass(' classID ['Deprecated'] { annotation } { individualID } ')'
Finally, in the OWL DL abstract syntax it is possible to require that a collection of descriptions be pairwise disjoint, or have the same instances, or that one description is a subclass of another. Note that the last two of these axioms generalize, except for lack of annotation, the first kind of class axiom just above.
axiom ::= 'DisjointClasses(' description description { description } ')'  'EquivalentClasses(' description { description } ')'  'SubClassOf(' description description ')'
In OWL DL it is permitted to have only one description in an EquivalentClasses construct. This allows ontologies to include descriptions that are not connected to anything, which is not semantically useful, but makes allowances for lessthanoptimal editing of ontologies.
Datatype axioms are the same as in OWL Lite.
axiom ::= 'Datatype(' datatypeID ['Deprecated'] { annotation } )'
Descriptions in the OWL DL abstract syntax include class identifiers and restrictions. Descriptions can also be boolean combinations of other descriptions, and sets of individuals.
description ::= classID  restriction  'unionOf(' { description } ')'  'intersectionOf(' { description } ')'  'complementOf(' description ')'  'oneOf(' { individualID } ')'
Restrictions in the OWL DL abstract syntax generalize OWL Lite restrictions by allowing descriptions where classes are allowed in OWL Lite and allowing sets of data values as well as datatypes. The combination of datatypes and sets of data values is called a data range. In the OWL DL abstract syntax, values can also be given for properties in classes. In addition, cardinalities are not restricted to only 0 and 1.
restriction ::= 'restriction(' datavaluedPropertyID dataRestrictionComponent { dataRestrictionComponent } ')'  'restriction(' individualvaluedPropertyID individualRestrictionComponent { individualRestrictionComponent } ')' dataRestrictionComponent ::= 'allValuesFrom(' dataRange ')'  'someValuesFrom(' dataRange ')'  'value(' dataLiteral ')'  cardinality individualRestrictionComponent ::= 'allValuesFrom(' description ')'  'someValuesFrom(' description ')'  'value(' individualID ')'  cardinality cardinality ::= 'minCardinality(' nonnegativeinteger ')'  'maxCardinality(' nonnegativeinteger ')'  'cardinality(' nonnegativeinteger ')'
A data range, used as the range of a datavalued property and in other places in the OWL DL abstract syntax, is either a datatype or a set of data values.
dataRange ::= datatypeID  rdfs:Literal  'oneOf(' { dataLiteral } ')'
The OWL Lite limitations on which properties can have cardinality components in their restrictions are also present in OWL DL.
Property axioms in the OWL DL abstract syntax generalize OWL Lite property axioms by allowing descriptions in place of classes and data ranges in place of datatypes in domains and ranges.
axiom ::= 'DatatypeProperty(' datavaluedPropertyID ['Deprecated'] { annotation } { 'super(' datavaluedPropertyID ')'} ['Functional'] { 'domain(' description ')' } { 'range(' dataRange ')' } ')'  'ObjectProperty(' individualvaluedPropertyID ['Deprecated'] { annotation } { 'super(' individualvaluedPropertyID ')' } [ 'inverseOf(' individualvaluedPropertyID ')' ] [ 'Symmetric' ] [ 'Functional'  'InverseFunctional'  'Functional' 'InverseFunctional'  'Transitive' ] { 'domain(' description ')' } { 'range(' description ')' } ')'  'AnnotationProperty(' annotationPropertyID { annotation } ')'  'OntologyProperty(' ontologyPropertyID { annotation } ')'
The limitations on which properties can be specified to be functional or inversefunctional is also present in OWL DL.
As in OWL Lite, the following axioms make several properties be equivalent, or make one property be a subproperty of another.
axiom ::= 'EquivalentProperties(' datavaluedPropertyID datavaluedPropertyID { datavaluedPropertyID } ')'  'SubPropertyOf(' datavaluedPropertyID datavaluedPropertyID ')'  'EquivalentProperties(' individualvaluedPropertyID individualvaluedPropertyID { individualvaluedPropertyID } ')'  'SubPropertyOf(' individualvaluedPropertyID individualvaluedPropertyID ')'
This modeltheoretic semantics for OWL goes directly from ontologies in the OWL DL abstract syntax, which includes the OWL Lite abstract syntax, to a standard model theory. It is simpler than the semantics in Section 5, which is a vocabulary extension of the RDFS semantics.
The semantics here starts with the notion of a vocabulary. When considering an OWL ontology, the vocabulary must include all the URI references in that ontology, as well as ontologies that are imported by the ontology, but can include other URI references as well.
In this section V_{OP} will be the URI references for the builtin OWL ontology properties.
Definition: An OWL vocabulary V consists of seven sets of URI references, V_{C}, V_{D}, V_{I}, V_{DP}, V_{IP}, V_{AP}, and V_{O}. In any vocabulary V_{C} and V_{D} are disjoint and V_{DP}, V_{IP}, V_{AP}, and V_{OP} are pairwise disjoint. V_{C}, the class names of a vocabulary, contains owl:Thing and owl:Nothing. V_{D}, the datatype names of a vocabulary, contains the URI references for the builtin OWL datatypes and rdfs:Literal. V_{AP}, the annotation property names of a vocabulary, contains owl:versionInfo, rdfs:label, rdfs:comment, rdfs:seeAlso, and rdfs:isDefinedBy. V_{IP}, the individualvalued property names of a vocabulary, V_{DP}, the datavalued property names of a vocabulary, and V_{I}, the individual names of a vocabulary, V_{O}, the ontology names of a vocabulary, do not have any required members.
Definition: A datatype theory T is a partial mapping from URI references to datatypes that maps xsd:string and xsd:integer to the appropriate XML Schema datatypes.
A datatype theory may contain datatypes for the other builtin OWL datatypes. It may also contain other datatypes, but there is no provision in the OWL syntax for conveying what these datatypes are.
Definition: Let T be a datatype theory. An Abstract OWL interpretation with respect to T with vocabulary V_{C}, V_{D}, V_{I}, V_{DP}, V_{IP}, V_{AP}, V_{O} is a tuple of the form: I = <R, EC, ER, L, S, LV> where (with P being the power set operator)
EC provides meaning for URI references that are used as OWL classes and datatypes. ER provides meaning for URI references that are used as OWL properties. (The property rdf:type is added to the annotation properties so as to provide a meaning for deprecation, see below.)'' L provides meaning for typed literals. S provides meaning for URI references that are used to denote OWL individuals, and helps provide meaning for annotations. Note that there are no interpretations that can satisfy all the requirements placed on badlyformed literals, i.e., one whose lexical form is invalid for the datatype, such as 1.5^^xsd:integer.
S is extended to plain literals by (essentially) mapping them onto themselves, i.e., S("l") = l for l a plain literal without a language tag and S("l"@t) = <l,t> for l a plain literal with a language tag. S is extended to typed literals by using L, S(l) = L(l) for l a typed literal.
EC is extended to the syntactic constructs of descriptions, data ranges, individuals, values, and annotations as in the EC Extension Table.
Abstract Syntax  Interpretation (value of EC) 

complementOf(c)  O  EC(c) 
unionOf(c_{1} … c_{n})  EC(c_{1}) ∪ … ∪ EC(c_{n}) 
intersectionOf(c_{1} … c_{n})  EC(c_{1}) ∩ … ∩ EC(c_{n}) 
oneOf(i_{1} … i_{n}), for i_{j} individual IDs  {S(i_{1}), …, S(i_{n})} 
oneOf(v_{1} … v_{n}), for v_{j} literals  {S(v_{1}), …, S(v_{n})} 
restriction(p x_{1} … x_{n}), for n > 1  EC(restriction(p x_{1})) ∩…∩EC(restriction(p x_{n})) 
restriction(p allValuesFrom(r))  {x ∈ O  <x,y> ∈ ER(p) implies y ∈ EC(r)} 
restriction(p someValuesFrom(e))  {x ∈ O  ∃ <x,y> ∈ ER(p) ∧ y ∈ EC(e)} 
restriction(p value(i)), for i an individual ID  {x ∈ O  <x,S(i)> ∈ ER(p)} 
restriction(p value(v)), for v a literal  {x ∈ O  <x,S(v)> ∈ ER(p)} 
restriction(p minCardinality(n))  {x ∈ O  card({y ∈ O∪LV : <x,y> ∈ ER(p)}) ≥ n} 
restriction(p maxCardinality(n))  {x ∈ O  card({y ∈ O∪LV : <x,y> ∈ ER(p)}) ≤ n} 
restriction(p cardinality(n))  {x ∈ O  card({y ∈ O∪LV : <x,y> ∈ ER(p)}) = n} 
Individual(annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) type(c_{1}) … type(c_{m}) pv_{1} … pv_{n}) 
EC(annotation(p_{1} o_{1})) ∩ …
EC(annotation(p_{k} o_{k})) ∩ EC(c_{1}) ∩ … ∩ EC(c_{m}) ∩ EC(pv_{1}) ∩…∩ EC(pv_{n}) 
Individual(i annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) type(c_{1}) … type(c_{m}) pv_{1} … pv_{n}) 
{S(i)} ∩ EC(annotation(p_{1} o_{1})) ∩ …
EC(annotation(p_{k} o_{k})) ∩ EC(c_{1}) ∩ … ∩ EC(c_{m}) ∩ EC(pv_{1}) ∩…∩ EC(pv_{n}) 
value(p Individual(…))  {x ∈ O  ∃ y∈EC(Individual(…)) : <x,y> ∈ ER(p)} 
value(p id) for id an individual ID  {x ∈ O  <x,S(id)> ∈ ER(p) } 
value(p v) for v a literal  {x ∈ O  <x,S(v)> ∈ ER(p) } 
annotation(p o) for o a URI reference  {x ∈ R  <x,S(o)> ∈ ER(p) } 
annotation(p Individual(…))  {x ∈ R  ∃ y ∈ EC(Individual(…)) : <x,y> ∈ ER(p) } 
An Abstract OWL interpretation, I, satisfies OWL axioms and facts as given in Axiom and Fact Interpretation Table. In the table, optional parts of axioms and facts are given in square brackets ([…]) and have corresponding optional conditions, also given in square brackets.
Directive  Conditions on interpretations 

Class(c [Deprecated] complete annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) descr_{1} … descr_{n}) 
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p_{1} o_{1})) … S(c) ∈ EC(annotation(p_{k} o_{k})) EC(c) = EC(descr_{1}) ∩…∩ EC(descr_{n}) 
Class(c [Deprecated] partial annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) descr_{1} … descr_{n}) 
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p_{1} o_{1})) … S(c) ∈ EC(annotation(p_{k} o_{k})) EC(c) ⊆ EC(descr_{1}) ∩…∩ EC(descr_{n}) 
EnumeratedClass(c [Deprecated] annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) i_{1} … i_{n}) 
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p_{1} o_{1})) … S(c) ∈ EC(annotation(p_{k} o_{k})) EC(c) = { S(i_{1}), …, S(i_{n}) } 
Datatype(c [Deprecated] annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) ) 
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p_{1} o_{1})) … S(c) ∈ EC(annotation(p_{k} o_{k})) EC(c) ⊆ LV 
DisjointClasses(d_{1} … d_{n})  EC(d_{i}) ∩ EC(d_{j}) = { } for 1 ≤ i < j ≤ n 
EquivalentClasses(d_{1} … d_{n})  EC(d_{i}) = EC(d_{j}) for 1 ≤ i < j ≤ n 
SubClassOf(d_{1} d_{2})  EC(d_{1}) ⊆ EC(d_{2}) 
DatatypeProperty(p [Deprecated] annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) super(s_{1}) … super(s_{n}) domain(d_{1}) … domain(d_{n}) range(r_{1}) … range(r_{n}) [Functional]) 
[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type) ] S(p) ∈ EC(annotation(p_{1} o_{1})) … S(p) ∈ EC(annotation(p_{k} o_{k})) ER(p) ⊆ O×LV ∩ ER(s_{1}) ∩…∩ ER(s_{n}) ∩ EC(d_{1})×LV ∩…∩ EC(d_{n})×LV ∩ O×EC(r_{1}) ∩…∩ O×EC(r_{n}) [ER(p) is functional] 
ObjectProperty(p [Deprecated] annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) super(s_{1}) … super(s_{n}) domain(d_{1}) … domain(d_{n}) range(r_{1}) … range(r_{n}) [inverse(i)] [Symmetric] [Functional] [ InverseFunctional] [Transitive]) 
[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type)] S(p) ∈ EC(annotation(p_{1} o_{1})) … S(p) ∈ EC(annotation(p_{k} o_{k})) ER(p) ⊆ O×O ∩ ER(s_{1}) ∩…∩ ER(s_{n}) ∩ EC(d_{1})×O ∩…∩ EC(d_{n})×O ∩ O×EC(r_{1}) ∩…∩ O×EC(r_{n}) [ER(p) is the inverse of ER(i)] [ER(p) is symmetric] [ER(p) is functional] [ER(p) is inverse functional] [ER(p) is transitive] 
AnnotationProperty(p annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}))  S(p) ∈ EC(annotation(p_{1} o_{1})) … S(p) ∈ EC(annotation(p_{k} o_{k})) 
OntologyProperty(p annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}))  S(p) ∈ EC(annotation(p_{1} o_{1})) … S(p) ∈ EC(annotation(p_{k} o_{k})) 
EquivalentProperties(p_{1} … p_{n})  ER(p_{i}) = ER(p_{j}) for 1 ≤ i < j ≤ n 
SubPropertyOf(p_{1} p_{2})  ER(p_{1}) ⊆ ER(p_{2}) 
SameIndividual(i_{1} … i_{n})  S(i_{j}) = S(i_{k}) for 1 ≤ j < k ≤ n 
DifferentIndividuals(i_{1} … i_{n})  S(i_{j}) ≠ S(i_{k}) for 1 ≤ j < k ≤ n 
Individual([i] annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) type(c_{1}) … type(c_{m}) pv_{1} … pv_{n}) 
EC(Individual([i] annotation(p_{1} o_{1}) … annotation(p_{k} o_{k}) type(c_{1}) … type(c_{m}) pv_{1} … pv_{n})) is nonempty 
From Section 2, an OWL ontology can have annotations, which need their own semantic conditions. Aside from this local meaning, an owl:imports annotation also imports the contents of another OWL ontology into the current ontology. The imported ontology is the one, if any, that has as name the argument of the imports construct. (This treatment of imports is divorced from Web issues. The intended use of names for OWL ontologies is to make the name be the location of the ontology on the Web, but this is outside of this formal treatment.)
Definition: Let T be a datatype theory. An Abstract OWL interpretation, I, with respect to T with vocabulary consisting of V_{C}, V_{D}, V_{I}, V_{DP}, V_{IP}, V_{AP}, V_{O}, satisfies an OWL ontology, O, iff
Definition: An Abstract OWL ontology is consistent with respect to datatype theory T iff there is some interpretation I with respect to T such that I satisfies the ontology.
Definition: A collection of abstract OWL ontologies entails an OWL axiom or fact with respect to a datatype theory T iff each interpretation with respect to T that satisfies each of the ontologies also satisfies the axiom or fact. A collection of abstract OWL ontologies entails an abstract OWL ontology with respect to a datatype theory T if each interpretation with respect to T that satisfies each ontology in the collection also satisfies the ontology.
This section of the document provides a mapping from the abstract syntax for OWL DL and OWL Lite given in Section 2 to the exchange syntax for OWL, namely RDF/XML [RDF Syntax]. This mapping (and its inverse) provide the normative relationship between the abstract syntax and the exchange syntax. It is shown in Section 5 and Appendix A.1 that this mapping preserves the meaning of OWL DL ontologies. Section 4.2 defines the OWL DL and OWL Lite dialects of OWL as those RDF graphs that are the result of mappings from abstract syntax ontologies.
The exchange syntax for OWL is RDF/XML [RDF Syntax], as specified in the OWL Reference Description [OWL Reference]. Further, the meaning of an OWL ontology in RDF/XML is determined only from the RDF graph [RDF Concepts] that results from the RDF parsing of the RDF/XML document. Thus one way of translating an OWL ontology in abstract syntax form into the exchange syntax is by giving a transformation of each directive into a collection of triples. As all OWL Lite constructs are special cases of constructs in the full abstract syntax, transformations are only provided for the OWL DL versions.
OWL DL has semantics defined over the abstract syntax and a concrete syntax consisting of a subset of RDF graphs. Hence it is necessary to relate specific abstract syntax ontologies with specific RDF/XML documents and their corresponding graphs. This section defines a manytomany relationship between abstract syntax ontologies and RDF graphs. This is done using a set of nondeterministic mapping rules. Thus to apply the semantics to a particular RDF graph it is necessary to find one of the abstract syntax ontologies that correspond with that graph under the mapping rules and to apply the semantics to that abstract ontology. The mapping is designed so that any of the RDF/XML graphs that correspond to a particular abstract ontology have the same meaning, as do any of the abstract ontologies that correspond to a particular RDF/XML graph. Moreover, since this process cannot be applied to RDF graphs that do not have corresponding abstract syntax forms, the mapping rules implicitly define a set of graphs, which syntactically characterise OWL DL in RDF/XML.
The syntax for triples used here is the one used in the RDF semantics [RDF MT]. In this variant, qualified names are allowed. As detailed in the RDF semantics, to turn this syntax into the standard one just expand the qualified names into URI references in the standard RDF manner by concatenating the namespace name with the local name, using the standard OWL namespaces.
The Transformation Table gives transformation rules that transform the abstract syntax to the OWL exchange syntax. In a few cases, notably for the DifferentIndividuals construct, there are different transformation rules. In such cases either rule can be chosen, resulting in a nondeterministic translation. In a few other cases, notably for class and property axioms, there are triples that may or may not be generated. These triples are indicated by flagging them with [opt]. In a couple of cases one of two triples must be generated. This is indicated by separating the triples with OR. These nondeterminisms allow the generation of more RDF Graphs.
The left column of the table gives a piece of abstract syntax (S); the center column gives its transformation into triples (T(S)); and the right column gives an identifier for the main node of the transformation (M(T(S))), for syntactic constructs that can occur as pieces of directives. Repeating components are listed using ellipses, as in description_{1} … description_{n}, this form allows easy specification of the transformation for all values of n allowed in the syntax. Optional portions of the abstract syntax (enclosed in square brackets) are optional portions of the transformation (signified by square brackets). As well, for any of the builtin OWL datatypes, builtin OWL classes, builtin OWL annotation properties, and builtin OWL ontology properties the first rdf:type triple in the translation of it or any axiom for it is optional.
Some transformations in the table are for directives. Other transformations are for parts of directives. The last transformation is for sequences, which are not part of the abstract syntax per se. This last transformation is used to make some of the other transformations more compact and easier to read.
For many directives these transformation rules call for the transformation of components of the directive using other transformation rules. When the transformation of a component is used as the subject, predicate, or object of a triple, even an optional triple, the transformation of the component is part of the production (but only once per production) and the main node of that transformation should be used in the triple.
Bnode identifiers here must be taken as local to each transformation, i.e., different identifiers should be used for each invocation of a transformation rule. Ontologies without a name are given a bnode as their main node; ontologies with a name use that name as their main node; in both cases this node is referred to as O below.
Abstract Syntax (and sequences)  S  Transformation  T(S)  Main Node  M(T(S)) 

Ontology(O directive_{1} … directive_{n})  O rdf:type owl:Ontology . T(directive_{1}) … T(directive_{n}) 

Ontology(directive_{1} … directive_{n})  O rdf:type owl:Ontology . T(directive_{1}) … T(directive_{n}) 

Annotation(ontologyPropertyID URIreference)  ontologyPropertyID rdf:type owl:OntologyProperty . O ontologyPropertyID URIreference . URIreference rdf:type owl:Ontology . 

Annotation(annotationPropertyID URIreference)  annotationPropertyID rdf:type owl:AnnotationProperty . annotationPropertyID rdf:type rdf:Property . [opt] O annotationPropertyID URIreference . 

Annotation(annotationPropertyID dataLiteral)  annotationPropertyID rdf:type owl:AnnotationProperty . annotationPropertyID rdf:type rdf:Property . [opt] O annotationPropertyID T(dataLiteral) . 

Annotation(annotationPropertyID individual)  annotationPropertyID rdf:type owl:AnnotationProperty . annotationPropertyID rdf:type rdf:Property . [opt] O annotationPropertyID T(individual) . 

rdfs:Literal  rdfs:Literal  
datatypeID  datatypeID rdf:type rdfs:Datatype .  datatypeID 
classID  classID rdf:type owl:Class . classID rdf:type rdfs:Class . [opt] 
classID 
individualID  individualID  
datavaluedPropertyID  datavaluedPropertyID rdf:type owl:DatatypeProperty . datavaluedPropertyID rdf:type rdf:Property . [opt] 
datavalued PropertyID 
individualvaluedPropertyID  individualvaluedPropertyID rdf:type owl:ObjectProperty . individualvaluedPropertyID rdf:type rdf:Property . [opt] 
individualvalued PropertyID 
dataLiteral  dataLiteral  dataLiteral 
Individual(iID annotation_{1} … annotation_{m} type(type_{1})… type(type_{n}) value(pID_{1} v_{1}) … value(pID_{k} v_{k})) 
iID T(annotation_{1}) … iID T(annotation_{m}) iID rdf:type T(type_{1}) . … iID rdf:type T(type_{n}) . iID T(pID_{1}) T(v_{1}) . … iID T(pID_{k}) T(v_{k}) . 
iID 
Individual(annotation_{1} … annotation_{m} type(type_{1})…type(type_{n}) value(pID_{1} v_{1}) … value(pID_{k} v_{k})) (With at least one type.) 
_:x T(annotation_{1}) … _:x T(annotation_{m}) _:x rdf:type T(type_{1}) . … _:x rdf:type T(type_{n}) . _:x T(pID_{1}) T(v_{1}) . … _:x T(pID_{k}) T(v_{k}) . 
_:x 
Individual(annotation_{1} … annotation_{m} value(pID_{1} v_{1}) … value(pID_{k} v_{k})) 
_:x T(annotation_{1}) … _:x T(annotation_{m}) _:x rdf:type owl:Thing . _:x T(pID_{1}) T(v_{1}) . … _:x T(pID_{k}) T(v_{k}) . 
_:x 
SameIndividual(iID_{1} … iID_{n})  iID_{i} owl:sameAs iID_{i+1} . 1≤i<n iID_{i} owl:sameAs iID_{j} . [opt] 1≤i≠j≤n 

DifferentIndividuals(iID_{1} … iID_{n})  iID_{i} owl:differentFrom iID_{j} .
OR iID_{j} owl:differentFrom iID_{i} . 1≤i<j≤n iID_{j} owl:differentFrom iID_{i} . [opt] 1≤i≠j≤n 

DifferentIndividuals(iID_{1} … iID_{n}) 
_:x rdf:type owl:AllDifferent . _:x owl:distinctMembers T(SEQ iID_{1} … iID_{n}) . 

Class(classID [Deprecated] partial annotation_{1} … annotation_{m} description_{1} … description_{n}) 
classID rdf:type owl:Class . classID rdf:type rdfs:Class . [opt] [classID rdf:type owl:DeprecatedClass .] classID T(annotation_{1}) … classID T(annotation_{m}) classID rdfs:subClassOf T(description_{1}) . … classID rdfs:subClassOf T(description_{n}) . 

Class(classID [Deprecated] complete annotation_{1} … annotation_{m} description_{1} … description_{n}) 
classID rdf:type owl:Class . classID rdf:type rdfs:Class . [opt] [classID rdf:type owl:DeprecatedClass .] classID T(annotation_{1}) … classID T(annotation_{m}) classID owl:intersectionOf T(SEQ description_{1}…description_{n}) . 

Class(classID [Deprecated] complete annotation_{1} … annotation_{m} description) 
classID rdf:type owl:Class . classID rdf:type rdfs:Class . [opt] [classID rdf:type owl:DeprecatedClass .] classID T(annotation_{1}) … classID T(annotation_{m}) classID owl:equivalentClass T(description) . 

Class(classID [Deprecated] complete annotation_{1} … annotation_{m} unionOf(description_{1} … description_{n})) 
classID rdf:type owl:Class . classID rdf:type rdfs:Class . [opt] [classID rdf:type owl:DeprecatedClass .] classID T(annotation_{1}) … classID T(annotation_{m}) classID owl:unionOf T(SEQ description_{1}…description_{n}) . 

Class(classID [Deprecated] complete annotation_{1} … annotation_{m} complementOf(description)) 
classID rdf:type owl:Class . classID rdf:type rdfs:Class . [opt] [classID rdf:type owl:DeprecatedClass .] classID T(annotation_{1}) … classID T(annotation_{m}) classID owl:complementOf T(description) . 

EnumeratedClass(classID [Deprecated] annotation_{1} … annotation_{m} iID_{1} … iID_{n}) 
classID rdf:type owl:Class . classID rdf:type rdfs:Class . [opt] [classID rdf:type owl:DeprecatedClass .] classID T(annotation_{1}) … classID T(annotation_{m}) . classID owl:oneOf T(SEQ iID_{1}…iID_{n}) . 

DisjointClasses(description_{1} … description_{n}) 
T(description_{i}) owl:disjointWith T(description_{j}) . OR T(description_{j}) owl:disjointWith T(description_{i}) . 1≤i<j≤n T(description_{i}) owl:disjointWith T(description_{j}) . [opt] 1≤i≠j≤n 

EquivalentClasses(description_{1} … description_{n}) 
T(description_{i}) owl:equivalentClass T(description_{j}) . for all <i,j> in G where G is a set of pairs over {1,...,n}x{1,...,n} that if interpreted as an undirected graph forms a connected graph for {1,...,n} 

SubClassOf(description_{1} description_{2})  T(description_{1}) rdfs:subClassOf T(description_{2}) .  
Datatype(datatypeID [Deprecated] annotation_{1} … annotation_{m} ) 
datatypeID rdf:type rdfs:Datatype . datatypeID rdf:type rdfs:Class . [opt] [datatypeID rdf:type owl:DeprecatedClass .] datatypeID T(annotation_{1}) … datatypeID T(annotation_{m}) 

unionOf(description_{1} … description_{n}) 
_:x rdf:type owl:Class . _:x rdf:type rdfs:Class . [opt] _:x owl:unionOf T(SEQ description_{1}…description_{n}) . 
_:x 
intersectionOf(description_{1} … description_{n}) 
_:x rdf:type owl:Class . _:x rdf:type rdfs:Class . [opt] _:x owl:intersectionOf T(SEQ description_{1}…description_{n}) . 
_:x 
complementOf(description)  _:x rdf:type owl:Class . _:x rdf:type rdfs:Class . [opt] _:x owl:complementOf T(description) . 
_:x 
oneOf(iID_{1} … iID_{n}) 
_:x rdf:type owl:Class . _:x rdf:type rdfs:Class . [opt] _:x owl:oneOf T(SEQ iID_{1}…iID_{n}) . 
_:x 
oneOf(v_{1} … v_{n}) 
_:x rdf:type owl:DataRange . _:x rdf:type rdfs:Class . [opt] _:x owl:oneOf T(SEQ v_{1} … v_{n}) . 
_:x 
restriction(ID component_{1} … component_{n}) (With at least two components) 
_:x rdf:type owl:Class . _:x rdf:type rdfs:Class . [opt] _:x owl:intersectionOf T(SEQ(restriction(ID component_{1}) … restriction(ID component_{n}))) . 
_:x 
restriction(ID allValuesFrom(range))  _:x rdf:type owl:Restriction . _:x rdf:type owl:Class . [opt] _:x rdf:type rdfs:Class . [opt] _:x owl:onProperty T(ID) . _:x owl:allValuesFrom T(range) . 
_:x 
restriction(ID someValuesFrom(required))  _:x rdf:type owl:Restriction . _:x rdf:type owl:Class . [opt] _:x rdf:type rdfs:Class . [opt] _:x owl:onProperty T(ID) . _:x owl:someValuesFrom T(required) . 
_:x 
restriction(ID value(value))  _:x rdf:type owl:Restriction . _:x rdf:type owl:Class . [opt] _:x rdf:type rdfs:Class . [opt] _:x owl:onProperty T(ID) . _:x owl:hasValue T(value) . 
_:x 
restriction(ID minCardinality(min))  _:x rdf:type owl:Restriction . _:x rdf:type owl:Class . [opt] _:x rdf:type rdfs:Class . [opt] _:x owl:onProperty T(ID) . _:x owl:minCardinality "min"^^xsd:nonNegativeInteger . 
_:x 
restriction(ID maxCardinality(max))  _:x rdf:type owl:Restriction . _:x rdf:type owl:Class . [opt] _:x rdf:type rdfs:Class . [opt] _:x owl:onProperty T(ID) . _:x owl:maxCardinality "max"^^xsd:nonNegativeInteger . 
_:x 
restriction(ID cardinality(card))  _:x rdf:type owl:Restriction . _:x rdf:type owl:Class . [opt] _:x rdf:type rdfs:Class . [opt] _:x owl:onProperty T(ID) . _:x owl:cardinality "card"^^xsd:nonNegativeInteger . 
_:x 
DatatypeProperty(ID [Deprecated] annotation_{1} … annotation_{m} super(super_{1})… super(super_{n}) domain(domain_{1})… domain(domain_{k}) range(range_{1})… range(range_{h}) [Functional]) 
ID rdf:type owl:DatatypeProperty . ID rdf:type rdf:Property . [opt] [ID rdf:type owl:DeprecatedProperty .] ID T(annotation_{1}) … ID T(annotation_{m}) ID rdfs:subPropertyOf T(super_{1}) . … ID rdfs:subPropertyOf T(super_{n}) . ID rdfs:domain T(domain_{1}) . … ID rdfs:domain T(domain_{k}) . ID rdfs:range T(range_{1}) . … ID rdfs:range T(range_{h}) . [ID rdf:type owl:FunctionalProperty . ] 

ObjectProperty(ID [Deprecated] annotation_{1} … annotation_{m} super(super_{1})… super(super_{n}) domain(domain_{1})… domain(domain_{k}) range(range_{1})… range(range_{h}) [inverseOf(inverse)] [Functional  InverseFunctional  Transitive]) [Symmetric] 
ID rdf:type owl:ObjectProperty . [opt if one of the last three triples is included] ID rdf:type rdf:Property . [opt] [ID rdf:type owl:DeprecatedProperty .] ID T(annotation_{1}) … ID T(annotation_{m}) ID rdfs:subPropertyOf T(super_{1}) . … ID rdfs:subPropertyOf T(super_{n}) . ID rdfs:domain T(domain_{1}) . … ID rdfs:domain T(domain_{k}) . ID rdfs:range T(range_{1}) . … ID rdfs:range T(range_{h}) . [ID owl:inverseOf T(inverse) .] [ID rdf:type owl:FunctionalProperty . ] [ID rdf:type owl:InverseFunctionalProperty . ] [ID rdf:type owl:TransitiveProperty . ] [ID rdf:type owl:SymmetricProperty . ] 

AnnotationProperty(ID annotation_{1} … annotation_{m}) 
ID rdf:type owl:AnnotationProperty . ID rdf:type rdf:Property . [opt] ID T(annotation_{1}) … ID T(annotation_{m}) 

OntologyProperty(ID annotation_{1} … annotation_{m}) 
ID rdf:type owl:OntologyProperty . ID rdf:type rdf:Property . [opt] ID T(annotation_{1}) … ID T(annotation_{m}) 

EquivalentProperties(dvpID_{1} … dvpID_{n})  T(dvpID_{i}) owl:equivalentProperty T(dvpID_{i+1}) . 1≤i<n  
SubPropertyOf(dvpID_{1} dvpID_{2})  T(dvpID_{1}) rdfs:subPropertyOf T(dvpID_{2}) .  
EquivalentProperties(ivpID_{1} … ivpID_{n})  T(ivpID_{i}) owl:equivalentProperty T(ivpID_{i+1}) . 1≤i<n  
SubPropertyOf(ivpID_{1} ivpID_{2})  T(ivpID_{1}) rdfs:subPropertyOf T(ivpID_{2}) .  
annotation(annotationPropertyID URIreference)  annotationPropertyID URIreference . annotationPropertyID rdf:type owl:AnnotationProperty . annotationPropertyID rdf:type rdf:Property . [opt] 

annotation(annotationPropertyID dataLiteral)  annotationPropertyID T(dataLiteral) . annotationPropertyID rdf:type owl:AnnotationProperty . annotationPropertyID rdf:type rdf:Property . [opt] 

annotation(annotationPropertyID individual)  annotationPropertyID T(individual) . annotationPropertyID rdf:type owl:AnnotationProperty . annotationPropertyID rdf:type rdf:Property . [opt] 

SEQ  rdf:nil  
SEQ item_{1}…item_{n} 
_:l_{1} rdf:type rdf:List . [opt] _:l_{1} rdf:first T(item_{1}) . _:l_{1} rdf:rest _:l_{2} . … _:ln rdf:type rdf:List . [opt] _:ln rdf:first T(item_{n}) . _:ln rdf:rest rdf:nil . 
_:l_{1} 
This transformation is not injective, as several OWL abstract ontologies that do not use the above reserved vocabulary can map into equal RDF graphs. However, the only cases where this can happen is with constructs that have the same meaning, such as several DisjointClasses axioms having the same effect as one larger one. It would be possible to define a canonical inverse transformation, if desired.
When considering OWL Lite and DL ontologies in RDF graph form, care must be taken to prevent the use of certain vocabulary as OWL classes, properties, or individuals. If this is not done the builtin definitions or use of this vocabulary (in the RDF or OWL specification) would augment the information in the OWL ontology. Only some of the RDF vocabulary fits in this category, as some of the RDF vocabulary, such as rdf:subject, is given little or no meaning by the RDF specifications and its use does not present problems, as long as the use is consistent with any meaning given by the RDF specifications.
Definition: The disallowed vocabulary from RDF is rdf:type, rdf:Property, rdf:nil, rdf:List, rdf:first, rdf:rest, rdfs:domain, rdfs:range, rdfs:Resource, rdfs:Datatype, rdfs:Class, rdfs:subClassOf, rdfs:subPropertyOf, rdfs:member, rdfs:Container and rdfs:ContainerMembershipProperty. The disallowed vocabulary from OWL is owl:AllDifferent, owl:allValuesFrom, owl:AnnotationProperty, owl:cardinality, owl:Class, owl:complementOf, owl:DataRange, owl:DatatypeProperty, owl:DeprecatedClass, owl:DeprecatedProperty, owl:differentFrom, owl:disjointWith, owl:distinctMembers, owl:equivalentClass, owl:equivalentProperty, owl:FunctionalProperty, owl:hasValue, owl:intersectionOf, owl:InverseFunctionalProperty, owl:inverseOf, owl:maxCardinality, owl:minCardinality, owl:ObjectProperty, owl:oneOf, owl:onProperty, owl:Ontology, owl:OntologyProperty, owl:Restriction, owl:sameAs, owl:someValuesFrom, owl:SymmetricProperty, owl:TransitiveProperty, and owl:unionOf. The disallowed vocabulary is the union of the disallowed vocabulary from RDF and the disallowed vocabulary from OWL.
Definition: The classonly vocabulary is rdf:Statement, rdf:Seq, rdf:Bag, and rdf:Alt. The datatypeonly vocabulary is the builtin OWL datatypes. The propertyonly vocabulary is rdf:subject, rdf:predicate, rdf:object, and all the container membership properties, i.e., rdf:_1, rdf:_2, ….
Definition: A collection of OWL DL ontologies in abstract syntax form, O, has a separated vocabulary if
Definition: An RDF graph is an OWL DL ontology in RDF graph form if it is equal (see below for a slight relaxation) to a result of the transformation to triples above of a collection of OWL DL ontologies in abstract syntax form that has a separated vocabulary. For the purposes of determining whether an RDF graph is an OWL DL ontology in RDF graph form, cardinality restrictions are explicitly allowed to use constructions like "1"^^xsd:integer so long as the data value so encoded is a nonnegative integer.
Definition: An RDF graph is an OWL Lite ontology in RDF graph form if it is as above except that the ontologies in O are OWL Lite ontologies in abstract syntax form.
This modeltheoretic semantics for OWL is an extension of the semantics defined in the RDF semantics [RDF MT], and defines the OWL semantic extension of RDF.
NOTE: The details of this semantics depends on several postlastcall fixes and other changes to the RDF model theory. Most of these changes are not noticable, but several, including the removal of language tags from typed literals and the changes to datatypes, result in noticable changes.
All of the OWL vocabulary is defined on the 'OWL universe', which is a division of part of the RDF universe into three parts, namely OWL individuals, classes, and properties. The class extension of owl:Thing comprises the individuals of the OWL universe. The class extension of owl:Class comprises the classes of the OWL universe. The union of the class extensions of owl:ObjectProperty, owl:DatatypeProperty, owl:AnnotationProperty, and owl:OntologyProperty comprises the properties of the OWL universe.
There are two different styles of using OWL. In the more freewheeling style, called OWL Full, the three parts of the OWL universe are identified with their RDF counterparts, namely the class extensions of rdfs:Resource, rdfs:Class, and rdf:Property. In OWL Full, as in RDF, elements of the OWL universe can be both an individual and a class, or, in fact, even an individual, a class, and a property. In the more restrictive style, called OWL DL here, the three parts are different from their RDF counterparts and, moreover, pairwise disjoint. The morerestrictive OWL DL style gives up some expressive power in return for decidability of entailment. Both styles of OWL provide entailments that are missing in a naive translation of the DAML+OIL modeltheoretic semantics into the RDF semantics.
A major difference in practice between the two styles lies in the care that is required to ensure that URI references are actually in the appropriate part of the OWL universe. In OWL Full, no care is needed. In OWL DL, localizing information must be provided for many of the URI references used. These localizing assumptions are all trivially true in OWL Full, and can also be ignored when one uses the OWL abstract syntax, which corresponds closely to OWL DL. But when writing OWL DL in triples, however, close attention must be paid to which elements of the vocabulary belong to which part of the OWL universe.
Throughout this section the OWL vocabulary will be the disallowed vocabulary from OWL plus the builtin classes, the builtin annotation properties, and the builtin ontology properties.
The semantics of OWL DL and OWL Full are very similar. The common portion of their semantics is thus given first, and the differences left until later.
From the RDF semantics [RDF MT], for V a set of URI references containing the RDF and RDFS vocabulary and T a datatype theory, a Tinterpretation of V is a tuple I = < R_{I}, P_{I}, EXT_{I}, S_{I}, L_{I}, LV_{I} >. R_{I} is the domain of discourse or universe, i.e., a set that contains the denotations of URI references. (The specifics of datatype theories used here differ slightly from those in the RDF semantics currently under review. It is expected that these discrepancies will be resolved during last call, following which this document will be revised to correspond directly to RDF datatyping.) P_{I} is a subset of R_{I}, the properties of I. EXT_{I} is used to give meaning to properties, and is a mapping from P_{I} to P(R_{I} × R_{I}). S_{I} is a mapping from V to R_{I} that takes a URI reference to its denotation. L_{I} is a mapping from typed literals to LV_{I}. LV_{I} contains at least all the values for plain literals. CEXT_{I} is then defined as CEXT_{I}(c) = { x∈R_{I}  <x,c>∈EXT_{I}(S_{I}(rdf:type)) }. As well C_{I} is defined as C_{I} = CEXT_{I}(S_{I}(rdfs:Class)). Tinterpretations must meet several other conditions, as detailed in the RDF semantics. For example, EXT(S_{I}(rdfs:subClassOf)) must be a transitive relation and the class extension of all datatypes must be subsets of LV_{I}.
Definition: Let T be a datatype theory that includes datatypes for xsd:integer and xsd:string. An OWL interpretation, I = < R_{I}, P_{I}, EXT_{I}, S_{I}, L_{I} >, of a vocabulary V, where V includes the RDF and RDFS vocabularies and the OWL vocabulary, is a Tinterpretation of V that satisfies all the constraints in this section.
Note: Elements of the OWL vocabulary that construct descriptions in the abstract syntax are given a different treatment from elements of the OWL vocabulary that correspond to (other) semantic relationships. The former have onlyif semantic conditions and comprehension principles; the latter have ifandonlyif semantic conditions. The onlyif semantic conditions for the former are needed to prevent semantic paradoxes and other problems with the semantics. The comprehension principles for the former and the ifandonlyif semantic conditions for the latter are needed so that useful entailments are valid.
Conditions concerning the parts of the OWL universe and syntactic categories
If E is  then  Note  

S_{I}(E)∈  CEXT_{I}(S_{I}(E))=  and  
owl:Class  C_{I}  IOC  IOC⊆C_{I}  This defines IOC as the set of OWL classes. 
rdfs:Datatype  IDC  IDC⊆C_{I}  This defines IDC as the set of OWL datatypes.  
owl:Restriction  C_{I}  IOR  IOR⊆IOC  This defines IOR as the set of OWL restrictions. 
owl:Thing  IOC  IOT  IOT⊆R_{I}  This defines IOT as the set of OWL individuals. 
owl:Nothing  IOC  {}  
rdfs:Literal  IDC  LV_{I}  LV_{I}⊆R_{I}  
owl:ObjectProperty  C_{I}  IOOP  IOOP⊆P_{I}  This defines IOOP as the set of OWL individualvalued properties. 
owl:DatatypeProperty  C_{I}  IODP  IODP⊆P_{I}  This defines IODP as the set of OWL datatype properties. 
owl:AnnotationProperty  C_{I}  IOAP  IOAP⊆P_{I}  This defines IOAP as the set of OWL annotation properties. 
owl:OntologyProperty  C_{I}  IOXP  IOXP⊆P_{I}  This defines IOXP as the set of OWL ontology properties. 
owl:Ontology  C_{I}  IX  This defines IX as the set of OWL ontologies.  
owl:AllDifferent  C_{I}  IAD  
rdf:List  IL  IL⊆R_{I}  This defines IL as the set of OWL lists.  
rdf:nil  IL  
"l"^^d  CEXT_{I}(S_{I}(d))  S_{I}("l"^^d) ∈ LV_{I}  Typed literals are wellbehaved in OWL. 
OWL builtin syntactic classes and properties
I(owl:FunctionalProperty), I(owl:InverseFunctionalProperty), I(owl:SymmetricProperty), I(owl:TransitiveProperty), I(owl:DeprecatedClass), and I(owl:DeprecatedProperty) are in C_{I}.
I(owl:equivalentClass), I(owl:disjointWith), I(owl:equivalentProperty), I(owl:inverseOf), I(owl:sameAs), I(owl:differentFrom), I(owl:complementOf), I(owl:unionOf), I(owl:intersectionOf), I(owl:oneOf), I(owl:allValuesFrom), I(owl:onProperty), I(owl:someValuesFrom), I(owl:hasValue), I(owl:minCardinality), I(owl:maxCardinality), I(owl:cardinality), and I(owl:distinctMembers) are all in P_{I}.
I(owl:versionInfo), I(rdfs:label), I(rdfs:comment), I(rdfs:seeAlso), and I(rdfs:isDefinedBy) are all in IOAP. I(owl:imports), I(owl:priorVersion), I(owl:backwardCompatibleWith), and I(owl:incompatibleWith), are all in IOXP.
Characteristics of OWL classes, datatypes, and properties
If E is  then if e∈CEXT_{I}(S_{I}(E)) then  Note 

owl:Class  CEXT_{I}(e)⊆IOT  Instances of OWL classes are OWL individuals. 
rdfs:Datatype  CEXT_{I}(e)⊆LV_{I}  
owl:DataRange  CEXT_{I}(e)⊆LV_{I}  OWL dataranges are special kinds of datatypes. 
owl:ObjectProperty  EXT_{I}(e)⊆IOT×IOT  Values for indivdiualvalued properties are OWL individuals. 
owl:DatatypeProperty  EXT_{I}(e)⊆IOT×LV_{I}  Values for datatype properties are literal values. 
owl:AnnotationProperty  EXT_{I}(e)⊆IOT×(IOT∪LV_{I})  Values for annotation properties are less unconstrained. 
owl:OntologyProperty  EXT_{I}(e)⊆IX×IX  Ontology properties relate ontologies to other ontologies. 
If E is  then c∈CEXT_{I}(S_{I}(E)) iff c∈IOOP∪IODP and  Note 
owl:FunctionalProperty  <x,y_{1}>, <x,y_{2}> ∈ EXT_{I}(c) implies y_{1} = y_{2}  Both individualvalued and datatype properties can be functional properties. 
If E is  then c∈CEXT_{I}(S_{I}(E)) iff c∈IOOP and  Note 
owl:InverseFunctionalProperty  <x_{1},y>, <x_{2},y>∈EXT_{I}(c) implies x_{1} = x_{2}  Only individualvalued properties can be inverse functional properties. 
owl:SymmetricProperty  <x,y> ∈ EXT_{I}(c) implies <y, x>∈EXT_{I}(c)  Only individualvalued properties can be symmetric properties. 
owl:TransitiveProperty  <x,y>, <y,z>∈EXT_{I}(c) implies <x,z>∈EXT_{I}(c)  Only individualvalued properties can be transitive properties. 
Ifandonlyif conditions for rdfs:subClassOf, rdfs:subPropertyOf, rdfs:domain, and rdfs:range
If E is  then for  <x,y>∈EXT_{I}(S_{I}(E)) iff 

rdfs:subClassOf  x,y∈IOC  CEXT_{I}(x) ⊆ CEXT_{I}(y) 
rdfs:subPropertyOf  x,y∈IOOP  EXT_{I}(x) ⊆ EXT_{I}(y) 
rdfs:subPropertyOf  x,y∈IODP  EXT_{I}(x) ⊆ EXT_{I}(y) 
rdfs:domain  x∈IOOP∪IODP,y∈IOC  <z,w>∈EXT_{I}(x) implies z∈CEXT_{I}(y) 
rdfs:range  x∈IOOP∪IODP,y∈IOC∪IDC  <w,z>∈EXT_{I}(x) implies z∈CEXT_{I}(y) 
Characteristics of OWL vocabulary related to equivalence
If E is  then <x,y>∈EXT_{I}(S_{I}(E)) iff 

owl:equivalentClass  x,y∈IOC and CEXT_{I}(x)=CEXT_{I}(y) 
owl:disjointWith  x,y∈IOC and CEXT_{I}(x)∩CEXT_{I}(y)={} 
owl:equivalentProperty  x,y∈IOOP∪IODP and EXT_{I}(x) = EXT_{I}(y) 
owl:inverseOf  x,y∈IOOP and <u,v>∈EXT_{I}(x) iff <v,u>∈EXT_{I}(y) 
owl:sameAs  x = y 
owl:differentFrom  x ≠ y 
Conditions on OWL vocabulary related to boolean combinations and sets
We will say that l_{1} is a sequence of
y_{1},…,y_{n} over C iff
n=0 and l_{1}=S_{I}(rdf:nil)
or n>0 and l_{1}∈IL and
∃ l_{2}, …, l_{n} ∈ IL such that
<l_{1},y_{1}>∈EXT_{I}(S_{I}(rdf:first)), y_{1}∈C,
<l_{1},l_{2}>∈EXT_{I}(S_{I}(rdf:rest)), …,
<l_{n},y_{n}>∈EXT_{I}(S_{I}(rdf:first)), y_{n}∈C, and
<l_{n},S_{I}(rdf:nil)>∈EXT_{I}(S_{I}(rdf:rest)).
If E is  then <x,y>∈EXT_{I}(S_{I}(E)) iff 

owl:complementOf  x,y∈ IOC and CEXT_{I}(x)=IOTCEXT_{I}(y) 
owl:unionOf  x∈IOC and y is a sequence of y_{1},…y_{n} over IOC and CEXT_{I}(x) = CEXT_{I}(y_{1})∪…∪CEXT_{I}(y_{n}) 
owl:intersectionOf  x∈IOC and y is a sequence of y_{1},…y_{n} over IOC and CEXT_{I}(x) = CEXT_{I}(y_{1})∩…∩CEXT_{I}(y_{n}) 
owl:oneOf  x∈C_{I} and y is a sequence of y_{1},…y_{n} over IOT or over LV_{I} and CEXT_{I}(x) = {y_{1},..., y_{n}} 
Further conditions on owl:oneOf
If E is  and  then if <x,l>∈EXT_{I}(S_{I}(E)) then 

owl:oneOf  l is a sequence of y_{1},…y_{n} over LV_{I}  x∈IDC 
owl:oneOf  l is a sequence of y_{1},…y_{n} over IOT  x∈IOC 
Conditions on OWL restrictions
If  then x∈IOR, y∈IOC∪IDC, p∈IOOP∪IODP, and CEXT_{I}(x) = 

<x,y>∈EXT_{I}(S_{I}(owl:allValuesFrom))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) 
{u∈IOT  <u,v>∈EXT_{I}(p) implies v∈CEXT_{I}(y) } 
<x,y>∈EXT_{I}(S_{I}(owl:someValuesFrom))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) 
{u∈IOT  ∃ <u,v>∈EXT_{I}(p) such that v∈CEXT_{I}(y) } 
If  then x∈IOR, y∈IOT∪LV_{I}, p∈IOOP∪IODP, and CEXT_{I}(x) = 
<x,y>∈EXT_{I}(S_{I}(owl:hasValue))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) 
{u∈IOT  <u, y>∈EXT_{I}(p) } 
If  then x∈IOR, y∈LV_{I}, y is a nonnegative integer, p∈IOOP∪IODP, and CEXT_{I}(x) = 
<x,y>∈EXT_{I}(S_{I}(owl:minCardinality))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) 
{u∈IOT  card({v ∈ IOT ∪ LV : <u,v>∈EXT_{I}(p)}) ≥ y } 
<x,y>∈EXT_{I}(S_{I}(owl:maxCardinality))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) 
{u∈IOT  card({v ∈ IOT ∪ LV : <u,v>∈EXT_{I}(p)}) ≤ y } 
<x,y>∈EXT_{I}(S_{I}(owl:cardinality))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) 
{u∈IOT  card({v ∈ IOT ∪ LV : <u,v>∈EXT_{I}(p)}) = y } 
Comprehension conditions (principles)
The first two comprehension conditions require the existence of the finite sequences that are used in some OWL constructs. The third comprehension condition requires the existence of instances of owl:AllDifferent. The remaining comprehension conditions require the existence of the appropriate OWL descriptions and data ranges.
If there exists  then there exists l_{1},…,l_{n} ∈ IL with 

x_{1}, …, x_{n} ∈ IOC  <l_{1},x_{1}> ∈ EXT_{I}(S_{I}(rdf:first)),
<l_{1},l_{2}> ∈ EXT_{I}(S_{I}(rdf:rest)), … <l_{n},x_{n}> ∈ EXT_{I}(S_{I}(rdf:first)), <l_{n},S_{I}(rdf:nil)> ∈ EXT_{I}(S_{I}(rdf:rest)) 
x_{1}, …, x_{n} ∈ IOT∪LV_{I}  <l_{1},x_{1}> ∈ EXT_{I}(S_{I}(rdf:first)),
<l_{1},l_{2}> ∈ EXT_{I}(S_{I}(rdf:rest)), … <l_{n},x_{n}> ∈ EXT_{I}(S_{I}(rdf:first)), <l_{n},S_{I}(rdf:nil)> ∈ EXT_{I}(S_{I}(rdf:rest)) 
If there exists  then there exists y with 
l, a sequence of x_{1},…,x_{n} over IOT with x_{i}≠x_{j} for 1≤i<j≤n 
y∈IAD, <y,l>∈EXT_{I}(S_{I}(owl:distinctMembers)) 
If there exists  then there exists y with 
l, a sequence of x_{1},…,x_{n} over IOC  y∈IOC, <y,l> ∈ EXT_{I}(S_{I}(owl:unionOf)) 
l, a sequence of x_{1},…,x_{n} over IOC  y∈IOC, <y,l> ∈ EXT_{I}(S_{I}(owl:intersectionOf)) 
l, a sequence of x_{1},…,x_{n} over IOT  y∈IOC, <y,l> ∈ EXT_{I}(S_{I}(owl:oneOf)) 
l, a sequence of x_{1},…,x_{n} over LV_{I}  y∈IDC, <y,l> ∈ EXT_{I}(S_{I}(owl:oneOf)) 
If there exists  then there exists y ∈ IOC with 
x ∈ IOC  <y,x> ∈ EXT_{I}(S_{I}(owl:complementOf)) 
If there exists  then there exists y ∈ IOR with 
x ∈ IOOP∪IODP ∧ w ∈ IOC ∪ IDC  <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:allValuesFrom)) 
x ∈ IOOP∪IODP ∧ w ∈ IOC ∪ IDC  <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:someValuesFrom)) 
x ∈ IOOP∪IODP ∧ w ∈ IOT ∪ LV_{I}  <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:hasValue)) 
x ∈ IOOP∪IODP ∧ w ∈ LV_{I} ∧ w is a nonnegative integer  <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:minCardinality)) 
x ∈ IOOP∪IODP ∧ w ∈ LV_{I} ∧ w is a nonnegative integer  <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:maxCardinality)) 
x ∈ IOOP∪IODP ∧ w ∈ LV_{I} ∧ w is a nonnegative integer  <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:cardinality)) 
OWL Full augments the common conditions with conditions that force the parts of the OWL universe to be the same as their analogues in RDF. These new conditions strongly interact with the common conditions. For example, because in OWL Full IOT is the entire RDF domain of discourse, the second comprehension condition for lists generates lists of any kind, including lists of lists.
Definition: A OWL Full interpretation of a vocabulary V is an OWL interpretation as above that satisfies the following conditions.
IOT = R_{I} 
IOOP = P_{I} 
IOC = C_{I} 
Definition: 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 the result of the RDF processing of the RDF/XML document, if any, accessible at u into an RDF graph. The imports closure of a collection of RDF graphs is the smallest importclosed collection of RDF graphs containing the graphs.
Definitions: Let K and Q be collections of RDF graphs. Then K OWL Full entails Q iff every OWL Full interpretation (of any vocabulary V that includes the RDF and RDFS vocabularies and the OWL vocabulary) that satisfies all the RDF graphs in K also satisfies all the RDF graphs in Q. K is OWL Full consistent iff there is some OWL Full interpretation that satisfies all the RDF graphs in K.
OWL DL augments the above conditions with a separation of the domain of discourse into several disjoint parts. This separation has two consequences. First, the OWL portion of the domain of discourse becomes standard firstorder, in that predicates (classes and properties) and individuals are disjoint. Second, the OWL portion of a OWL DL interpretation can be viewed as a Description Logic interpretation for a particular expressive Description Logic.
Definition: A OWL DL interpretation of a vocabulary V is an OWL interpretation as above that satisfies the following conditions.
LV_{I}, IOT, IOC, IDC, IOOP, IODP, IOAP, IOXP, IL, and IX are all pairwise disjoint. 
For v in the disallowed vocabulary (Section 4.2), S_{I}(v) ∈ R_{I}  (LV_{I}∪IOT∪IOC∪IDC∪IOOP∪IODP∪IOAP∪IOXP∪IL∪IX). 
Entailment in OWL DL is defined similarly to entailment in OWL Full.
Definitions: Let K and Q be collections of RDF graphs. Then K OWL DL entails Q iff every OWL DL interpretation (of any vocabulary V that includes the RDF and RDFS vocabularies and the OWL vocabulary) that satisfies all the RDF graphs in K also satisfies all the RDF graphs in Q. K is OWL DL consistent iff there is some OWL DL interpretation that satisfies all the RDF graphs in K.
There is a strong correspondence between the direct semantics and the OWL DL semantics. Basically, an ontology that could be written in the abstract syntax OWL DL entails another exactly when it entails the other in the direct semantics. There are a number of complications to this basic story having to do with splitting up the vocabulary so that, for example, concepts, properties, and individuals do not interfere, and arranging that imports works the same.
For the correspondence to be valid there has to be some connection between an ontology in the abstract syntax with a particular name and the document available on the Web at that URI. This connection is outside the semantics here, and so must be specially arranged. This connection is also only an idealization of the Web, as it ignores temporal and transport aspects of the Web.
Definition: Let T be the mapping from OWL ontologies in the abstract syntax to RDF graphs from Section 4.1. Let O be a collection of OWL DL ontologies in abstract syntax form. O is said to be imports closed iff for any URI, u, in an imports directive in any ontology in O the RDF parsing of the document accessible on the Web at u results in T(K), where K is the ontology in O with name u.
Theorem 1:
Let O and O' be collections of OWL DL ontologies in abstract syntax form
that are imports closed,
such that their union has a
separated vocabulary
(Section 4.2).
Then
O entails O'
if and only if
the translation (Section 4.1) of the ontologies in O
OWL DL entails
the translation of the ontologies in O'.
The proof is contained in Appendix A.1.
A simple corollary of this is that O is consistent if and only if the translation of the ontologies in O is consistent.
There is also a correspondence between OWL DL entailment and OWL Full entailment.
Theorem 2: Let O and O' be collections of OWL DL ontologies in abstract syntax form that are imports closed, such that their union has a separated vocabulary (Section 4.2). Then the translation of the ontologies in O OWL Full entails the translation of the ontologies in O' if the translation of the ontologies in O OWL DL entails the translation of the ontologies in O'. A sketch of the proof is contained in Appendix A.2.
This appendix contains proofs of theorems contained in Section 5 of the document.
This section shows that the two semantics, the direct model theory for abstract OWL ontologies from Section 3, here called the direct model theory, and the OWL DL semantics from Section 5, here called the OWL DL model theory, correspond on certain OWL ontologies.
Nomenclature: Throughout this section D will be a datatype theory (Section 3.1) containing datatypes for all the builtin OWL datatypes; T will be the mapping from abstract OWL ontologies to RDF graphs from Section 4.1; and VB will be the builtin OWL vocabulary.
Definition: Given D as above, a separated OWL vocabulary (Section 4.2) is here further formalized into a set of URI references V', disjoint from the disallowed vocabulary (Section 4.2), with a disjoint partition of V', written as V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP, where the builtin OWL classes are in VC, the URI references all the datatype names of D and rdfs:Literal are in VD, the OWL builtin annotation properties are in VAP, and the OWL builtin ontology properties are in VXP.
Definition:
The translation of a separated OWL vocabulary,
V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP,
written T(V'), consists of all the triples of the form
v rdf:type owl:Ontology .
for v ∈ VO,
v rdf:type owl:Class .
for v ∈ VC,
v rdf:type rdfs:Datatype .
for v ∈ VD,
v rdf:type owl:Thing .
for v ∈ VI,
v rdf:type owl:ObjectProperty .
for v ∈ VOP,
v rdf:type owl:DatatypeProperty .
for v ∈ VDP,
v rdf:type owl:AnnotationProperty .
for v ∈ VAP, and
v rdf:type owl:OntologyProperty .
for v ∈ VXP.
Definition: A collection of OWL DL ontologies in abstract syntax form, O, (Section 2) with a separated vocabulary (Section 4) is here further formalized with the new notion of a separated vocabulary V = VO + VC + VD + VI + VOP + VDP + VAP + VXP, as follows:
The theorem to be proved is then: Let O and O' be collections of OWL DL ontologies in abstract syntax form that are imports closed, such that their union has a separated vocabulary. Then O direct entails O' if and only if T(O) OWL DL entails T(O') the translation of the ontologies in O' (exending T to allow it to translate collections of ontologies in the obvious way).
Lemma 1: Let V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP be a separated OWL vocabulary. Let V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VB. Let I'= <R,EC,ER,L,S,LV> be a direct interpretation of V'. Let I = <R_{I},P_{I},EXT_{I},S_{I},L_{I},LV_{I}> be a OWL DL interpretation of V that satisfies T(V'), with LV_{I} = LV. Let CEXT_{I} have its usual meaning, and, as usual, overload I to map any syntactic construct into its denotation. If
then for d any abstract OWL description or data range over V',
Proof:
The proof of the lemma is by a structural induction. Throughout the proof, let IOT = CEXT_{I}(I(owl:Thing)), IOC = CEXT_{I}(I(owl:Class)), IDC = CEXT_{I}(I(rdfs:Datatype)), IOOP = CEXT_{I}(I(owl:ObjectProperty)), IODP = CEXT_{I}(I(owl:DatatypeProperty)), and IL = CEXT_{I}(I(rdf:List)).
To make the induction work, it is necessary to show that for any d a description or data range with subconstructs T(d) contains triples for each of the subconstructs that do not share any blank nodes with triples from the other subconstructs. This can easily be verified from the rules for T.
If p∈VOP then I satisfies p∈IOOP. Then, as I is an OWL DL interpretation, I satisfies <p,I(owl:Thing)>∈EXT_{I}(I(rdfs:domain)) and <p,I(owl:Thing)>∈EXT_{I}(I(rdfs:range)). Thus I satisfies T(p). Similarly for p∈VDP.
Lemma 1.1: Let V', V, I', and I be as in Lemma 1. Let d be an abstract OWL individual construct over V', (of the form Individual(…)). Then for any A mapping all the blank nodes of T(d) into R_{I} where I+A OWL DL satisfies T(d), I+A(M(T(d))) ∈ EC(d). Also, for any r ∈ EC(d) there is some A mapping all the blank nodes of T(d) into R_{I} such that I+A(M(T(d))) = r.
Proof:
A simple inductive argument shows that I+A(M(T(d))) must satisfy all the requirements of EC(d). Another inductive argument, depending on the nonsharing of blank nodes in subconstructs, shows that for each r ∈ EC(d) there is some A such that I+A(M(T(d))) = r.
Lemma 1.9: Let V', V, I', and I be as in Lemma 1. Let F be an OWL directive over V' with an annotation of the form annotation(p x). If F is a class or property axiom, let n be the name of the class or property. If F is an individual axiom, let n be the main node of T(F). Then for any A mapping all the blank nodes of T(F) into R_{I}, I+A OWL DL satisfies the triples resulting from the annotation iff I' direct satisfies the conditions resulting from the annotation.
Proof:
For annotations to URI references, the lemma can be easily established by an inspection of the semantic condition and the translation triples. For annotations to Individual(…), the use of Lemma 1.1 is also needed.
Lemma 2: Let V', V, I', and I be as in Lemma 1. Let F be an OWL directive over V'. Then I satisfies T(F) iff I' satisfies F.
Proof:
The main part of the proof is a structural induction over directives. Annotations occur in many directives and work exactly the same so they just require a use of Lemma 1.9. The rest of the proof will thus ignore annotations. Deprecations can be handled in a simlar fashion and will also be ignored in the rest of the proof.
Let d=intersectionOf(d_{1} … d_{n}). As d is a description over V', thus I satisfies T(d) and for any A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXT_{I}(I+A(M(T(d)))) = EC(d). Thus for any subdescription of d, d', CEXT_{I}(I+A(M(T(d')))) = EC(d'), and I+A(M(T(d')))∈IOC. Thus for some A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXT_{I}(I+A(M(T(d)))) = EC(d) and I+A(M(T(d)))∈IOC; and for each d' a subdescription of d, CEXT_{I}(I+A(M(T(d')))) = EC(d'), and I+A(M(T(d')))∈IOC.
If I' satisfies F then EC(foo) = EC(d). From above, there is some A such that CEXT_{I}(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXT_{I}(I(foo)) and I+A(M(T(d)))∈IOC. Because I satisfies T(V), I(foo)∈IOC, thus <I(foo),I+A(M(T(d)))> ∈ EXT_{I}(I(owl:equivalentClass)). Further, because of the semantic conditions on I(owl:intersectionOf), <I(foo),I+A(M(T(SEQ d_{1} … d_{n})))> ∈ EXT_{I}(I(owl:intersectionOf)).
If d is of the form intersectionOf(d_{1}) then CEXT_{I}(I+A(M(T(d_{1})))) = EC(d_{1}) = EC(d) = EC(foo) and I+A(M(T(d_{1})))∈IOC. So, from the semantic conditions on I(owl:equivalentClass), <I(foo),I+A(M(T(d_{1})))> ∈ EXT_{I}(I(owl:equivalentClass)). If d_{1} is of the form complementOf(d'_{1}) then IOT  CEXT_{I}(I+A(M(T(d'_{1})))) = CEXT_{I}(I+A(M(T(d_{1})))) = EC(d_{1}) = EC(d) = EC(foo) and I+A(M(T(d'_{1})))∈IOC. So, from the semantic conditions on I(owl:complementOf), <I(foo),I+A(M(T(d'_{1})))> ∈ EXT_{I}(I(owl:complementOf)). If d_{1} is of the form unionOf(d_{11} … d_{1m}) then CEXT_{I}(I+A(M(T(d_{11})))) ∪ … ∪ CEXT_{I}(I+A(M(T(d_{1m})))) = CEXT_{I}(I+A(M(T(d_{1})))) = EC(d_{1}) = EC(d) = EC(foo) and I+A(M(T(d_{1j})))∈IOC, for 1≤ j ≤ m. So, from the semantic conditions on I(owl:unionOf), <I(foo),I+A(M(T(SEQ d_{11} … d_{1m})))> ∈ EXT_{I}(I(owl:unionOf)).
Therefore I satisfies T(F), for each potential T(F).
If I satisfies T(F) then I satisfies T(intersectionOf(d_{1} … d_{n})). Thus there is some A as above such that <I(foo),I+A(M(T(d)))> ∈ EXT_{I}(I(owl:equivalentClass)). Thus EC(d) = CEXT_{I}(I+A(M(T(d)))) = CEXT_{I}(I(foo)) = EC(foo). Therefore I' satisfies F.
Let d=intersectionOf(d_{1} … d_{n}). As d is a description over V', thus I satisfies T(d) and for any A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXT_{I}(I+A(M(T(d)))) = EC(d). Thus CEXT_{I}(I+A(M(T(d_{i})))) = EC(d_{i}), for 1 ≤ i ≤ n. Thus for some A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXT_{I}(I+A(M(T(d_{i})))) = EC(d_{i}), and I+A(M(T(d_{i}))∈IOC, for 1 ≤ i ≤ n.
If I' satisfies F then EC(foo) ⊆ EC(d_{i}), for 1 ≤ i ≤ n. From above, there is some A such that CEXT_{I}(I+A(M(T(d_{i})))) = EC(d_{i}) ⊇ EC(foo) = CEXT_{I}(I(foo)) and I+A(M(T(d_{i}))∈IOC. Because I satisfies T(V), I(foo)∈IOC, thus <I(foo),I+A(M(T(d_{i})))> ∈ EXT_{I}(I(rdfs:subClassOf)), for 1 ≤ i ≤ n. Therefore I satisfies T(F).
If I satisfies T(F) then I satisfies T(d_{i}), for 1 ≤ i ≤ n. Thus there is some A as above such that <I(foo),I+A(M(T(d_{i})))> ∈ EXT_{I}(I(rdfs:subClassOf)), for 1 ≤ i ≤ n. Thus EC(d) = CEXT_{I}(I+A(M(T(d_{i})))) ⊇ CEXT_{I}(I(foo)) = EC(foo), for 1 ≤ i ≤ n. Therefore I' satisfies F.
Let d=oneOf(i_{1} … i_{n}). As d is a description over V' so I satisfies T(d) and for some A mapping the blank nodes of T(d) such that I+A satisfies T(d), EC(d) = CEXT_{I}(I+A(M(T(d)))) = {S_{I}(M(T(i_{1})), … S_{I}(M(T(i_{n}))} Also, S_{I}(M(T(i_{j})) ∈ IOT, for 1 ≤ j ≤ n.
If I' satisfies F then EC(foo) = EC(d). From above, there is some A such that CEXT_{I}(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXT_{I}(I(foo)) and I+A(M(T(d))∈IOC. Let e be I+A(M(T(SEQ i_{1} … i_{n}))). Then, from the semantic conditions on I(owl:oneOf), <I(foo),e> ∈ EXT_{I}(I(owl:oneOf)). Therefore I satisfies T(F).
If I satisfies T(F) then I satisfies T(SEQ i_{1} … i_{n}). Thus there is some A as above such that <I(foo),I+A(M(T(SEQ i_{1} … i_{n})))> ∈ EXT_{I}(I(owl:oneOf)). Thus {S_{I}(M(T(i_{1})), …, S_{I}(M(T(i_{n}))} = CEXT_{I}(I(foo)) = EC(foo). Therefore I' satisfies F.
The only thing that needs to be shown here is the typing for foo, which is similar to that for classes.
As d_{i} is a description over V' therefore I satisfies T(d_{i}) and for any A mapping the blank nodes of T(d_{i}) such that I+A satisfies T(d_{i}), CEXT_{I}(I+A(M(T(d_{i})))) = EC(d_{i}).
If I satisfies T(F) then for 1≤i≤n there is some A_{i} such that I satisfies <I+A_{i}(M(T(d_{i}))),I+A_{j}(M(T(d_{j})))> ∈ EXT_{I}(I(owl:disjointWith)) for each 1≤i<j≤n. Thus EC(d_{i})∩EC(d_{j}) = {}, for i≠j. Therefore I' satisfies F.
If I' satisfies F then EC(d_{i})∩EC(d_{j}) = {} for i≠j. For any A_{i} and A_{j} as above <I+A_{i}+A_{j}(M(T(d_{i}))),I+A_{i}+A_{j}(M(T(d_{j})))> ∈ EXT_{I}(I(owl:disjointWith)), for i≠j. As at least one A_{i} exists for each i, and the blank nodes of the T(d_{j}) are all disjoint, I+A_{1}+…+A_{n} satisfies T(DisjointClasses(d_{1} … d_{n})). Therefore I satisfies T(F).
As d_{i} for 1≤i≤m is a description over V' therefore I satisfies T(d_{i}) and for any A mapping the blank nodes of T(d_{i}) such that I+A satisfies T(d_{i}), CEXT_{I}(I+A(M(T(d_{i})))) = EC(d_{i}). Similarly for r_{i} for 1≤i≤k.
If I' satisfies F, then, as p∈VOP, I satisfies I(p)∈IOOP. Then, as I is an OWL DL interpretation, I satisfies <I(p),I(owl:Thing)>∈EXT_{I}(I(rdfs:domain)) and <I(p),I(owl:Thing)>∈EXT_{I}(I(rdfs:range)). Also, ER(p)⊆ER(s_{i}) for 1≤i≤n, so EXT_{I}(I(p))=ER(p) ⊆ ER(s_{i})=EXT_{I}(I(s_{i})) and I satisfies <I(p),I(s_{i})>∈EXT_{I}(I(rdfs:subPropertyOf)). Next, ER(p)⊆EC(d_{i})×R for 1≤i≤m, so <z,w>∈ER(p) implies z∈EC(d_{i}) and for any A such that I+A satisfies T(d_{i}), <z,w>∈EXT_{I}(p) implies z∈CEXT_{I}(I+A(M(T(d_{i})))) and thus <I(p),I+A(M(T(d_{i})))>∈EXT_{I}(I(rdfs:domain)). Similarly for r_{i} for 1≤i≤k.
If I' satisfies F and inverse(i) is in F, then ER(p) and ER(i) are converses. Thus <u,v>∈ER(p) iff <v,u>∈ER(i) so <u,v>∈EXT_{I}(p) iff <v,u>∈EXT_{I}(i) and I satisfies <I(p),I(i)>∈EXT_{I}(I(owl:inverseOf)). If I' satisfies F and Symmetric is in F, then ER(p) is symmetric. Thus if <x,y>∈ ER(p) then <y,x>∈ER(p) so if <x,y> ∈ EXT_{I}(p) then <y, x>∈EXT_{I}(p). and thus I satisfies p∈CEXT_{I}(I(owl:Symmetric)). Similarly for Functional, InverseFunctional, and Transitive. Thus if I' satisfies F then I satisfies T(F).
If I satisfies T(F) then, for 1≤i≤n, <I(p),I(s_{i})>∈EXT_{I}(I(rdfs:subPropertyOf)) so ER(p)=EXT_{I}(I(p)) ⊆ EXT_{I}(I(s_{i}))=ER(s_{i}). Also, for 1≤i≤m, for some A such that I+A satisfies T(d_{i}), <I(p),I+A(M(T(d_{i})))>∈EXT_{I}(I(rdfs:domain)) so <z,w>∈EXT_{I}(p) implies z∈CEXT_{I}(I+A(M(T(d_{i})))). Thus <z,w>∈ER(p) implies z∈EC(d_{i}) and ER(p)⊆EC(d_{i})×R. Similarly for r_{i} for 1≤i≤k.
If I satisfies T(F) and inverse(i) is in F, then I satisfies <I(p),I(i)>∈EXT_{I}(I(owl:inverseOf)). Thus <u,v>∈EXT_{I}(p) iff <v,u>∈EXT_{I}(i) so <u,v>∈ER(p) iff <v,u>∈ER(i) and ER(p) and ER(i) are converses. If I satisfies F and Symmetric is in F, then I satisfies p∈CEXT_{I}(I(owl:Symmetric)) so if <x,y> ∈ EXT_{I}(p) then <y, x>∈EXT_{I}(p). Thus if <x,y>∈ ER(p) then <y,x>∈ER(p) and ER(p) is symmetric. Similarly for Functional, InverseFunctional, and Transitive. Thus if I satisfies T(F) then I' satisfies F.
As p_{i}∈VOP and I satisfies T(V'), I(p_{i})∈IOOP. If I satisfies T(F) then <I(p_{i}),I(p_{j})> ∈ EXT_{I}(I(owl:equivalentProperty)), for each 1≤i<j≤n. Therefore EXT_{I}(p_{i}) = EXT_{I}(p_{j}), for each 1≤i<j≤n; ER(p_{i}) = ER(p_{j}), for each 1≤i<j≤n; and I' satisfies F.
If I' satisfies F then ER(p_{i}) = ER(p_{j}), for each 1≤i<j≤n. Therefore EXT_{I}(p_{i}) = EXT_{I}(p_{j}), for each 1≤i<j≤n. From the OWL DL definition of owl:equivalentProperty, <I(p_{i}),I(p_{j})> ∈ EXT_{I}(I(owl:equivalentProperty)), for each 1≤i<j≤n. Thus I satisfies T(F).
If I satisfies T(F) then there is some A that maps each blank node in T(F) such that I+A satisfies T(F). A simple examination of T(F) shows that the mappings of A plus the mappings for the individual IDs in F, which are all in IOT, show that I' satisfies F.
If I' satisfies F then for each Individual construct in F there must be some element of R that makes the type relationships and relationships true in F. The triples in T(F) then fall into three categories. 1/ Type relationships to owl:Thing, which are true in I because the elements above belong to R. 2/ Type relationships to OWL descriptions, which are true in I because they are true in I', from Lemma 1. 3/ OWL property relationships, which are true in I' because they are true in I. Thus I satisfies T(F).
Lemma 3: Let V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP be a separated OWL vocabulary. Let V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VB. Then for every OWL DL interpretation I = <R_{I},P_{I},EXT_{I},S_{I},L_{I},LV_{I}> of V that satisfies T(V') there is an direct interpretation I' of V' such that for any collection of OWL abstract ontologies O with vocabulary V' such that O is imports closed, I' direct satisfies O iff I OWL DL satisfies T(O).
Proof:
Let CEXT_{I} be defined as usual from I. The required direct interpretation will be I' = < R_{I}, EC, ER, L, S, LV_{I} > where
V', V, I', and I meet the requirements of Lemma 2, so for any directive D over V' I satisfies T(D) iff I' satisfies D.
Because O is imports closed, O includes all the ontologies that would be imported in T(O) the importing part of imports directives will be handled the same. Satisfying an abstract ontology is just satisfying its directives and satisfying the translation of an abstract ontology is just satisfying all the triples so I OWL DL satisfies T(K) iff I' direct satisfies K.
Lemma 4: Let V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP be a separated OWL vocabulary. Let V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VB. Then for every direct interpretation I' = < U, EC, ER, L, S, LV > of V' there is an OWL DL interpretation I of V that satisfies T(V') such that for any collection of OWL abstract ontologies O with vocabulary V' such that O is imports closed, I' direct satisfies O iff I OWL DL satisfies T(O).
Proof:
Construct I = < R_{I}, P_{I}, EXT_{I}, S_{I}, L, LV_{I} > as follows:
Then I is an OWL DL interpretation because the conditions for the class extensions in OWL DL match up with the conditions for classlike OWL abstract syntax constructs.
V', V, I', and I meet the requirements of Lemma 2, so for any directive D over V' I satisfies T(D) iff I' satisfies D.
Because O is imports closed, O includes all the ontologies that would be imported in T(O) the importing part of imports directives will be handled the same. Satisfying an abstract ontology is just satisfying its directives and satisfying the translation of an abstract ontology is just satisfying all the triples so I OWL DL satisfies T(K) iff I' direct satisfies K.
Theorem 1: Let O and O' be collections of OWL DL ontologies in abstract syntax form that are imports closed, such that their union has a separated vocabulary, V', and every URI reference in V' is used in O. Then O entails O' if and only if T(O) OWL DL entails T(O') the translation of the ontologies in O' (exending T to allow it to translate collections of ontologies in the obvious way).
Then I satisfies T(V'), because each URI reference in V' is used on O.
Proof: Suppose O entails O'. Let I be an OWL DL interpretation that satisfies T(O). Then from Lemma 3, there is some direct interpretation I' such that for any abstract OWL ontology X over V', I satisfies T(X) iff I' satisfies X. Thus I' satisfies each ontology in O. Because O entails O', I' satisfies O', so I satisfies T(O'). Thus T(K),T(V') OWL DL entails T(Q).
Suppose T(O) OWL DL entails T(O'). Let I' be an direct interpretation that satisfies K. Then from Lemma 4, there is some OWL DL interpretation I such that for any abstract OWL ontology X over V', I satisfies T(X) iff I' satisfies X. Thus I satisfies T(O). Because T(O) OWL DL entails T(O'), I satisfies T(O'), so I' satisfies O'. Thus O entails O'.
This section contains a proof sketch concerning the relationship between OWL DL and OWL Full. This proof has not been fully worked out. Significant effort may be required to finish the proof and some details of the relationship may have to change.
Let K be an RDF graph. An OWL interpretation of K is an OWL interpretation (from Section 5.2) that is an Dinterpretation of K.
Lemma 5: Let V be a separated vocabulary. Then for every OWL intepretation I there is an OWL DL interpretation I' (as in Section 5.3) such that for K any OWL ontology in the abstract syntax with separated vocabulary V, I is an OWL interpretation of T(K) iff I' is an OWL DL interpretation of T(K).
Proof sketch: As all OWL DL interpretations are OWL interpretations, the reverse direction is obvious.
Let I = < R_{I}, EXT_{I}, S_{I}, L_{I} > be an OWL interpretation that satisfies T(K). Let I' = < R_{I'}, EXT_{I'}, S_{I'}, L_{I'} > be an OWL interpretation that satisfies T(K). Let R_{I'} = CEXT_{I}(I(owl:Thing)) + CEXT_{I}(I(owl:ObjectProperty)) + CEXT_{I}(I(owl:ObjectProperty)) + CEXT_{I}(I(owl:Class)) + CEXT_{I}(I(rdf:List)) + R_{I}, where + is disjoint union. Define EXT_{I'} so as to separate the various roles of the copies. Define S_{I'} so as to map vocabulary into the appropriate copy. This works because K has a separated vocabulary, so I can be split according the the roles, and there are no inappropriate relationships in EXT_{I}. In essence the first component of R_{I'} is OWL individuals, the second component of R_{I'} is OWL datatype properties, the third component of R_{I'} is OWL individualvalued properties, the fourth component of R_{I'} is OWL classes, the fifth component of R_{I'} is RDF lists, and the sixth component of R_{I'} is everything else.
Theorem 2: Let O and O' be collections of OWL DL ontologies in abstract syntax form that are imports closed, such that their union has a separated vocabulary (Section 4.2). Then the translation of the ontologies in O OWL Full entails the translation of the ontologies in O' if the translation of the ontologies in O OWL DL entails the translation of the ontologies in O'.
Proof: From the above lemma and because all OWL Full interpretations are OWL interpretations.
Note: The only if direction is not true.
This appendix gives examples of the concepts developed in the rest of the document.
The transformation rules in Section 4 can transform the ontology
Ontology(ex:ontology DatatypeProperty(ex:name) ObjectProperty(ex:author) Class(ex:Book) Class(ex:Person) Individual(type(ex:Book) value(ex:author Individual(type(ex:Person) value(ex:name "Fred"^^xsd:string)))))
to
ex:ontology rdf:type owl:Ontology . ex:name rdf:type owl:DatatypeProperty . ex:author rdf:type owl:ObjectProperty . ex:Book rdf:type owl:Class . ex:Person rdf:type owl:Class . _:x rdf:type ex:Book . _:x ex:author _:x1 . _:x1 rdf:type ex:Person . _:x1 ex:name "Fred"^^xsd:string .
and
Ontology(ex:ontology2 Class(ex:Person) Class(ex:Student) ObjectProperty(ex:enrolledIn) Class(ex:Student complete ex:Person restriction(ex:enrolledIn allValuesFrom(ex:School) minCardinality(1))))
can be transformed to
ex:ontology2 rdf:type owl:Ontology . ex:enrolledIn rdf:type owl:ObjectProperty . ex:Person rdf:type owl:Class . ex:School rdf:type owl:Class . ex:Student rdf:type owl:Class . ex:Student owl:equivalentClass _:x . _:x owl:intersectionOf _:l1 . _:l1 rdf:first ex:Person . _:l1 rdf:rest _:l2 . _:l2 rdf:first _:lr . _:l2 rdf:rest rdf:nil . _:lr owl:intersectionOf _:lr1 . _:lr1 rdf:first _:r1 . _:lr1 rdf:rest _:lr2 . _:lr2 rdf:first _:r2 . _:lr2 rdf:rest rdf:nil . _:r1 rdf:type owl:Restriction . _:r1 owl:onProperty ex:enrolledIn . _:r1 owl:allValuesFrom ex:School . _:r2 rdf:type owl:Restriction . _:r2 owl:onProperty ex:enrolledIn . _:r2 owl:minCardinality "1"^^xsd:nonNegativeInteger .
OWL DL supports the entailments that one would expect, as long as the vocabulary can be shown to belong to the appropriate piece of the domain of discourse. For example,
John friend Susan .
does not OWL DL entail
John rdf:type owl:Thing .
Susan rdf:type owl:Thing .
friend rdf:type owl:ObjectProperty .
The above three triples would have to be added before the following restriction could be concluded
John rdf:type _:x .
_:x owl:onProperty friend .
_:x owl:minCardinality "1"^^xsd:nonNegativeInteger .
However, once this extra information is added, all natural entailments follow, except for those that involve descriptions with loops. For example,
John rdf:type owl:Thing .
friend rdf:type owl:ObjectProperty .
John rdf:type _:x .
_:x owl:onProperty friend .
_:x owl:maxCardinality "0"^^xsd:nonNegativeInteger .
does not entail
John rdf:type _:y .
_:y owl:onProperty friend .
_:y owl:allValuesFrom _:y .
because there are no comprehension principles for such looping descriptions. It is precisely the lack of such comprehension principles that prevent the formation of paradoxes in OWL DL while still retaining natural entailments.
In OWL DL one can repair missing localizations in any separatedsyntax KB by adding a particular set of localizing assertions consisting of all triples of the form
<individual> rdf:type owl:Thing .
<class> rdf:type owl:Class .
<oproperty> rdf:type owl:ObjectProperty .
<dtproperty> rdf:type owl:DatatypeProperty .
Call the result of adding all such assertions to a OWL DL KB the localization of the KB.
OWL Full supports the entailments that one would expect, and there is no need to provide typing information for the vocabulary. For example,
John friend Susan .
does OWL Full entail
John rdf:type _:x .
_:x owl:onProperty friend .
_:x owl:minCardinality "1"^^xsd:nonNegativeInteger .
This appendix provides an informative account of the changes from the lastcall version of this document. Postlast call changes to the document, except for some minor changes to fix formatting, etc., are indicated in the style of this appendix.
This section provides information on the changes to the document that make changes to the specification of OWL.
This section provides information on editorial changes to the document, i.e., changes that do not affect the specification of OWL.
The following table provides pointers to information about each element of the OWL vocabulary, as well as some elements of the RDF and RDFS vocabularies. The first column points to the vocabulary element's major definition in the abstract syntax of Section 2. The second column points to the vocabulary element's major definition in the OWL Lite abstract syntax. The third column points to the vocabularly element's major definition in the direct semantics of Section 3. The fourth column points to the major piece of the translation from the abstract syntax to triples for the vocabulary element Section 4. The fifth column points to the vocabularly element's major definition in the RDFScompatible semantics of Section 5.
The Joint US/EU ad hoc Agent Markup Language Committee developed DAML+OIL, which is the direct precursor to OWL. Many of the ideas in DAML+OIL and thus in OWL are also present in the Ontology Inference Layer (OIL). Many of the other members of the W3C Web Ontology Working Group have had substantial input into this document.
This document is the result of extensive discussions within the Web Ontology Working Group as a whole. The members of this group working group included: Yasser al Safadi, JeanFrancois Baget, James Barnette, Sean Bechhofer, Jonathan Borden, Frederik Brysse, Stephen Buswell, Jeremy Carroll, Dan Connolly, Peter Crowther, Jonathan Dale, Jos De Roo, David De Roure, Mike Dean, Larry Eshelman, Jerome Euzenat, Dieter Fensel, Tim Finin, Nicholas Gibbins, Pat Hayes, Jeff Heflin, Ziv Hellman, James Hendler, Bernard Horan, Masahiro Hori, Ian Horrocks, Francesco Iannuzzelli, Mario Jeckle, Ruediger Klein, Natasha Kravtsova, Ora Lassila, Alexander Maedche, Massimo Marchiori, Deborah McGuinness, Libby Miller, Enrico Motta, Leo Obrst, Laurent Olivry , Peter PatelSchneider, Martin Pike, Marwan Sabbouh, Guus Schreiber, Shimizu Noboru, Michael Sintek, Michael Smith, Ned Smith, John Stanton, Lynn Andrea Stein, Herman ter Horst, Lynne R. Thompson, David Trastour, Frank van Harmelen, Raphael Volz, Evan Wallace, Christopher Welty, Charles White, and John Yanosy.