Web Ontology Language (OWL) Abstract Syntax and Semantics

W3C Working Draft 8 November 2002

This version:

http://www.w3.org/TR/2002/WD-owl-semantics-20021108/

Latest version:

http://www.w3.org/TR/owl-semantics/

Previous version:

http://www.w3.org/TR/2002/WD-owl-absyn-20020729/

Editors:

Peter F. Patel-Schneider, Bell Labs Research
Patrick Hayes, IHMC, University of West Florida
Ian Horrocks, Department of Computer Science, University of Manchester
Frank van Harmelen, Department of Artificial Intelligence, Vrije Universiteit Amsterdam

The normative form of this document is a compound HTML document.

Copyright ©2002 W3C ^© ( MIT, INRIA, Keio). All Rights Reserved. W3C liability, trademark , document use and software licensing rules apply.

---

Abstract

Status of this document

1. Introduction

The W3C Web Ontology Working Group (WebOnt) is tasked with producing a web ontology language extending the reach of XML, RDF, and RDF Schema. This language, called OWL, is based on the DAML+OIL web ontology language [DAML+OIL].

This document contains several interrelated specifications of the several styles of OWL. First, Section 2 contains a high-level, abstract syntax for both OWL Lite, a subset of OWL [OWL Features], and a fuller style of using OWL, sometimes called OWL/DL. This document, however, defines neither a presentation syntax nor an exchange syntax for OWL. The official exchange syntax for OWL is RDF/XML; a document defining how RDF is used to encode OWL is the subject of the OWL Reference document [OWL Reference]. A mapping from the abstract syntax to n-triples [RDF Tests] 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 an extension of the RDFS model-theoretic semantics that starts with n-triples and provides a semantics for OWL ontologies written in the official OWL exchange syntax. Two versions of this second semantics are provided, one that corresponds more-closely to the direct semantics and one that can be used in cases where classes need to be treated as individuals. 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 two different 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.

Finally a few examples of the various concepts defined in the document are presented in Appendix B.

1.1. Differences from DAML+OIL

The language described in this document is very close to DAML+OIL. The exchange syntax for OWL, as defined in the OWL Reference document [OWL Reference], has only minor changes from DAML+OIL. Even the abstract syntax can be viewed as an abstract syntax for DAML+OIL.

The only substantive changes between OWL and DAML+OIL are

• the removal of qualified number restrictions, per a decision of WebOnt;
• the ability to directly state that properties can be symmetric, per a decision of WebOnt; and
• the absence in abstract syntax of some abnormal DAML+OIL constructs, particularly restrictions with extra components, and a difference in their meaning.

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]. These naming changes may indicate potential changes to the preferred names in the concrete syntax for OWL, but the intent of WebOnt is to maintain the DAML+OIL names to the maximum extent reasonable.

1.2. Stances Taken on Open OWL Issues

This document takes stances on several open working group issues, some of which are detailed below. All working group issues are discussed in the issue listing document [OWL Issues].

• The document allows (in the abstract syntax) arbitrary annotations of ontologies and many kinds of axioms and facts. The n-triples syntax and RDFS-compatible semantics allows annotation of ontologies by using RDF properties on the document URI and annotation of classes, properties, and individuals by using RDF properties on the class, property, or individual. This is a simple solution to issue 4.4 and issue 5.14.
• This document provides a full account of the list construct, presenting a resolution for Issue 5.5. Lists do not occur in the abstract syntax. In the n-triples syntax lists are formed using rdf:List, rdf:first, rdf:rest, and rdf:nil. In the RDFS-compatible semantics, sufficient lists exist in all interpretations to support the presence of OWL syntax in interpretations, but there is no general comprehension principle for lists and there is no requirement that lists are well formed.
• This document provides an Imports directive in the abstract syntax, and gives it a meaning in terms of imports closure. In the RDFS-compatible semantics, an imports triple whose subject is the empty relative URI serves to signal an import with the same effect. This is a potential resolution for issue 5.6.
• This document uses a method for datatyping that is close to the emerging treatment of RDF datatyping in the RDF model theory, assuming that issue 5.8 will be resolved in favor of OWL using RDF datatyping. As the treatment of datatyping in the RDF model theory is undergoing change, this document does not completely match up with the current treatment of RDF datatyping.

Acknowledgments

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.

References

[DAML+OIL]

DAML+OIL (March 2001) Reference Description. Dan Connolly, Frank van Harmelen, Ian Horrocks, Deborah L. McGuinness, Peter F. Patel-Schneider, and Lynn Andrea Stein. W3C Note 18 December 2001. Latest version is available at http://www.w3.org/TR/daml+oil-reference.

[OWL Features]

Feature Synopsis for OWL Lite and OWL. Deborah L. McGuinness and Frank van Harmelen. W3C Working Draft 29 July 2002. Latest version is available at http://www.w3.org/TR/owl-features/.

[OWL Issues]

Web Ontology Issue Status. Michael K. Smith, ed. 10 July 2002.

[OWL Reference]

OWL Web Ontology Language 1.0 Reference. Mike Dean, Dan Connolly, Frank van Harmelen, James Hendler, Ian Horrocks, Deborah L. McGuinness, Peter F. Patel-Schneider, and Lynn Andrea Stein. W3C Working Draft 29 July 2002. Latest version is available at http://www.w3.org/TR/owl-ref/.

[RDFMS]

Resource Description Framework (RDF) Model and Syntax Specification. Ora Lassila and Ralph R. Swick, eds. W3C Recommendation 22 February 1999. Latest version is available at http://www.w3.org/TR/REC-rdf-syntax/.

[RDF MT]

RDF Model Theory. Patrick Hayes, ed. W3C Working Draft 29 April 2002. Latest version is available at http://www.w3.org/TR/rdf-mt/.

[RDF Tests]

RDF Test Cases. Jan Grant and Dave Beckett, ed. W3C Working Draft 29 April 2002. Latest version is available at http://www.w3.org/TR/rdf-testcases/.

2. Abstract Syntax

The description of OWL here 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 in DAML+OIL), again for ease of readability. 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.

This syntax does not have to worry about any of the problems induced by the RDF triple model, including non-closed and ill-formed lists and restrictions. No parsetype extensions are needed for readability, and many issues of coordination with the RDF Core WG are not relevant at this level of syntax. Layering issues can also be safely ignored. Further, namespace issues can also be somewhat ignored; in the syntax here reserved words are not given with any namespace qualification.

