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 high-level abstract syntax for both OWL DL and OWL Lite, sublanguages of OWL. A model-theoretic semantics is given to provide a formal meaning for OWL ontologies written in this abstract syntax. A model-theoretic semantics in the form of an extension to the RDF model theory 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 is a W3C Web Ontology Working Group Working Draft produced 3 February 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 public W3C Working Draft and may be updated, replaced, or obsoleted by other documents at any time. However, it is expected that this working draft is quite close to the Last Call version of the document. It is inappropriate to use W3C Working Drafts as reference material or to cite as other than "work in progress". A list of current W3C Recommendations and other technical documents can be found at http://www.w3.org/TR/.
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 public-webont-comments@w3.org. An archive of comments is available at http://lists.w3.org/Archives/Public/public-webont-comments/ .
This document contains several interrelated 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 high-level, 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 model-theoretic semantics for OWL ontologies written in the abstract syntax. The other, defined in Section 5, is a vocabulary extension of the RDF model-theoretic 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 RDFS-compatible 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. For such OWL ontologies the direct model theory is authoritative and the RDFS-compatible model theory is secondary. Appendix A also contains the sketch of a proof that the entailments in the RDFS-compatible semantics for OWL Full include all the entailments in the RDFS-compatible 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 language described in this document is very close to the DAML+OIL web ontology language [DAML+OIL]. The only substantive changes between OWL and DAML+OIL are
There are also a number of minor differences between OWL and DAML+OIL, including a number of changes to the names of the various constructs, as mentioned in Appendix A of the OWL Reference Description [OWL Reference].
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 DAM+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.
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 RDFS-compatible semantics of Section 5.
The description of OWL in this Section abstracts from concrete syntax and thus facilitates access to and evaluation of the language. A high-level syntax is used to make the language features easier to see. This particular syntax has a frame-like 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; non-terminals are 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.
The meaning of each construct in the abstract syntax is described when it is introduced. The formal meaning of these constructs is given in Section 3 via a model-theoretic 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 Features]. This smaller language also attempts to describe a useful language that provides more than RDF Schema [RDF Schema] with the goal of adding functionality that is important in order to support web applications. 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 self-referential 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.
OWL uses some of the facilities of XML Schema. [XML Schema Datatypes]. The following built-in non-list XML Schema datatypes, called the OWL datatypes, can be used in OWL 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 built-in XML Schema datatypes may be used, but with caveats (see below).
The specific considerations with the other built-in XML Schema datatypes are:
An OWL ontology in the abstract syntax is a sequence of axioms and facts, plus inclusion references to other ontologies, which are considered to be included in the ontology. Ontologies can also have annotations that can be used to record authorship and other information associated with an ontology. OWL ontologies are web documents, and can be referenced by means of a URI.
ontology ::= 'Ontology(' { directive } ')' directive ::= 'Annotation(' URIreference URIreference ')' | 'Annotation(' URIreference dataLiteral ')' | 'Imports(' URI ')' | axiom | fact
Ontologies incorporate information about classes, properties, and individuals, each of which can have an identifier which is a URI reference.
datatypeID ::= URIreference classID ::= URIreference individualID ::= URIreference datavaluedPropertyID ::= URIreference individualvaluedPropertyID ::= URIreference
If a URI reference is a datatype, i.e., the URI reference points to one of the useful XML Schema datatypes described above, then that URI reference cannot be used as the identifier of a class. 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 in this abstract syntax, although the ontology cannot then be translated into an OWL DL RDF graph. Individual identifiers are used to refer to resources, and data literals are used to refer to data values.
In OWL, as in RDF, 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 two disjoint groups, data-valued properties and individual-valued properties. Data-valued properties relate individuals to data values; individual-valued properties relate individuals to other individuals.
There are two built-in classes in OWL, they both use URI references in the OWL URI, http://www.w3.org/2002/07/owl#, for which the namespace name owl is used here. The class with identifier owl:Thing is the class of all individuals, and is part of OWL Lite. The class with identifier owl:Nothing is the empty class.
Many OWL constructs use annotations, which, just like annotation directives, are used to record information associated with some portion of the construct.
annotation ::= 'annotation(' URIreference URIreference ')' | 'annotation(' URIreference dataLiteral ')'
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 mirror RDF/XML syntax without the use of rdf:nodeID.
fact ::= individual individual ::= 'Individual(' [ individualID ] { annotation } { 'type(' type ')' } { propertyValue } ')' propertyValue ::= '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 classIDs or OWL Lite restrictions
type ::= classID | restriction
In the OWL DL abstract syntax types can be general descriptions, which include classIDs and OWL Lite restrictions as well as other constructs
type ::= description
Data literals in the abstract syntax consist of a datatype and the lexical representation of a data value in that datatype (a typed literal) or just a string (an untyped literal). In the abstract syntax typed literals must be valid, i.e., xsd:integer1.5 is not a valid OWL data literal.
dataLiteral ::= typedLiteral | untypedLiteral typedLiteral ::= datatypeID lexicalForm untypedLiteral ::= lexicalForm lexicalForm ::= UniCode string enclosed in quotes
The second kind of facts is used to make individual identifiers be the same or pairwise distinct.
fact ::= 'SameIndividual(' individualID {individualID} ')' | 'DifferentIndividuals(' 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. The OWL DL axioms include the 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 logical 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 more-general 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 more-general classes and restrictions. In the OWL DL abstract syntax a class axiom contains a collection of descriptions, which can be more-general 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 sub-properties of others; can be made functional, inverse functional, symmetric, or transitive; and can be given global domains and ranges. However, most information about properties is more naturally expressed in restrictions, which allow local range and cardinality information to be specified.
There is no requirement in the abstract syntax that there be an axiom for each class used in an ontology. In fact, there can be any number of axioms for each class, including none. Properties used in an abstract syntax ontology have to be categorized as either data-valued or individual-valued, so they need an axiom for this purpose at least. There is no requirement that there be at most one axiom for a class or property used in an ontology. Each axiom for a particular class (or property) identifier contributes to the meaning of the class (or property).
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.
axiom ::= 'Class(' classID 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 } ')'
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.
There is a side condition in OWL Lite that properties that are transitive or that have transitive sub-properties may not have cardinality conditions expressed on them in restrictions.
restriction ::= 'restriction(' datavaluedPropertyID { 'allValuesFrom(' datatypeID ')'} { 'someValuesFrom(' datatypeID ')' } { cardinality } ')' | 'restriction(' individualvaluedPropertyID { 'allValuesFrom(' classID ')'} { 'someValuesFrom(' classID ')' } { cardinality } ')' cardinality ::= 'minCardinality(0)' | 'minCardinality(1)' | | 'maxCardinality(0)' | 'maxCardinality(1)' | | 'cardinality(0)' | 'cardinality(1)'
Properties are also specified using a frame-like syntax. Properties are divided into data-valued properties, which relate individuals to data values, like integers, and individual-valued properties, which relate individuals to other individuals. Properties can be given super-properties, allowing the construction of a property hierarchy. It does not make sense to have an individual property be a super-property of a data property, or vice versa.
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. Properties can have 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, properties can have 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 individual-valued properties are classes; ranges for data-valued properties are datatypes.
Data-valued 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. Individual-valued properties can be specified to be the inverse of another property. Individual-valued properties can also be specified to be symmetric as well as partial functional, partial inverse-functional, or transitive.
Individual-valued properties that are transitive, or that have transitive sub-properties, may not have cardinality conditions expressed on them, either in restrictions or by being functional, or inverse functional. This is needed to maintain the decidability of the language.
axiom ::= 'DatatypeProperty(' datavaluedPropertyID { annotation } { 'super(' datavaluedPropertyID ')' } {domain(classID')'} {range(datatypeID')' } [Functional] ')' axiom ::= 'ObjectProperty(' individualvaluedPropertyID { annotation } { 'super(' individualvaluedPropertyID ')'} { 'domain(' classID ')'} { 'range(' classID ')' } ['inverseOf(' individualvaluedPropertyID' )'] [ Symmetric ] [ 'Functional' | 'InverseFunctional' | 'Functional' 'InverseFunctional' | 'Transitive' ] ')'
The following axioms make several properties be equivalent, or make one property be a sub-property of another.
axiom ::= 'EquivalentProperties(' datavaluedPropertyID { datavaluedPropertyID } ')' | 'SubPropertyOf(' datavaluedPropertyID datavaluedPropertyID ')' | 'EquivalentProperties(' individualvaluedPropertyID { individualvaluedPropertyID } ')' | 'SubPropertyOf(' individualvaluedPropertyID individualvaluedPropertyID ')'
The OWL DL abstract syntax has more-general versions of the OWL Lite class axioms where superclasses, more-general restrictions, and boolean combinations of these are allowed. Together, these constructs are called descriptions.
axiom ::= 'Class(' classID 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 { 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 annotataion, the first kind of class axiom just above.
axiom ::= 'DisjointClasses(' description { description } ')' | 'EquivalentClasses(' description { description } ')' | 'SubClassOf(' description description ')'
Descriptions in the OWL DL abstract syntax include class identifiers and the restriction constructor. 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. As well, cardinalities are not restricted to only 0 and 1.
restriction ::= 'restriction(' datavaluedPropertyID { 'allValuesFrom(' dataRange ')'} { 'someValuesFrom(' dataRange ')'} { 'value(' dataLiteral ')' } { cardinality } ')' | 'restriction(' individualvaluedPropertyID { 'allValuesFrom(' description ')'} { 'someValuesFrom(' description ')'} { 'value(' individualID ')' } { cardinality } ')' cardinality ::= 'minCardinality(' non-negative-integer ')' | 'maxCardinality(' non-negative-integer ')' | 'cardinality(' non-negative-integer ')'
A dataRange, used as the range of a data-valued property and in other places in the OWL DL abstract syntax, is either a datatype or a set of data values.
dataRange ::= datatypeID | 'oneOf(' { dataLiteral } ')'
As in OWL Lite, there is a side condition that properties that are transitive, or that have transitive sub-properties, may not have cardinality conditions expressed on them in restrictions.
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 { annotation } { 'super(' datavaluedPropertyID ')'} { 'domain(' description ')' } { 'range(' dataRange ')'} [ 'Functional' ] ')' | 'ObjectProperty(' individualvaluedPropertyID { annotation } { 'super(' individualvaluedPropertyID ')'} { 'domain(' description ')' } { 'range(' description ')' } [ 'inverseOf(' individualvaluedPropertyID ')' ] [ 'Symmetric' ] [ 'Functional' | 'InverseFunctional' | 'Functional' 'InverseFunctional' | 'Transitive' ] ')'
As in OWL Lite, the following axioms make several properties be equivalent, or make one property be a sub-property of another.
axiom ::= 'EquivalentProperties(' datavaluedPropertyID { datavaluedPropertyID } ')' | 'SubPropertyOf(' datavaluedPropertyID datavaluedPropertyID ')' | 'EquivalentProperties(' individualvaluedPropertyID { individualvaluedPropertyID } ')' | 'SubPropertyOf(' individualvaluedPropertyID individualvaluedPropertyID ')'
This model-theoretic 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 for RDF graphs that is a vocabulary extension of the RDFS model theory.
The semantics here starts with the notion of a vocabulary, which is a set of URI references. 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.
Definition: An OWL vocabulary V is a set of URI references, including http://www.w3.org/2002/07/owl#Thing (which will generally be written as owl:Thing) and http://www.w3.org/2002/07/owl#Nothing (which will generally be written as owl:Nothing). Each OWL vocabulary also includes the canonical URI references for the OWL datatypes. In the semantics below, LV is the (non-disjoint) union of the value spaces of the OWL datatypes and Unicode strings.
Definition: An Abstract OWL interpretation with vocabulary V is a four-tuple of the form: I = <R, EC, ER, S> where
EC and ER provide meaning for URI references that are used as OWL classes and OWL properties, respectively. S provides meaning for URI references that are used to denote OWL individuals. S is extended to untyped literals by mapping them onto themselves, i.e., S(l) = l for l an untyped literal. S is extended to typed data literals by utilizing the XML Schema mapping for the datatype, i.e., S(d l) is the value corresponding to l for the XML Schema dataytpe d. (P is the power set operator.)
Abstract OWL interpretations have the following conditions having to do with OWL datatypes:
EC is extended to the syntactic constructs of descriptions, dataRanges, individuals, and propertyValues as in the EC Extension Table.
An Abstract OWL interpretation, I, satisfies OWL axioms and facts as given in Axiom 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.
From Section 2, an OWL ontology in the abstract syntax is a sequence of axioms, facts, imports, and annotations. The effect of an imports construct is to import the contents of another OWL ontology into the current ontology. The imported ontology is the one that can be found by accessing the document at the URI that is the argument of the imports construct.
Definition: The imports closure of an OWL ontology is then the result of adding the contents of imported ontologies into the current ontology. If these contents contain further imports constructs, the process is repeated as necessary. A particular ontology is never imported more than once in this process, so loops can be handled. Annotation directives have no effect on the semantics of OWL ontologies in the abstract syntax.
Definitions: An Abstract OWL interpretation, I, satisfies an OWL ontology, O, iff I satisfies each axiom and fact in the imports closure of O. An Abstract OWL ontology is consistent if there is some interpretation that satisfies it. An Abstract OWL ontology entails an OWL axiom or fact if each interpretation that satisfies the ontology also satisfies the axiom or fact. An Abstract OWL ontology entails another Abstract OWL ontology if each interpretation that satisfies the first ontology also satisfies the second ontology. Note that there is no need to create the imports closure of an ontology - any method that correctly determines the entailment relation is allowed.
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.
The syntax for triples used here is the one used in the RDF Model Theory [RDF MT]. In this variant, qualified names are allowed. As detailed in the RDF Model Theory, 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. The only namespace prefixes used in the transformation are rdf, rdfs, xsd, and owl, which correspond to the namespaces http://www.w3.org/1999/02/22-rdf-syntax-ns#, http://www.w3.org/2000/01/rdf-schema#, http://www.w3.org/2001/XMLSchema#, and http://www.w3.org/2002/07/owl#, respectively.
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 non-deterministic 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]. These non-determinisms allow the generation of more RDF Graphs.
The left column of the table gives a piece of syntax (S), the center column gives its transformation (T(S)), and the right column gives an identifier for the main node of the transformation (M(T(S))), but only for syntactic constructs that can occur as pieces of directives. Repeating components are listed using ellipses, as in description1; … descriptionn, this form allows easy specification of the transformation for all values of n greater than or equal to zero. Optional portions of the abstract syntax (enclosed in square brackets) are optional portions of the transformation (signified by square brackets).
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 or object of a triple, the transformation of the construct is part of the production (but only once per production) and the main node of that transformation should be used for that node of 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. Also, some of the transformations require a URI for the current ontology. It is assumed that ontologies that are subject to this sort of transformation will be placed into a web-accessible document; the URI of this document is given as U.
Definition: An RDF graph is an OWL DL ontology in RDF graph form if it is equal (see below for a slight expansion) to a result of the transformation to triples above of the imports closure of an OWL DL ontology in abstract syntax form and, moreover,
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:decimal
so long as
the data value so encoded is a non-negative integer.
Definition: An RDF graph is an OWL Lite ontology in RDF graph form if it is equal (with the same relaxation as for OWL DL) to a result of the transformation to triples above of the imports closure of an OWL Lite ontology in abstract syntax form that meets the requirements given just above.
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.
The above definition of OWL DL and OWL Lite ontologies in RDF graph form is couched from the perspective of the abstract syntax, as this is the perspective from which it can be easily stated. The following, much longer description of OWL DL ontologies in RDF graph form is couched from the perspective of RDF graphs. This description is strictly informative. The normative definition of what constitutes an OWL DL ontology in RDF graph form is given above.
Let G be an RDF graph. A node x1 in G is a non-empty list in G with elements e1,…,en if there is a set of triples in G of the form
x1 rdf:type rdf:List . x1 rdf:first e1 . x1 rdf:rest x2 . ... xn rdf:type rdf:List . xn rdf:first en . xn rdf:rest rdf:nil .
where each xi is a distinct blank node that appears as the object of exactly one triple in G and x1 does not appear as the object of an rdf:rest triple. The definition triples of x1 are the triples above plus the definition triples of e1,...,en.
A node x in G is a description in G if x is a blank node and there is a set of triples of one of the entries in the Description Triples table, where
The definition triples of the description are the triples above plus any
x rdf:type owl:Class .
or
x rdf:type rdfs:Class .
triples
plus the definition triples of any description, data range, or list in the
triples above.
A node x in G is a data range in G if x is a blank node and there
is a triple of the form
x owl:oneOf rdf:nil .
or
x owl:oneOf is .
where is is a non-empty list whose elements are typed or untyped literals.
The definition triples of the data range are the triples above plus any
triples of the form
x rdf:type rdfs:Class .
plus the definition triples of the list.
A node x in G is a datatype property if x is a URI reference and
there is a triple of the form
x rdf:type owl:DatatypeProperty .
but no triple of any of the following forms
x rdf:type owl:SymmetricProperty . x rdf:type owl:InverseFunctionalProperty . x rdf:type owl:TransitiveProperty .
The assertions about x in G are the triples in G of the following forms, where y is a datatype property in G, d is a description or class in G, and r is a data range or datatype in G
x rdf:type owl:DatatypeProperty . x rdf:type rdf:Property . x rdfs:subPropertyOf y . x rdfs:domain d . x rdfs:range r . x rdf:type owl:FunctionalProperty . x owl:samePropertyAs y .
plus the definition triples of any description or data range in these triples.
A node x in G is an object property if x is a URI reference and
there is a triple of the form
x rdf:type owl:ObjectProperty .
The assertions about x in G are the triples in G of the following forms,
where y is an object property in G, d is a description or class in G
x rdf:type owl:ObjectProperty . x rdf:type rdf:Property . x rdfs:subPropertyOf y . x rdfs:domain d . x rdfs:range d . x owl:inverseOf y . x rdf:type owl:SymmetricProperty . x rdf:type owl:FunctionalProperty . x rdf:type owl:InverseFunctionalProperty . x rdf:type owl:TransitiveProperty . x owl:samePropertyAs y .
plus the definition triples of any description in these triples.
A node x in G is a transitive object property if x is an object
property and there is a triple of the form
x rdf:type owl:TransitiveProperty .
A node x in G is a complex object property if x is an object property and there is a triple of any of the following forms in G
x rdf:type owl:FunctionalProperty . x rdf:type owl:InverseFunctionalProperty . x owl:inverseOf y . x owl:samePropertyAs y . y rdfs:subClassOf x .
where y is a complex object property in G or if there are triples of each of the forms
z owl:onProperty x . z c y .
where c is one of owl:minCardinality
,
owl:maxCardinality
, or owl:cardinality
.
A node x in G is a datatype if x is a URI reference and there
is a triple of the form
x rdf:type rdfs:Datatype .
The assertions about x in G are the triples in G of the following forms,
where d is a top-level description or class in G
x rdf:type rdfs:Datatype .
A node x in G is a class if x is owl:Thing
or
owl:Nothing
or x is a URI reference and there is a triple of
the form
x rdf:type owl:Class .
The assertions about x in G are the triples in G of the following forms,
where d is a top-level description or class in G and ds is rdf:nil or a
non-empty list whose elements are descriptions or classes and is is rdf:nil
or a non-empty list whose elements are individuals, plus the definition
triples of any non-empty lists in these triples
x rdf:type owl:Class . x rdf:type rdfs:Class . x rdfs:subClassOf d . x owl:sameClassAs d . x owl:disjointFrom d. x owl:complementOf d. x owl:intersectionOf ds. x owl:unionOf ds. x owl:oneOf is .
A node x in G is a top-level description if x is a description that is not in the definition triples of any other description in G nor an element of a list in G. The assertions about x in G are the triples in G of the following forms, where d is a top-level description or class in G
x rdf:type owl:Class . x rdfs:subClassOf d . x owl:sameClassAs d . x owl:disjointWith d .
plus the definition triples of x.
A node x in G is an individual if there is a triple of the form
x rdf:type c .
where c is a description or class.
The assertions about x in G are the triples of G of the following forms,
where c is a description or class, rd is a datatype property, v is a typed
or untyped literal, ro is an object property, and i is an individual.
x rdf:type c . x rd v . x ro i . x owl:sameIndividualAs i . x owl:differentFrom i .
plus the definition triples of any description in these triples.
A node x in G is an all-different node if there is a triple of the
form
x rdf:type owl:allDifferent .
and there is exactly one other triple in G whose subject is x and this
triple is of one of the following forms, where l is a non-empty list
whose elements are individuals
x owl:distinctMembers owl:nil . x owl:distinctMembers l .
The assertions about x are the above triples, plus the definition triples of l, if present.
A node x in G is an ontology if x is a URI reference and there
is a triple of the form
x rdf:type owl:Ontology .
The assertions about x are the triples of G of the following form
x rdf:type owl:Ontology . x owl:imports y .
where y is a URI reference that is not a datatype property, an object property, a class, or an individual.
An RDF graph is an OWL DL graph if:
A quick incomplete gloss of the above is that
This model-theoretic semantics for OWL is an extension of the RDFS semantics as defined in the RDF model theory [RDF MT], and defines the OWL semantic extension of RDF.
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 the class extensions of owl:Thing, owl:Class, and owl:Property. 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 class extension of owl:Property comprises the properties of the OWL universe.
There are two different styles of using OWL. In the more free-wheeling style, called OWL Full, the three parts of the OWL universe are identified with their RDFS counterparts, namely the class extensions of rdfs:Resource, rdfs:Class, and rdf:Property. In OWL Full, as in RDFS, 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 RDFS counterparts and, moreover, pairwise disjoint.
The 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 model-theoretic semantics into the RDFS semantics.
The chief differences in practice between the two styles lie 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. 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 qualified names are used as shorthand for URI references. The namespace identifiers used in such names, namely rdf, rdfs, xsd, and owl, should be used as if they are given their usual definitions. Throughout this section VRDFS is the RDF and RDFS built-in vocabulary, i.e., rdf:type, rdf:Property, rdfs:Class, rdfs:subClassOf, …, minus rdfs:Literal; and VOWL is the OWL built-in vocabulary, i.e., owl:Class, owl:onProperty, …, minus owl:Thing and owl:Nothing.
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 model theory [RDF MT], for V a set of URI references containing the RDF and RDFS vocabulary and a set D of datatypes, a D-interpretation of V is a tuple I = < RI, PI, EXTI, SI, LI >, where LV ⊆ RI. Here RI is the domain of discourse or universe, i.e., a set that contains the denotations of URI references. PI is a subset of RI, the properties of I. EXTI is used to give meaning to properties, and is a mapping from PI to P(RI × RI). SI is a mapping from V to RI that takes a URI reference to its denotation. LI is a mapping from typed literals to LV.
CEXTI is then defined as CEXTI(c) = { x∈RI | <x,c>∈EXTI(SI(rdf:type)) }. D-interpretations must meet several conditions, as detailed in the RDFS model theory. For example, I(rdfs:subClassOf) must be a transitive relation and the class extension of all datatypes must be in LV.
Definition: Let D be the RDF datatyping scheme generated by the OWL datatypes. An OWL interpretation, I = < RI, PI, EXTI, SI, LI >, of a vocabulary V, where V includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing, and the canonical URI references for the OWL datatypes, as its datatypes, is a D-interpretation of V that satisfies all the constraints in this section.
Elements of the OWL vocabulary that correspond to Description Logic constructors are given a different treatment from elements of the OWL vocabulary that correspond to (other) semantic relationships. The former have only-if semantic conditions and comprehension principles; the latter have if-and-only-if semantic conditions. The only-if 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 if-and-only-if semantic conditions for the latter are needed so that useful entailments are valid.
If-and-only-if conditions for RDFS domains and ranges
If E is | then for | <x,y>∈EXTI(SI(E)) iff |
---|---|---|
rdfs:domain | x∈IOP,y∈IOC | <z,w>∈EXTI(x) → z∈CEXTI(y) |
rdfs:range | x∈IOP,y∈IOC∪IDC | <w,z>∈EXTI(x) → z∈CEXTI(y) |
Note that IOC is the set of OWL classes, IDC is the set of OWL datatypes, and IOP is the set of OWL properties. These sets, and a few others, are defined in the next table.
Conditions concerning the parts of the OWL universe and syntactic categories
The above table is the definition of several semantic sets, namely IOC, IOT, IOR, IOP, IOOP, IODP, IDC, IAD, and IL. That is, these are simply shorthand names for the appropriate class extension.
Characteristics of OWL classes, datatypes, and properties
Characteristics of OWL vocabulary related to equivalence
Conditions on OWL vocabulary related to boolean combinations and sets
We will say that l1 is a sequence of
y1,…,yn over C iff
n=0 and l1=SI(rdf:nil)
or n>0 and l1∈IL and
∃ l2, …, ln ∈ IL such that
<l1,y1>∈EXTI(SI(rdf:first)), y1∈C,
<l1,l2>∈EXTI(SI(rdf:rest)), …,
<ln,yn>∈EXTI(SI(rdf:first)), yn∈C, and
<ln,SI(rdf:nil)>∈EXTI(SI(rdf:rest)).
Further conditions on owl:oneOf
If E is | and | then if <x,l>∈EXTI(SI(E)) then |
---|---|---|
owl:oneOf | l is a sequence of y1,…yn over LV | x∈IDC and CEXTI(x) = {y1,..., yn} |
owl:oneOf | l is a sequence of y1,…yn over IOT | x∈IOC and CEXTI(x) = {y1,..., yn} |
Conditions on OWL restrictions
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.
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 first-order, 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.
The domain of discourse is divided up into several pieces.
LV, IOT, IOC, IDC, IOP, and IL are all pairwise disjoint. |
There is a disjoint partition of IOP into IOOP and IODP. |
For v ∈ VRDFS∪VOWL - {rdf:nil}, SI(v) ∈ RI - (LV∪IOT∪IOC∪IDC∪IOP∪IL). |
Now entailment in OWL DL can be defined.
Definition: Let K be an RDF graph. The imports closure of K is the smallest superset of K such that if the imports closure of K contains a triple of the form x owl:imports y . where x and y are any URIs then the imports closure of K contains the triples resulting from the RDF parsing of the document, if any, accessible at y into triples.
Definitions: Let K and Q be RDF graphs. Then K OWL DL entails Q whenever every OWL DL interpretation (of any vocabulary V that includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing) that satisfies the RDF graph specified by imports closure of K also satisfies the RDF graph specified by imports closure of Q. K is OWL DL consistent if there is some OWL DL interpretation that satisfies the imports closure of K.
One way to automatically obtain typing information for the vocabulary is to use translations into RDF graphs of certain kinds of OWL ontologies in the abstract syntax, as such translations contain information on what a URI reference denotes. This is made more formal below.
Definition: A separated OWL vocabulary, V', is a set of URI references with a disjoint partition into VI, VC, VD, VOP, and VDP, where owl:Thing and owl:Nothing are in VC, rdfs:Literal is in VD, and all the canonical URI references for the OWL datatypes are in VD. Further V' is disjoint from VRDFS∪VOWL. A separated OWL vocabulary will generally be written as V' = VI + VC + VD + VOP + VDP. If the partition is not important, it will not be written out.
Definition: An OWL abstract ontology with separated names over a separated OWL vocabulary V' = VI + VC + VD + VOP + VDP, is a set of OWL axioms and facts in the abstract syntax without annotations as in Section 2 where <individualID>s are taken from VI, <classID>s are taken from VC, <datatypeID>s are taken from VD, <individualvaluedPropertyID>s are taken from VOP, and <datavaluedPropertyID>s are taken from VDP.
Theorem 1: Let T be the mapping from OWL ontologies in the abstract syntax to RDF graphs. Let V' = VI + VC + VD + VOP + VDP be a separated OWL vocabulary. Let K and Q be OWL abstract syntax ontologies with separated names over V' and let V = V' ∪ VRDFS ∪ VOWL. Then it is the case that K entails Q if and only if T(K) OWL DL entails T(Q). The proof is contained in Appendix A.1.
A simple corollary of this is that K is consistent if and only if T(K) is consistent.
OWL Full augments the common conditions with conditions that force the parts of the OWL universe to be the same as their analogues in RDFS. These new conditions interact with the common conditions. For example, because in OWL Full IOT is the entire RDF domain of discourse, the second comprension 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 = RI |
IOC = CEXTI(SI(rdfs:Class)) |
IOP = CEXTI(SI(rdf:Property)) |
OWL Full entailment and OWL Full consistency are defined in same manner as OWL DL entailment and OWL DL consistency.
Theorem 2: Let K,C be RDF graphs such that each of K, C, and K∪C is the translation of some OWL ontology in the abstract syntax with separated vocabulary. Then K OWL Full entails C if K OWL DL entails C. An initial 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 for OWL DL correspond on certain OWL ontologies. One semantics used in this section is the direct model theory for abstract OWL ontologies given in the direct model-theoretic semantics section of this document. The other semantics is the extension of the RDFS semantics given in the RDFS-compatible model-theoretic semantics section of this document.
Throughout this section qualified names are used as shorthand for URI
references.
The namespace identifiers used in such names, namely rdf, rdfs, xsd,
and owl, should be used as if they are given their usual definitions.
Throughout this section
VRDFS is the RDF and RDFS built-in vocabulary,
i.e., rdf:type, rdf:Property, rdfs:Class, rdfs:subClassOf, …,
minus rdfs:Literal; and
VOWL is the OWL built-in vocabulary,
i.e., owl:Class, owl:onProperty, …,
minus owl:Thing and owl:Nothing.
Throughout this section D will be a datatyping scheme, i.e., a set of
URI references that have class extensions that are subsets of LV and
mappings from strings to their class extension.
Throughout this section T will be the mapping from abstract OWL
ontologies to RDF graphs.
Recall that a separated OWL vocabulary is a set of URI references V with a disjoint partition, written V = VI + VC + VD + VOP + VDP where owl:Thing and owl:Nothing are in VC, rdfs:Literal is in VD, and all the elements of D are in VD. Further V is disjoint from VRDFS∪VOWL.
An OWL abstract KB with separated names over a separated OWL vocabulary V = VI + VC + VD + VOP + VDP is a set of OWL axioms and facts without annotations as in Section 2 where <individualID>s are taken from VI, <classID>s are taken from VC, <datatypeID>s are taken from VD, <individualvaluedPropertyIDs> are taken from VOP, and <datavaluedPropertyID>s are taken from VDP.
Let V = VI + VC + VD + VOP + VDP be a separated OWL vocabulary. Then T(V) is the RDF graph that contains exactly <v,rdf:type,owl:Thing > for v ∈ VI, <v,rdf:type,owl:Class > for v ∈ VC, <v,rdf:type,rdfs:Datatype > for v ∈ VD, <v,rdf:type,owl:ObjectProperty > for v ∈ VOP, and <v,rdf:type,owl:DatatypeProperty > for v ∈ VDP.
The theorem to be proved is:
Let V' be a separated OWL vocabulary.
Let K,Q be abstract OWL ontologies with separated names over V'.
Then K OWL entails Q iff T(K),T(V') OWL DL entails T(Q).
Actually, a slightly stronger correspondence can be shown, but this is enough for now, as the presence of annotations and imports causes even more complications.
Lemma 1:
Let V' = VI + VC + VD + VOP + VDP be a separated OWL vocabulary.
Let V = VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VRDFS ∪ VOWL.
Let I'= <R,EC,ER,S> be an abstract OWL interpretation of V'.
Let I = <RI,PI,EXTI,SI,LI>
be an OWL DL interpretation of V that satisfies T(V').
Let CEXTI have its usual meaning, and, as usual, overload I to
map any syntactic construct into its denotation.
If R=CEXTI(I(owl:Thing)),
S(v)=SI(v) for v ∈ VI,
EC(v)=CEXTI(SI(v)) for v∈VC∪VD, and
ER(v)=EXTI(SI(v)) for v∈VOP∪VDP
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 = CEXTI(I(owl:Thing)), IOC = CEXTI(I(owl:Class)), IDC = CEXTI(I(rdfs:Datatype)), IOOP = CEXTI(I(owl:ObjectProperty)), IODP = CEXTI(I(owl:DatatypeProperty)), and IL = CEXTI(I(rdf:List)).
To make the induction work, it is necessary to show that for any d a description or data range with sub-constructs T(d) contains triples for each of the sub-constructs that do not share any blank nodes with triples from the other sub-constructs. 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)>∈EXTI(I(rdfs:domain)) and <p,I(owl:Thing)>∈EXTI(I(rdfs:range)). Thus I satisfies T(p). Similarly for p∈VDP.
Lemma 2: Let V', V, I', and I be as in Lemma 1. Let D be an OWL directive over V'. Then I satisfies T(D) iff I' satisfies D.
Proof
Let d=intersectionOf(d1 … dn). 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), CEXTI(I+A(M(T(d)))) = EC(d). Thus for some A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXTI(I+A(M(T(d)))) = EC(d) and I+A(M(T(d))∈IOC.
If I' satisfies D then EC(foo) = EC(d). From above, there is some A such that CEXTI(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXTI(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)))> ∈ EXTI(I(owl:sameClassAs)). Therefore I satisfies T(D).
If I satisfies T(D) then I satisfies T(intersectionOf(d1 … dn)). Thus there is some A as above such that <I(foo),I+A(M(T(d)))> ∈ EXTI(I(owl:sameClassAs)). Thus EC(d) = CEXTI(I+A(M(T(d)))) = CEXTI(I(foo)) = EC(foo). Therefore I' satisfies D.
Let d=intersectionOf(d1 … dn). 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), CEXTI(I+A(M(T(d)))) = EC(d). Thus for some A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXTI(I+A(M(T(d)))) = EC(d) and I+A(M(T(d))∈IOC.
If I' satisfies D then EC(foo) ⊆ EC(d). From above, there is some A such that CEXTI(I+A(M(T(d)))) = EC(d) ⊇ EC(foo) = CEXTI(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)))> ∈ EXTI(I(rdfs:subClassOf)). Therefore I satisfies T(D).
If I satisfies T(D) then I satisfies T(intersectionOf(d1 … dn)). Thus there is some A as above such that <I(foo),I+A(M(T(d)))> ∈ EXTI(I(rdfs:subClassOf)). Thus EC(d) = CEXTI(I+A(M(T(d)))) ⊇ CEXTI(I(foo)) = EC(foo). Therefore I' satisfies D.
Let d=oneOf(i1 … in). 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), CEXTI(I+A(M(T(d)))) = EC(d).
If I' satisfies D then EC(foo) = EC(d). From above, there is some A such that CEXTI(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXTI(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)))> ∈ EXTI(I(owl:sameClassAs)). Therefore I satisfies T(D).
If I satisfies T(D) then I satisfies T(intersectionOf(d1 … dn)). Thus there is some A as above such that <I(foo),I+A(M(T(d)))> ∈ EXTI(I(owl:sameClassAs)). Thus EC(d) = CEXTI(I+A(M(T(d)))) = CEXTI(I(foo)) = EC(foo). Therefore I' satisfies D.
As di is a description over V' therefore I satisfies T(di) and for any A mapping the blank nodes of T(di) such that I+A satisfies T(di), CEXTI(I+A(M(T(di)))) = EC(di).
If I satisfies T(D) then for 1≤i≤n there is some Ai such that I satisfies <I+Ai(M(T(di))),I+Aj(M(T(dj)))> ∈ EXTI(I(owl:disjointWith)) for each 1≤i<j≤n. Thus EC(di)∩EC(dj) = {}, for i≠j. Therefore I' satisfies D.
If I' satisfies D then EC(di)∩EC(dj) = {} for i≠j. For any Ai and Aj as above <I+Ai+Aj(M(T(di))),I+Ai+Aj(M(T(dj)))> ∈ EXTI(I(owl:disjointWith)), for i≠j. As at least one Ai exists for each i, and the blank nodes of the T(dj) are all disjoint, I+A1+…+An satisfies T(DisjointClasses(d1 … dn)). Therefore I satisfies T(D).
As di for 1≤i≤m is a description over V' therefore I satisfies T(di) and for any A mapping the blank nodes of T(di) such that I+A satisfies T(di), CEXTI(I+A(M(T(di)))) = EC(di). Similarly for ri for 1≤i≤k.
If I' satisfies D, then, as p∈VOP, I satisfies I(p)∈IOOP. Then, as I is an OWL DL interpretation, I satisfies <I(p),I(owl:Thing)>∈EXTI(I(rdfs:domain)) and <I(p),I(owl:Thing)>∈EXTI(I(rdfs:range)). Also, ER(p)⊆ER(si) for 1≤i≤n, so EXTI(I(p))=ER(p) ⊆ ER(si)=EXTI(I(si)) and I satisfies <I(p),I(si)>∈EXTI(I(rdfs:subPropertyOf)). Next, ER(p)⊆EC(di)×R for 1≤i≤m, so <z,w>∈ER(p) → z∈EC(di) and for any A such that I+A satisfies T(di), <z,w>∈EXTI(p) → z∈CEXTI(I+A(M(T(di)))) and thus <I(p),I+A(M(T(di)))>∈EXTI(I(rdfs:domain)). Similarly for ri for 1≤i≤k.
If I' satisfies D and inverse(i) is in D, then ER(p) and ER(i) are converses. Thus <u,v>∈ER(p) iff <v,u>∈ER(i) so <u,v>∈EXTI(p) iff <v,u>∈EXTI(i) and I satisfies <I(p),I(i)>∈EXTI(I(owl:inverseOf)). If I' satisfies D and Symmetric is in D, then ER(p) is symmetric. Thus if <x,y>∈ ER(p) then <y,x>∈ER(p) so if <x,y> ∈ EXTI(p) then <y, x>∈EXTI(p). and thus I satisfies p∈CEXTI(I(owl:Symmetric)). Similarly for Functional, InverseFunctional, and Transitive. Thus if I' satisfies D then I satisfies T(D).
If I satisfies T(D) then, for 1≤i≤n, <I(p),I(si)>∈EXTI(I(rdfs:subPropertyOf)) so ER(p)=EXTI(I(p)) ⊆ EXTI(I(si))=ER(si). Also, for 1≤i≤m, for some A such that I+A satisfies T(di), <I(p),I+A(M(T(di)))>∈EXTI(I(rdfs:domain)) so <z,w>∈EXTI(p) → z∈CEXTI(I+A(M(T(di)))). Thus <z,w>∈ER(p) → z∈EC(di) and ER(p)⊆EC(di)×R. Similarly for ri for 1≤i≤k.
If I satisfies T(D) and inverse(i) is in D, then I satisfies <I(p),I(i)>∈EXTI(I(owl:inverseOf)). Thus <u,v>∈EXTI(p) iff <v,u>∈EXTI(i) so <u,v>∈ER(p) iff <v,u>∈ER(i) and ER(p) and ER(i) are converses. If I satisfies D and Symmetric is in D, then I satisfies p∈CEXTI(I(owl:Symmetric)) so if <x,y> ∈ EXTI(p) then <y, x>∈EXTI(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(D) then I' satisfies D.
As pi∈VOP and I satisfies T(V'), I(pi)∈IOP. If I satisfies T(D) then <I(pi),I(pj)> ∈ EXTI(I(owl:samePropertyAs)), for each 1≤i<j≤n. Therefore EXTI(pi) = EXTI(pj), for each 1≤i<j≤n; ER(pi) = ER(pj), for each 1≤i<j≤n; and I' satisfies D.
If I' satisfies D then ER(pi) = ER(pj), for each 1≤i<j≤n. Therefore EXTI(pi) = EXTI(pj), for each 1≤i<j≤n. From the OWL DL definition of owl:samePropertyAs, <I(pi),I(pj)> ∈ EXTI(I(owl:samePropertyAs)), for each 1≤i<j≤n. Thus I satisfies T(D).
If I satisfies T(D) then there is some A that maps each blank node in T(D) such that I+A satisfies T(D). A simple examination of T(D) shows that the mappings of A plus the mappings for the individual IDs in D, which are all in IOT, show that I' satisfies D.
If I' satisfies D then for each Individual construct in D there must be some element of R that makes the type relationships and relationships true in D. The triples in T(D) 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(D).
Lemma 3: Let V' = VI + VC + VD + VOP + VDP be a separated OWL vocabulary. Let V = VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VRDFS ∪ VOWL. Then for every OWL DL interpretation I = < RI, PI, EXTI, SI, LI > of V that satisfies T(V') there is an abstract OWL interpretation I' of V' such that for any OWL abstract KB K of V, I' abstract OWL satisfies K iff I OWL DL satisfies T(K).
Proof
Let CEXTI be defined as usual from I. The required abstract OWL interpretation will be I' = < CEXTI(I(owl:Thing)), EC, ER, S > where S(n) = I(n) for n∈VI, EC(n) = CEXTI(I(n)) for n∈VC∪VD, and ER(n) = EXTI(I(n)) for n∈VOP∪VDP.
Satisfying an abstract KB is just satisfying its directives and satisfying the translation of an abstract KB is just satisfying all the triples so I OWL DL satisfies T(K) iff I' abstract OWL satisfies K.
Lemma 4: Let V' = VI + VC + VD + VOP + VDP be a separated OWL vocabulary. Let V = VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VRDFS ∪ VOWL. Then for every Abstract OWL interpretation I' = < U, EC, ER, S > of V' there is an OWL DL interpretation I of V that satisfies T(V') such that for any abstract OWL KB K of V', I OWL DL satisfies T(K) iff I' abstract OWL satisfies K.
Proof
Theorem 1: Let V' be a separated OWL vocabulary. Let K,Q be abstract OWL ontologies with separated names over V'. Then K OWL entails Q iff T(K),T(V') OWL DL entails T(Q).
Proof
Suppose K OWL entails Q. Let I be an OWL DL interpretation that satisfies T(K),T(V'). Then from Lemma 3, there is some abstract OWL interpretation I' such that for any abstract OWL ontology X over V', I satisfies T(X) iff I' satisfies X. Thus I' satisfies K. Because K OWL entails Q, I' satisfies Q, so I satisfies T(Q). Thus T(K),T(V') OWL DL entails T(Q).
Suppose T(K),T(V') OWL DL entails T(Q). Let I' be an abstract OWL interpretation that satisfies K. Then from Lemma 4, there is some OWL DL interpretation I that satisfies T(V') such that for any abstract OWL ontology X over V', I satisfies T(X) iff I' satisfies X. Thus I satisfies T(K). Because T(K),T(V') OWL DL entails T(Q), I satisfies T(Q), so I' satisfies Q. Thus K abstract OWL entails Q.
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 RDFS interpretation 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 KB 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 = < RI, EXTI, SI, LI > be an OWL interpretation that satisfies T(K). Let I' = < RI', EXTI', SI', LI' > be an OWL interpretation that satisfies T(K). Let RI' = CEXTI(I(owl:Thing)) + CEXTI(I(owl:ObjectProperty)) + CEXTI(I(owl:IndividualProperty)) + CEXTI(I(owl:Class)) + CEXTI(I(rdf:List)) + RI, where + is disjoint union. Define EXTI' so as to separate the various roles of the copies. Define SI' 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 EXTI. In essence the first component of RI' is OWL individuals, the second component of RI' is OWL datatype properties, the third component of RI' is OWL object properties, the fourth component of RI' is OWL classes, the fifth component of RI' is RDF lists, and the sixth component of RI' is everything else.
Theorem 2: Let K,C be RDF graphs such that each of K, C, and K∪C is the translation of some OWL KB in the abstract syntax with separated vocabulary. Then K OWL Full entails C if K OWL DL entails C.
Proof: From the above lemma and because all OWL Full interpretations are OWL interpretations.
Comment: The only if direction cannot be proved without showing that OWL Full has no semantic oddities, which has not yet been done.
This appendix gives examples of the concepts developed in the rest of the document.
The transformation rules in Section 4 transform
DatatypeProperty(ex:name) ObjectProperty(ex:author) Individual(type(ex:Book) value(ex:author Individual(type(ex:Person) value(ex:name xsd:string"Fred"))))
to
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
ObjectProperty(ex:enrolledIn) Class(ex:Student complete ex:Person restriction(ex:enrolledIn allValuesFrom(ex:School) minCardinality(1)))
to
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:sameClassAs _:x . _:x owl:intersectionOf _:l1 . _:l1 rdf:type rdf:List . _:l1 rdf:first ex:Person . _:l1 rdf:rest _:l2 . _:l2 rdf:type rdf:List . _:l2 rdf:first _:lr . _:l2 rdf:rest rdf:nil . _:lr owl:intersectionOf _:lr1 . _:lr1 rdf:type rdf:List . _:lr1 rdf:first _:r1 . _:lr1 rdf:rest _:lr2 . _:lr2 rdf:type rdf:List . _: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 .
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 .
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 separated-syntax 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 .