The abstract syntax is specified here by means of a version of Extended BNF. In this version of BNF, terminals are not quoted, non-terminals are enclosed in pointy brackets (<…>), and alternatives are either separated by vertical bars (|) or are given in different productions. Elements that can occur at most once are enclosed in square brackets ([…]); elements that can occur any number of times (including zero) are enclosed in braces ({…}).

The meaning of each construct in the OWL 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 (and DAML+OIL) 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 target that is approachable to a wider audience, a smaller language has been defined, now referred to as OWL Lite [OWL Features]. This smaller language attempts to capture many of the commonly used features of OWL. It also attempts to describe a useful language that provides more than RDF Schema with the goal of adding functionality that is important in order to support web applications. An abstract syntax is expressed both for this smaller language and also for a fuller style of OWL.

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 restrictions required to make OWL fit into the Description Logic paradigm, and thus this abstract syntax should be thought of a syntax for OWL/DL as defined in Section 5.3.1.

2.1. Ontologies

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 non-logical annotations that can be used to record authorship, and other non-logical information associated with an ontology. OWL ontologies are web documents, and can be referenced by means of a URI.

<ontology> ::= Ontology ( {<directive>} )

<directive> ::= Annotation ( <URI reference> <URI reference> )
<directive> ::= Annotation ( <URI reference> <lexical-form> )
<directive> ::= Imports ( <URI> )
<directive> ::= <axiom>
<directive> ::= <fact>

Ontologies incorporate information about classes, properties, and individuals, each of which can have an ID which is a URI reference. (It is convenient to use QNames wherever possible, turning their expansion into a URI reference, as is done in RDF.) Ontologies can also reference built-in XML Schema datatypes, by means of a URI reference for the datatype.

<datatypeID>                 ::= <URI reference>
<classID>                    ::= <URI reference>
<individualID>               ::= <URI reference>
<datavaluedPropertyID>       ::= <URI reference>
<individualvaluedPropertyID> ::= <URI reference>

If a URI reference is a datatype, i.e., if there is a datatype definition retrievable using the URI reference, then that URI reference cannot be used as the ID for a class. However, a URI reference can be the ID of a class or datatype as well as the ID of a property as well as the ID of an individual. Individual IDs are used to refer to resources, and typed data literals are used to refer to the XML Schema data values.

In OWL a datatype denotes the set of XML Schema 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. Elements of the first group of properties relate individuals to data values, elements of the second group relate individuals to other individuals.

There are two built-in classes in OWL, they both use URI references in the as-yet-to-be-determined OWL URI, for which the namespace name owl is used here. The class with ID owl:Thing is the class of all individuals, and is part of OWL Lite. The class with ID owl:Nothing is the empty class.

Many OWL constructs use annotations, which, just like annotation directives, are used to record non-logical information associated with some portion of the construct.

<annotation> ::= annotation ( <URI reference> <URI reference> )
<annotation> ::= annotation ( <URI reference> <lexical-form> )

2.2. Facts

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 the normal RDF/XML syntax.

<fact> ::= <individual> 
<individual> ::= Individual( [<individualID>] {<annotation>}
                              {type(<type>)} {<propertyValue>} )
<propertyValue> ::= value( <individualvaluedPropertyID>  <individualID> )
                  | value( <individualvaluedPropertyID>  <individual> )
                  | value( <datavaluedPropertyID>  <dataLiteral> )

Facts are the same in OWL Lite and the full abstract syntax, except for what can be a type. In OWL Lite, types can be classIDs or OWL Lite restrictions

<type> ::= <classID>
         | <restriction>

In the full abstract syntax types can be general descriptions, which include classIDs and OWL Lite restrictions

<type> ::= <description>

In the abstract syntax data literals consist of a datatype and the lexical representation of a data value in that datatype (a typed data literal).

<dataLiteral> ::= <typedDataLiteral>
<typedDataLiteral> ::= <datatypeID>  <lexical-form>

In the abstract syntax the other kinds of facts are used to make individual IDs be the same or pairwise distinct.

<fact> ::= SameIndividual( <individualID> {<individualID>} )
<fact> ::= DifferentIndividuals( <individualID> {<individualID>} )

2.3. Axioms

The biggest differences between OWL Lite and the full abstract syntax 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, and then the full abstract syntax is given as additions to OWL Lite.

Axioms are used to associate class and property IDs 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 full 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 the same 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 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) ID contributes to the meaning of the class (or property).

2.3.1. OWL Lite Axioms

2.3.1.1. OWL Lite Class Axioms

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 classes are the same.

<axiom> ::= EquivalentClasses( <classID> {<classID>} )

2.3.1.2. OWL Lite Restrictions

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 objects 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> ::= restriction( <individualvaluedPropertyID> {allValuesFrom(<classID>)}
                               {someValuesFrom(<classID>)} [<cardinality>] )
<cardinality> ::= minCardinality(0) | minCardinality(1) |
                | maxCardinality(0) | maxCardinality(1) |
                | cardinality(0)    | cardinality(1) 

2.3.1.3. OWL Lite Property Axioms

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 verb, just as in RDF. 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 the property. 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 functional, 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 the same, or make one property be a sub-property of another.

<axiom> ::= EquivalentProperties( <datavaluedPropertyID>  {<datavaluedPropertyID>} )
<axiom> ::= SubPropertyOf( <datavaluedPropertyID>  <datavaluedPropertyID> )
<axiom> ::= EquivalentProperties( <individualvaluedPropertyID>  {<individualvaluedPropertyID>} )
<axiom> ::= SubPropertyOf( <individualvaluedPropertyID>  <individualvaluedPropertyID> )

2.3.2. OWL Axioms

2.3.2.1. OWL Class Axioms

The full 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 full 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 full abstract syntax it is possible to require that a collection of descriptions be pairwise disjoint, or have the same members, or that one description is a subclass of another. Note that the last two of these axioms generalize the first kind of class axiom just above.

<axiom> ::= DisjointClasses( <description> {<description>} )
<axiom> ::= EquivalentClasses( <description> {<description>} )
<axiom> ::= SubClassOf( <description> <description> )

2.3.2.2. OWL Descriptions

Descriptions in the full abstract syntax include class IDs 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>} )

2.3.2.3. OWL Restrictions

Restrictions in the full 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 full 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> ::= 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 full abstract syntax, is either a datatype or a set of data values.

<dataRange> ::= <datatypeID>
<dataRange> ::= oneOf({<typedDataLiteral>} )

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.

2.3.2.4. OWL Property Axioms

Property axioms in the full 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] )

<axiom> ::= ObjectProperty 
        ( <individualvaluedPropertyID> {<annotation>} {super(<individualvaluedPropertyID>)}
          {domain(<description>)} {range(<description>)} 
          [inverseOf(<individualvaluedPropertyID>)] [Symmetric] 
          [Functional | InverseFunctional | Functional InverseFunctional | Transitive] )

3. Direct Model-Theoretic Semantics

This model-theoretic semantics for OWL goes directly from ontologies in the abstract syntax to a standard model theory. It is much simpler than the semantics Section 5 that uses an OWL knowledge base in the form of n-triples and is an extension of the RDFS model theory.

3.1. Vocabularies and Interpretations

The semantics here starts with the notion of a vocabulary, which can be thought of as the URI references that are of interest in a knowledge base. It is, however, not necessary that a vocabulary consist only of the URI references in a knowledge base.

An OWL vocabulary V is a set of URI references, including owl:Thing, owl:Nothing, and rdfs:Literal. Each OWL vocabulary also includes URI references for each of the XML Schema non-list built-in simple datatypes. In the semantics LV is the (non-disjoint) union of the value spaces of these datatypes.

An Abstract OWL interpretation with vocabulary V is a four-tuple of the form: I = <R, S, EC, ER>
where

• R is a non-empty set of resources, disjoint from LV
• S : V → R
• EC : V → 2^R ∪ 2^LV
• ER : V → 2^(R×R) ∪ 2^(R×LV)

S provides meaning for URI references that are used to denote OWL individuals, while EC and ER provide meaning for URI references that are used as OWL classes and OWL properties, respectively.

Abstract OWL interpretations have the following conditions having to do with datatypes:

1. If d is the URI reference for an XML Schema non-list built-in simple datatype then EC(d) is the value space of this datatype.
2. If c is not the URI reference for any XML Schema non-list built-in simple datatype then EC(c) is a subset of R.
3. If d,l is a datatype,literal pair then D(d,l) is the data value for l in XML Schema datatype d.

3.2. Interpreting Embedded Constructs

EC is extended to the syntactic constructs of <description>s, <dataRange>s, <individual>s, and <propertyValue>s as follows:

3.3. Interpreting Axioms and Facts

An Abstract OWL interpretation, I, is an interpretation of OWL axioms and facts as given in the table below. In the table, optional parts of axioms and facts are given in square brackets ([…]) and have corresponding optional conditions, also given in square brackets.

3.4. Interpreting Ontologies

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. 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.

Annotations have no effect on the semantics of OWL ontologies in the abstract syntax.

An Abstract OWL interpretation, I, is an interpretation of an OWL ontology, O, iff I is an interpretation of each axiom and fact in the imports closure of O.

An Abstract OWL ontology entails an OWL axiom or fact if each interpretation of the ontology is also an interpretation of the axiom or fact. An Abstract OWL ontology entails another Abstract OWL ontology if each interpretation of the first ontology is also an interpretation of 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.

4. Mapping to RDF N-Triples

The exchange syntax for OWL is RDF/XML, as specified in the OWL Reference Description [OWL Reference]. Further, the meaning of an OWL document base in RDF/XML is determined only from the n-triples [RDF Tests] that result 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 n-triples.

The n-triples syntax used here is the one used in the RDF Model Theory [RDF MT]. In this variant, QNames are allowed. To turn this syntax into the standard one, just turn the QName into the obvious URI reference. The only prefixes used in the transformation are rdf, rdfs, xsd, and owl, which should be expanded into 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.

As all OWL Lite constructs are special cases of constructs in the full abstract syntax, transformations are only provided for the full versions.

Each type of directive is translated via one of the transformation rules below. In the transformation rules nonterminals are enclosed in angle brackets. Repeating nonterminals are listed using ellipses, as in <description₁> … <description_n>, this form allows easy specification of the transformation for all values of n, including 0. Optional portions of the abstract syntax (enclosed in square brackets) are optional portions of the transformation (signified by square brackets).

The table below gives the transformation rules that transform the abstract syntax to the OWL exchange syntax. The left column gives a piece of syntax (S), the center column gives its transformation (T(S)), and the right column gives a node identifier that is the main node of the transformation (M(T(S))), but only for syntactic constructs that can occur as pieces of directives. 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 in a node position 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.

4.1. Definition of OWL/DL Ontologies in N-Triple Form

A collection of n-triples is an OWL/DL ontology in n-triple form if it is the result of the above transformation of an OWL ontology in abstract syntax form and, moreover,

1. the abstract syntax form does not use any URI reference as more than one of a classID, a datatypeID, an individualID, a datavaluedPropertyID, or an individualvaluedPropertyID;
2. the abstract syntax form does not use the URI of the document itself as a URI reference;
3. the abstract syntax form does not use any URI reference that is the first or second argument of an Annotation directive or an annotation portion of a directive as a classID, a datatypeID, an individualID, or a datavaluedPropertyID, nor does it use any URI reference that is the first argument of an Annotation directive or an annotation portion of a directive as an individualvaluedPropertyID; and
4. the abstract syntax form does not mention any of the URI references from the RDF, RDFS, or OWL namespaces except rdf:Literal, owl:Thing, and owl:Nothing.

This transformation is not injective, as several OWL abstract ontologies that do not use the above reserved vocabulary can map into the same collection of triples. 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.

5. RDFS-Compatible Model-Theoretic Semantics

This model-theoretic semantics for OWL is upward-compatible with the RDFS semantics as defined in the RDF model theory [RDF MT].

5.1. The OWL and RDFS universes

All of the OWL vocabulary is defined on the 'OWL universe', which is a collection of RDFS classes that are intended to circumscribe the domain of application of the OWL vocabulary: owl:Thing, owl:Class and owl:Property. The RDFS class extension of owl:Thing comprises the individuals of the OWL universe. The RDFS class extension of owl:Class comprises the classes of the OWL universe. The RDFS 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 here, these three classes are identified with their RDFS counterparts. In OWL/Full, as in RDFS, resources 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, these three classes 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. Further, OWL/DL can be processed by efficient DL reasoners. 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 OWL universe. In OWL/Full, no care is needed, as the OWL universe is the same as the RDFS universe. In OWL/DL, typing 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 n-triples close attention must be paid to which parts of the vocabulary can be 'legally' used to refer to things in the OWL universe.

5.1.1. Qualified Names and URI References

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, the datatypes of D, that have class extensions that are subsets of LV and mappings from literal strings to elements of their class extension. A typed literal string is a pair, d,s, consisting of a datatype and a literal string. For d,s a typed literal string, D(d,s) is the element of LV that is the literal value for string s in datatype d.

5.2. OWL Interpretations

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, an RDFS interpretation over V is a triple I = < R_I, EXT_I, S_I >. Here R_I is the domain of discourse or universe, i.e., a set that contains the denotations of URI references. EXT_I is used to give meaning to properties, and is a mapping from R_I to sets of pairs over R_I × (R_I∪LV). Finally, S_I is a mapping from V to R_I that takes a URI reference to its denotation. CEXT_I is then defined as CEXT_I(c) = { x∈R_I | <x,c>∈EXT_I(S_I(rdf:type)) }. RDFS interpretations must meet several conditions, as detailed in the RDFS model theory. For example, S_I(rdfs:subClassOf) must be a transitive relation.

An OWL interpretation, I = < R_I, EXT_I, S_I >, over a vocabulary V, where V includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing, is an RDFS interpretation over V that satisfies the following conditions:

Relationships between OWL classes

Membership in OWL classes

Characteristics of members of OWL classes

The next constraints are IFF, which may be harder to deal with in OWL/DL, as they extend the various categories of properties to all of owl:Property. However, in OWL/DL ontologies you can neither state that an owl:DatatypeProperty is inverse functional nor ask whether it is, so there should be not adverse consequences.

RDFS domains and ranges are strengthened to if-and-only-if over the OWL universe.

Some OWL properties have iff characterizations

Some OWL properties have only-if characterizations

We will say that l₁ is a sequence of y₁,…,y_n over C iff n=0 and l₁=S_I(rdf:nil) or n>0 and l₁∈IL and ∃ l₂, …, l_n ∈ IL such that
<l₁,y₁>∈EXT_I(S_I(rdf:first)), y₁∈CEXT_I(C), <l₁,l₂>∈EXT_I(S_I(rdf:rest)), …,
<l_n,y_n>∈EXT_I(S_I(rdf:first)), y_n∈CEXT_I(C), and <l_n,S_I(rdf:nil)>∈EXT_I(S_I(rdf:rest)).

R_I contains elements corresponding to all possible OWL descriptions and data ranges

The first three conditions require the existence of the finite sequences that are used in some OWL constructs. The remaining conditions require the existence of the OWL descriptions and data ranges.

5.3. OWL/DL

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 objects 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.

A OWL/DL interpretation over a vocabulary V', where V' includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing, is an OWL interpretation as above that satisfies the following conditions.

The domain of discourse is divided up into several pieces.

5.3.1. OWL/DL Entailment

Now entailment in OWL/DL can be defined.

Let K be an RDF graph and let V be a vocabulary that includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing. An OWL/DL interpretation of K is an OWL/DL interpretation over V that is also an RDFS interpretation of K.

Let K be a set of n-triples. 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 is the empty URI and y is any URI then the imports closure of K contains the n-triples resulting from the RDF parsing of the document, if any, accessible at y into n-triples.

Let K and Q be collections of n-triples and let V be a vocabulary that includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing. Then K OWL/DL entails Q whenever all OWL/DL interpretations of the RDF graph specified by imports closure of K are also OWL/DL interpretations of the RDF graph specified by imports closure of Q.

5.3.2. Correspondence to the Direct Semantics

One way to automatically obtain typing information for the vocabulary is to use translations into n-triples of certain kinds of OWL ontologies in the abstract syntax, as such translations contain information on which kind of entity a URI reference denotes. This is made more formal below.

A separated OWL vocabulary, V', is a set of URI references with a disjoint partition 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 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, <individualvaluedPropertyIDs> are taken from VOP, and <datavaluedPropertyID>s are taken from VDP.

Let T be the mapping from OWL ontologies in the abstract syntax to n-triples. 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.

5.4. OWL/Full

OWL/Full augments the common conditions with conditions that force the OWL and RDFS universes to be the same.

A OWL/Full interpretation over a vocabulary V, where V includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing, is an OWL interpretation as above that satisfies the following conditions.

OWL/Full entailment is defined in same manner as OWL/DL entailment.

Let K,C be collections of n-triples 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.

Appendix A. Proofs (Informative)

This appendix contains proofs of theorems contained in the document.

A.1 Correspondence between Abstract OWL and OWL/DL

This section shows that the two semantics for OWL/DL correspond on certain OWL knowledge bases. One semantics used in this section is the direct model theory for abstract OWL knowledge bases 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 elements of their class extension.
Throughout this section T will be the mapping from OWL abstract knowledge bases to n-triples.

A separated OWL vocabulary is a set of URI references V with a disjoint partition 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 set of n-triples that contains exactly <v,rdf:type,owl:Thing > for v ∈ VI, <v,rdf:type,owl:Class > for v ∈ VC, <v,rdf:type,owl: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 knowledge bases 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.

A.1.1 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,S,EC,ER> be an abstract OWL interpretation over V'.
Let I = <R_I,S_I,EXT_I> be an OWL/DL interpretation over V of T(V'). Let CEXT_I have its usual meaning.
If R=CEXT_I(S_I(owl:Thing)), S(v)=S_I(v) for v ∈ VI, EC(v)=CEXT_I(S_I(v)) for v∈VC∪VD, and ER(v)=EXT_I(S_I(v)) for v∈VOP∪VDP
then for d any abstract OWL description or data range over V', I OWL/DL satisfies T(d) and
for any E mapping all the blank nodes of T(d) into R_I where I+E OWL/DL satisfies T(d),

1. CEXT_I(S_I(M(T(d)))) = EC(d),
2. if d is a description then S_I(M(T(d)))∈CEXT_I(S_I(owl:Class)), and
3. if d is a data range then S_I(M(T(d)))∈CEXT_I(S_I(owl:Datatype)).

Proof

The proof of the lemma is by a structural induction. Throughout the proof, let IOT = CEXT_I(S_I(owl:Thing)), IOC = CEXT_I(S_I(owl:Class)), IDC = CEXT_I(S_I(owl:Datatype)), IOOP = CEXT_I(S_I(owl:ObjectProperty)), IODP = CEXT_I(S_I(owl:DatatypeProperty)), and IL = CEXT_I(S_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 the n-triples of T(d) contains n-triples for each of the sub-constructs that do not share any blank nodes with n-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,S_I(owl:Thing)>∈EXT_I(S_I(rdfs:domain)) and <p,S_I(owl:Thing)>∈EXT_I(S_I(rdfs:range)). Thus I satisfies T(p). Similarly for p∈VDP.

Base Case: v ∈ VC, including owl:Thing and owl:Nothing

As v∈VC and I satisfies T(V), thus S_I(v)∈CEXT_I(S_I(owl:Class)). Because I is an OWL/DL interpretation CEXT_I(S_I(v))⊆IOT, so <S_I(v),S_I(owl:Thing)>∈EXT_I(S_I(rdfs:subClassOf)). Thus I OWL/DL satisfies T(v). As M(T(v)) is v, thus CEXT_I(S_I(M(T(v))))=EC(v). Finally, from above, S_I(v)∈IOC.

Base Case: v ∈ VD, including rdfs:Literal

As v∈VD and I satisfies T(V), thus S_I(v)∈CEXT_I(S_I(owl:Datatype)). Because I is an OWL/DL interpretation CEXT_I(S_I(v))⊆LV, so <S_I(v),S_I(rdfs:Literal)>∈EXT_I(S_I(rdfs:subClassOf)). Thus I OWL/DL satisfies T(v). As M(T(v)) is v, thus CEXT_I(S_I(M(T(v))))=EC(v). Finally, from above S_I(v)∈IDC.

Base Case: d=oneOf(i₁…i_n), where the i_j are individual IDs

As i_j∈VI for 1≤j≤n and I satisfies T(V), thus S_I(i_j)∈IOT. The second comprehension principle for sequences then requires that there is some l∈IL that is a sequence of S_I(i₁),…,S_I(i_n) over IOT. For any l that is a sequence of S_I(i₁),…,S_I(i_n) over IOT the comprehension principle for oneOf requires that there is some y∈CEXT_I(S_I(rdfs:Class)) such that <y,l> ∈ EXT_I(IS(owl:oneOf)). From the third characterization of oneOf, y∈IOC. Therefore I satisfies T(d). For any I+E that satisfies T(d), CEXT_I(I+E(M(T(d)))) = {S_I(i₁),…,S_I(i_n)} = EC(d). Finally, I+E(M(T(d)))∈IOC.

Base Case: d=oneOf(v₁…v_n), where the vi are typed data values

As v_j is a typed data value for 1≤j≤n S_I(v_j)∈LV. The second comprehension principle for sequences then requires that there is some l∈IL that is a sequence of S_I(v₁),…,S_I(v_n) over LV. For any l that is a sequence of S_I(v₁),…,S_I(v_n) over LV the comprehension principle for oneOf requires that there is some y∈CEXT_I(S_I(rdfs:Class)) such that <y,l> ∈ EXT_I(IS(owl:oneOf)). From the second characterization of oneOf, y∈IOC. Therefore I satisfies T(d). For any I+E that satisfies T(d), CEXT_I(I+E(M(T(d)))) = {S_I(i₁),…,S_I(i_n)} = EC(d). Finally, I+E(M(T(d)))∈IDC.

Base Case: d=restriction(p value(i)), with p∈VOP∪VDP and i an individualID

As p∈VOP∪VDP, from above I satisfies T(p). As I satisfies T(V'), S_I(p)∈IOOP∪IODP. As i∈VI and I satisfies T(V'), S_I(i)∈IOT. From a comprehension principle for restriction, I satisfies T(d). For any E such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = { x∈IOT | <x,S_I(i)> ∈ EXT_I(p) } = { x∈R | <x,S(i)> ∈ ER(p) } = EC(d). Finally, I+E(M(T(d)))∈IOC.

Base Case: d=restriction(p value(i)), with p∈VOP∪VDP and i a typed data value.

Similar.

Base Case: d=restriction(p minCardinality(n)), with p∈VOP∪VDP and n a non-negative integer

Similar.

Base Case: d=restriction(p maxCardinality(n)), with p∈VOP∪VDP and n a non-negative integer

Similar.

Base Case: d=restriction(p Cardinality(n)), with p∈VOP∪VDP and n a non-negative integer

Similar.

Inductive Case: d=complementOf(d')

From the induction hypothesis, I satisfies T(d'). As d' is a description, from the induction hypothesis any extension of I, I+E, that satisfies T(d') has has I+E(M(T(d'))) = EC(d') and I+E(M(T(d')))∈IOC. The comprehension principle for complementOf then requires that there is a y∈IOC such that I+E satisfies <y,e>∈EXT_I(S_I(owl:complementOf)) so I satisfies T(d). For any I+E that satisfies T(d), CEXT_I(I+E(M(T(d)))) = IOT-CEXT_I(I+E(M(T(d)))) = R-EC(d') = EC(d). Finally, I+E(M(T(d)))∈IOC.

Inductive Case: d = unionOf(d₁ … d_n)

From the induction hypothesis, I satisfies d_i for ₁≤i≤n so there is an extension of I, E_i, that maps all the blank nodes in T(d_i) into domain elements such that I+E_i satisfies T(d_i). As the blank nodes in T(d_i) are disjoint from the blank nodes of T(d_j) for i≠j, I+E₁+…+E_n, and thus I, satisfies T(d_i)∪…∪T(d_n). Each d_i is a description, so from the induction hypothesis, I+E₁+…+E_n(M(T(d_i)))∈IOC. The first comprehension principle for sequences then requires that there is some l∈IL that is a sequence of I+E₁+…+E_n(M(T(d₁))),…, I+E₁+…+E_n(M(T(d_n))) over IOC. The comprehension principle for unionOf then requires that there is some y∈IOC such that <y,l>∈EXT_I(S_I(owl:unionOf)) so I satisfies T(d).
For any I+E that satisfies T(d), I+E satisfies T(d_i) so CEXT_I(I+E(d_i)) = EC(d_i)). Then CEXT_I(I+E(M(T(d)))) = CEXT_I(I+E(d₁))∪…∪CEXT_I(I+E(d_n)) = EC(d₁)∪…∪EC(d_n) = EC(d). Finally, S_I(M(T(d)))∈IOC.

Inductive Case: d = intersectionOf(d₁ … d_n)

Similar.

Inductive Case: d = restriction(p x₁ x₂ … x_n)

As p∈VOP∪VDP, from above I satisfies T(p). From the induction hypothesis, I satisfies restriction(p x_i) for ₁≤i≤n so there is an extension of I, E_i, that maps all the blank nodes in T(restriction(p x_i)) into domain elements such that I+E_i satisfies T(restriction(p x_i)). As the blank nodes in T(restriction(p x_i)) are disjoint from the blank nodes of T(restriction(p x_j)) for i≠j, I+E₁+…+E_n, and thus I, satisfies T(restriction(p x₁))∩…∩T(restriction(p x_n)). Each restriction(p x_i) is a description, so from the induction hypothesis, M(T(restriction(p x_i)))∈IOC. The first comprehension principle for sequences then requires that there is some l∈IL that is a sequence of I+E₁+…+E_n(M(T(restriction(p x_i))),…, I+E₁+…+E_n(M(T(restriction(p x_i))) over IOC. The comprehension principle for intersectionOf then requires that there is some y∈IOC such that <y,l>∈EXT_I(S_I(owl:intersectionOf)) so I satisfies T(d).
For any I+E that satisfies T(d) I+E satisfies T(d_i) so CEXT_I(I+E(d_i)) = EC(d_i)). Then CEXT_I(I+E(M(T(d)))) = CEXT_I(I+E(restriction(p x_i)))∩…∩ CEXT_I(I+E(restriction(p x_n))) = EC(restriction(p x_i))cup;…∪EC(restriction(p x_i)) = EC(d). Finally, S_I(M(T(d)))∈IOC.

Inductive Case: d = restriction(p allValuesFrom(d')), with p∈VOP∪VDP and d' a description

As p∈VOP∪VDP, from above I satisfies T(p). From the induction hypothesis, I satisfies T(d'). As d' is a description, from the induction hypothesis, any extension of I, I+E, that satisfies T(d') has I+E(M(T(d'))) = EC(d') and I+E(M(T(d')))∈IOC. As p∈VOP∪VDP and I satisfies T(V'), S_I(p)∈IOOP∪IODP. A comprehension principle for restriction then requires that I satisfies the n-triples in T(d) that are not in T(d') or T(p) in a way that shows that I satisfies T(d).
For any I+E that satisfies T(d), CEXT_I(I+E(M(T(d)))) = {x∈IOT | ∀ y∈IOT : <x,y>∈EXT_I(p) → y∈CEXT_I(M(T(d')))} = {x∈R | ∀ y∈R : <x,y>∈ER(p) → y∈EC(d')} = EC(d). Finally, I+E(M(T(d)))∈IOC.

Inductive Case: d = restriction(p someValuesFrom(d)) with p∈VOP∪VDP and d' a description

Similar.

Inductive Case: d = restriction(p allValuesFrom(d)) with p∈VOP∪VDP and d' a data range

Similar.

Inductive Case: d = restriction(p someValuesFrom(d)) with p∈VOP∪VDP and d' a data range

Similar.

A.1.2 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

Case: D = Class(foo complete d₁ … d_n).

Let d=intersectionOf(d₁ … d_n). As d is a description over V', thus I satisfies T(d) and for any E mapping the blank nodes of T(d) such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = EC(d). Thus for some E mapping the blank nodes of T(d) such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = EC(d) and I+E(M(T(d))∈IOC.

If I' satisfies D then EC(foo) = EC(d). From above, there is some E such that CEXT_I(I+E(M(T(d)))) = EC(d) = EC(foo) = CEXT_I(S_I(foo)) and I+E(M(T(d))∈IOC. Because I satisfies T(V), S_I(foo))∈IOC, thus <S_I(foo),I+E(M(T(d)))> ∈ EXT_I(S_I(owl:sameClassAs)). Therefore I satisfies T(D).

If I satisfies T(D) then I satisfies T(intersectionOf(d₁ … d_n)). Thus there is some E as above such that <S_I(foo),I+E(M(T(d)))> ∈ EXT_I(S_I(owl:sameClassAs)). Thus EC(d) = CEXT_I(I+E(M(T(d)))) = CEXT_I(S_I(foo)) = EC(foo). Therefore I' satisfies D.

Case: D = Class(foo partial d₁ … d_n)

Let d=intersectionOf(d₁ … d_n). As d is a description over V', thus I satisfies T(d) and for any E mapping the blank nodes of T(d) such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = EC(d). Thus for some E mapping the blank nodes of T(d) such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = EC(d) and I+E(M(T(d))∈IOC.

If I' satisfies D then EC(foo) ⊆ EC(d) From above, there is some E such that CEXT_I(I+E(M(T(d)))) = EC(d) ⊇ EC(foo) = CEXT_I(S_I(foo)) and I+E(M(T(d))∈IOC. Because I satisfies T(V), S_I(foo))∈IOC, thus <S_I(foo),I+E(M(T(d)))> ∈ EXT_I(S_I(rdfs:subClassOf)). Therefore I satisfies T(D).

If I satisfies T(D) then I satisfies T(intersectionOf(d₁ … d_n)). Thus there is some E as above such that <S_I(foo),I+E(M(T(d)))> ∈ EXT_I(S_I(rdfs:subClassOf)). Thus EC(d) = CEXT_I(I+E(M(T(d)))) ⊇ CEXT_I(S_I(foo)) = EC(foo). Therefore I' satisfies D.

Case: D = EnumeratedClass(foo i₁ … i_n)

Let d=oneOf(i₁ … i_n). As d is a description over V' so I satisfies T(d) and for some E mapping the blank nodes of T(d) such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = EC(d).

If I' satisfies D then EC(foo) = EC(d). From above, there is some E such that CEXT_I(I+E(M(T(d)))) = EC(d) = EC(foo) = CEXT_I(S_I(foo)) and I+E(M(T(d))∈IOC. Because I satisfies T(V), S_I(foo))∈IOC, thus <S_I(foo),I+E(M(T(d)))> ∈ EXT_I(S_I(owl:sameClassAs)). Therefore I satisfies T(D).

If I satisfies T(D) then I satisfies T(intersectionOf(d₁ … d_n)). Thus there is some E as above such that <S_I(foo),I+E(M(T(d)))> ∈ EXT_I(S_I(owl:sameClassAs)). Thus EC(d) = CEXT_I(I+E(M(T(d)))) = CEXT_I(S_I(foo)) = EC(foo). Therefore I' satisfies D.

Case: D= DisjointClasses(d₁ … d_n)

As d_i is a description over V' therefore I satisfies T(d_i) and for any E mapping the blank nodes of T(d_i) such that I+E satisfies T(d_i), CEXT_I(I+E(M(T(d_i)))) = EC(d_i).

If I satisfies T(D) then for each 1≤i≤n there is some E_i such that I satisfies <I+E_i(M(T(d_i))),I+E_j(M(T(d_j)))> ∈ EXT_I(S_I(owl:disjointWith)) for each 1≤i<j≤n. Thus EC(d_i)∩EC(d_j) = {}, for i≠j. Therefore I' satisfies D.

If I' satisfies D then EC(d_i)∪EC(d_j) = {} for i≠j. For any E_i and E_j as above <I+E_i+E_j(M(T(d_i))),I+E_i+E_j(M(T(d_j)))< ∈ EXT_I(S_I(owl:disjointWith)), for i≠j. As at least one E_i exists for each i, and the blank nodes of the T(d_j) are all disjoint, I+E₁+…+E_n satisfies T(DisjointClasses(d₁ … d_n)). Therefore I satisfies T(D).

Case: D = EquivalentClasses(d₁ … d_n)

Similar.

Case: D = SubClassOf(d₁ d2)

Somewhat similar.

Case: D = IndividualProperty(p super(s₁) … super(sn) domain(d₁) … domain(d_m) range(r₁) … range(r_l) [inverse(i)] [Symmetric] [Functional] [InverseFunctional] [OneToOne] [Transitive])

As d_i for 1≤i≤m is a description over V' therefore I satisfies T(d_i) and for any E mapping the blank nodes of T(d_i) such that I+E satisfies T(d_i), CEXT_I(I+E(M(T(d_i)))) = EC(d_i). Similarly for r_i for 1≤i≤l.

If I' satisfies D, then, as p∈VOP, I satisfies S_I(p)∈IOOP. Then, as I is an OWL/DL interpretation, I satisfies <S_I(p),S_I(owl:Thing)>∈EXT_I(S_I(rdfs:domain)) and <S_I(p),S_I(owl:Thing)>∈EXT_I(S_I(rdfs:range)). Also, ER(p)⊆ER(s_i) for 1≤i≤n, so EXT_I(S_I(p))=ER(p) ⊆ ER(s_i)=EXT_I(S_I(s_i)) and I satisfies <S_I(p),S_I(s_i)>∈EXT_I(S_I(rdfs:subPropertyOf)). Next, ER(p)⊆EC(d_i)×R for 1≤i≤m, so <z,w>∈ER(p) → z∈EC(d_i) and for any E such that I+E satisfies T(d_i), <z,w>∈EXT_I(p) → z∈CEXT_I(I+E(M(T(d_i)))) and thus <S_I(p),I+E(M(T(d_i)))>∈EXT_I(S_I(rdfs:domain)). Similarly for r_i) for 1≤i≤l.

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>∈EXT_I(p) iff <v,u>∈EXT_I(i) and I satisfies <S_I(p),S_I(i)>∈EXT_I(S_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> ∈ EXT_I(p) then <y, x>∈EXT_I(p). and thus I satisfies p∈CEXT_I(S_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, <S_I(p),S_I(s_i)>∈EXT_I(S_I(rdfs:subPropertyOf)). so ER(p)=EXT_I(S_I(p)) ⊆ EXT_I(S_I(s_i))=ER(s_i). Also, for 1≤i≤m, for some E such that I+E satisfies T(d_i), <S_I(p),I+E(M(T(d_i)))>∈EXT_I(S_I(rdfs:domain)) so <z,w>∈EXT_I(p) → z∈CEXT_I(I+E(M(T(d_i)))). Thus <z,w>∈ER(p) → z∈EC(d_i) and ER(p)⊆EC(d_i)×R. Similarly for r_i) for 1≤i≤l.

If I satisfies T(D) and inverse(i) is in D, then I satisfies <S_I(p),S_I(i)>∈EXT_I(S_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 D and Symmetric is in D, then I satisfies p∈CEXT_I(S_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(D) then I' satisfies D.

Case: D = DataProperty(p super(s₁) … super(sn) domain(d₁) … domain(d_m) range(r₁) … range(r_l) [Functional])

Similar.

Case: D = EquivalentProperties(p₁ … p_n), for p_i∈VOP

As p_i∈VOP and I satisfies T(V'), S_I(p_i)∈IOP. If I satisfies T(D) then <S_I(p_i),S_I(p_j)> ∈ EXT_I(S_I(owl:samePropertyAs)), for each 1≤i<j≤n. Therefore EXT_I(p_i) = EXT_I(p_j), for each 1≤i<j≤n; CR(p_i) = CR(p_j), for each 1≤i<j≤n; and I' satisfies D.

If I' satisfies D then CR(p_i) = CR(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:samePropertyAs, <S_I(p_i),S_I(p_j)> ∈ EXT_I(S_I(owl:samePropertyAs)), for each 1≤i<j≤n. Thus I satisfies T(D).

Case: D = SubPropertyOf(p₁ p₂)

Somewhat similar, but simpler.

Case: D = SameIndividual(i₁ … i_n)

Similar to SamePropertyAs.

Case: D = DifferentIndividuals(i₁ … i_n)

Similar to SamePropertyAs.

Case: D = Individual(i type(t₁) … type(t_n) value(p₁ v₁) … value(p_n v_n))

If I satisfies T(D) then there is some E that maps each blank node in T(D) such that I+E satisfies T(D). A simple examination of T(D) shows that the mappings of E 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 class memberships and relationships true in D. The n-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).

A.1.3 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 = < R_I, EXT_I, S_I > over V that satisfies T(V') there is an abstract OWL interpretation I' over V' such that for any OWL abstract KB K over V, I' abstract OWL satisfies K iff I OWL/DL satisfies T(K).

Proof

1. Let CEXT_I be defined as usual from I. The required abstract OWL interpretation will be I' = < CEXT_I(S_I(owl:Thing)), S, EC, ER > where S(n) = S_I(n) for n∈VI, EC(n) = CEXT_I(S_I(n)) for n∈VC∪VD, and ER(n) = EXT_I(S_I(n)) for n∈VOP∪VDP.

2. 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.

3. Satisfying an abstract KB is just satisfying its directives and satisfying the translation of an abstract KB is just satisfying all the n-triples so I OWL/DL satisfies T(K) iff I' abstract OWL satisfies K.

A.1.4 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, S, EC, ER > over V' there is an OWL/DL interpretation I over V that satisfies T(V') such that for any abstract OWL KB K over V', I OWL/DL satisfies T(K) iff I' abstract OWL satisfies K.

Proof

1. Construct I = < R_I, EXT_I, S_I > as follows:
   • Let IOC be the OWL descriptions over V', i.e., C is part of the Herbrand universe of OWL syntax.
     Let OD be the OWL data ranges over V'.
     Let OP = VOP u VDP.
     Let OL be the finite sequences over U, over C, and over LV plus rdf:nil.
     Let OX = VRDFS∪VOWL - {rdf:nil}.
   • R_I = U ∪ IOC ∪ OD ∪ OP ∪ OL ∪ OX
   • Let S_I(n) = S(n) for n∈VI.
     Let S_I(n) = n for n∈V-VI.
   • For i∈U, EXT_I(i)={} and CEXT_I(i)={}.
     For c∈IOC, EXT_I(c)={} and CEXT_I(c)=EC(c).
     For d∈OD, EXT_I(d)={} and CEXT_I(d)=EC(d).
     For r∈OP, EXT_I(r)=ER(r) and CEXT_I(r)={}.
     For l∈OL, EXT_I(r)={} and CEXT_I(r)={}.
     
   • CEXT_I(rdf:first)={}, CEXT_I(rdf:rest)={}
     CEXT_I(rdf:nil)={}, EXT_I(rdf:nil)={}
     CEXT_I(rdf:List)=OL, EXT_I(rdf:List)={}
     <x,y> ∈ EXT_I(rdf:first) iff x∈OL and y is its first element
     <x,y> ∈ EXT_I(rdf:rest) iff x∈OL and y is its tail
   • owl:intersectionOf, owl:oneOf, owl:unionOf, owl:complementOf, owl:onProperty, owl:allValuesFrom, owl:someValuesFrom, owl:hasValue, owl:minCardinality, owl:maxCardinality, and owl:cardinality have empty class extensions and their extensions are as necessary to link the elements of IOC up with their parts.
2. CEXT_I(rdfs:range) = {};
   EXT_I(rdfs:range) = { <x,y> : x∈OP y∈IOC ∧ ∀ z, <w,z> ∈ EXT_I(x) → z ∈ CEXT_I(y); } ∪ [RDFS ranges]
   CEXT_I(rdfs:subClassOf) = {};
   EXT_I(rdfs:subClassOf) = { <x,y> : x,y∈IOC ∧ CEXT_I(x) ⊆ CEXT_I(y) } ∪ [RDFS subclasses]
   CEXT_I(rdfs:subPropertyOf) = {};
   EXT_I(rdfs:subPropertyOf) = { <x,y> : x,y∈OP ∧ EXT_I(x) ⊆ EXT_I(y) } ∪ [RDFS subproperties]
   CEXT_I(rdf:type) = {}, EXT_I(rdf:type) is determined by CEXT_I. Then I is an OWL/DL interpretation because the conditions for the class extensions in OWL/DL match up with the conditions for class-like OWL abstract syntax constructs.
3. 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.
4. Satisfying an abstract KB is just satisfying its directives and satisfying the translation of an abstract KB is just satisfying all the n-triples so I OWL/DL satisfies T(K) iff I' abstract OWL satisfies K.

A.1.5 Correspondence Theorem

Let V' be a separated OWL vocabulary. Let K,Q be abstract OWL knowledge bases 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 knowledge base 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 knowledge base 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.

A.2 Correspondence between OWL/DL and OWL/Full

This section contains a poof 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 a collection of n-triples. An OWL interpretation of of K is an OWL interpretation (from Section 5.2) that is an RDFS interpretation of K.

Lemma: Let K be an OWL KB in the abstract syntax with separated vocabulary. Then for every OWL interpretation of T(K) there is an OWL/DL interpretation (as in Section 5.3) of T(K), and vice versa.

Proof sketch: As all OWL/DL interpretations are OWL interpretations, the reverse direction is obvious.

Let I = < R_I, EXT_I, S_I > be an OWL interpretation of T(K). Let I' = < R_I', EXT_I', S_I' > be an OWL interpretation of T(K). Let R_I' = CEXT_I(S_I(owl:Thing)) + CEXT_I(S_I(owl:ObjectProperty)) + CEXT_I(S_I(owl:IndividualProperty)) + CEXT_I(S_I(owl:Class)) + CEXT_I(S_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 S_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 object 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: Let K,C be collections of n-triples 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.

Appendix B. Examples (Informative)

This appendix gives examples of the concepts developed in the rest of the document.

B.1 Examples of Mapping from Abstract Syntax to N-Triples

The transformation rules in Section 4 transform

  DatatypeProperty(ex:name)
  ObjectProperty(ex:author)
  Individual(type(ex:Book) (ex:author (Individual (ex:name xsd:string"Fred"))))

to

  [ex:name] [rdf:type] [owl:DatatypeProperty] .
  [ex:name] [rdfs:domain] [owl:Thing] .
  [ex:name] [rdfs:range] [rdfs:Literal] .

  [ex:author] [rdf:type] [owl:ObjectProperty] .
  [ex:author] [rdfs:domain] [owl:Thing] .
  [ex:author] [rdfs:range] [owl:Thing] .

  [ex:book] [rdf:type] [owl:Class] .
  [ex:book] [rdfs:subClassOf] [owl:Thing] .

  _:x [rdf:type] [owl:Thing] .
  _:x [rdf:type] [ex:Book] .
  _:x [ex:author] _:x1 .
  _:x1 [rdf:type] [owl:Thing] .
  _:x1 [ex:name] xsd:string"Fred" .

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:enrolledIn] [rdfs:domain] [owl:Thing] .
  [ex:enrolledIn] [rdfs:range] [owl:Thing] .

  [ex:Person] [rdf:type] [owl:Class] .
  [ex:Person] [rdf:subClassOf] [owl:Thing] .

  [ex:School] [rdf:type] [owl:Class] .
  [ex:School] [rdf:subClassOf] [owl:Thing] .

  [ex:Student] [rdf:type] [owl:Class] .
  [ex:Student] [rdf:subClassOf] [owl:Thing] .

  [ex:Student] [owl:sameClassAs] _:x .
  _:x [owl:intersectionOf] _:l1 .
  _:l1 [rdf:type] [rdf:List] .
  _:l1 [rdf:first]  [ex:Person] .
  _:l1 [rdf:rest] [rdf:nil] .
  _: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] xsd:decimal"1" .

B.2 Examples of Entailments in OWL/DL and OWL/Full

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 .

and so all this would need to be added explicitly as an antecedent in order to draw the conclusion

John rdf:type _:x .
_:x owl:onProperty friend .
_:x owl:minCardinality 1 .

However, once these extra conditions are 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 _:x .
_: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 .