W3C

A Model-Theoretic Semantics for DAML+OIL (March 2001)

W3C Note 18 December 2001

This version:
http://www.w3.org/TR/NOTE-daml+oil-model-20011218
Latest version:
http://www.w3.org/TR/daml+oil-model
Authors:
Frank van Harmelen
Ian Horrocks
Peter F. Patel-Schneider

Abstract

The meaning of DAML+OIL constructs is provided by this terse model-theoretic semantics.

Status of this document

This document is a submission to the World Wide Web Consortium from Lucent Technologies (see Submission Request, W3C Staff Comment).

Please send comments to Peter F. Patel-Schneider pfps@research.bell-labs.com, or, preferably, to the publicly archived distribution list, www-rdf-logic@w3.org [archive].

This document is a NOTE made available by the W3C for discussion only. Publication of this Note by W3C indicates no endorsement by W3C or the W3C Team, or any W3C Members. W3C has had no editorial control over the preparation of this Note. This document is a work in progress and may be updated, replaced, or rendered obsolete by other documents at any time.

A list of current W3C technical documents can be found at the Technical Reports page.

Table of contents

  1. Introduction
  2. Typographical conventions
  3. Semantics

1. Introduction

This document provides a terse specification of the model-theoretic semantics for DAML+OIL. A DAML+OIL ontology (or knowledge base) is a collection of RDF triples. Some of these triples are relevant to DAML+OIL and some are not. This semantics only treats the triples that are obviously relevant to DAML+OIL and ignores the rest.

This document says nothing about how the collection of RDF triples is obtained. This document ignores all aspects of naming and importing. Thus it has nothing to do with the meaning of Ontology or versionInfo or imports. (The intended meaning of imports is that the RDF triples of the referenced ontology are included in the RDF triples of the current ontology.)

2. Typographical conventions

In the document various typographical conventions are used to represent sets, set relationships, and other mathematical notations. These may not be the most elegant typographical conventions, but they should be renderable by just about all HTML browsers.

Names in this document are qualified if they come from other namespaces than the DAML+OIL namespace. Think of the names as if the following XML namespace definitions are present:

Several DAML+OIL constructs accept a list. The semantic mappings show these lists as [x1,...,xn] in the interests of brevity and clarity.

3. Semantics

The semantics uses a non-empty domain of discourse, AD, which is a collection of DAML+OIL objects. Added to this object domain is the datatype domain, DD, which is the intended model for XML Schema data types, disjointly unioned with an infinite collection of other values. The disjoint union of AD and DD is designated by UD.

The semantics assigns a meaning to various syntactic constructs by means of three interpretation functions:

Some nodes in a DAML+OIL ontology are XML Schema datatype definitions. Such nodes are mapped by IC into the appropriate subset of the datatype domain. (To recognize whether a node is an XML Schema datatype definition it is sufficient to determine whether it is within an XML Schema context. For the built-in XML Schema datatypes, it is also possible to recognize them by their standard URI.) Nodes that are instances of daml:Class are mapped into subsets of the object domain AD by IC. As a special case rdfs:Literal is mapped by IC into DD.

The IR mapping maps object properties into subsets of AD x AD and datatype properties into subsets of AD x DD.

The IO mapping maps RDF literals into subsets of DD. This subset must include all elements of DD that have the literal as a lexical representation for some XML Schema datatype. It must not include any element of DD that is in the interpretation of any XML Schema datatype and that does not have the literal as a lexical representation for any XML Schema datatype. Nodes whose type is an XML Schema datatype are mapped into subsets of the mapping of that XML Schema datatype. All other nodes are mapped into singleton subsets of AD.

There currently is no unique name assumption. A method for asserting the equality and inequality of individuals would be helpful. (Actually, this could be done by creating classes that imply that two individuals are the same or distinct, but a direct method would be better.)

The semantics is specified via mappings from syntactic structures to constraints on semantic structures. Most mappings have formal parameters signified by means of a leading ``?''. Some mappings require the presence of several triples.

Consider a DAML+OIL ontology in the form of a collection of RDF triples. A semantic structure <AD,IC,IO,IR> is a model for the DAML+OIL ontology if the constraints resulting from the mappings from the ontology are true in the structure.

First we include a few preliminary mappings. Some of the effects of these mappings follow from the setup of the semantic structure above and from the definitions in the syntax document, but are included here for emphasis.

Syntactic Structure Semantic Constraint
<rdf:type,?C,rdfs:Class> IC(?C) <= UD
<rdf:type,?C,Class> IC(?C) <= AD
<rdf:type,?C,Datatype> IC(?C) <= DD
<rdf:type,?C,Restriction> IC(?C) <= AD
<rdf:type,?R,Property> IR(?R) <= AD x UD
<rdf:type,?R,ObjectProperty> IR(?R) <= AD x AD
<rdf:type,?R,DatatypeProperty> IR(?R) <= AD x DD
  IC(Thing) = AD
  IC(Nothing) = { }
  IC(rdfs:Literal) = DD
?L for ?L a literal, IO(?L) <= DD and if x is in the interpretation of an XML Schema datatype then x in IO(?L) iff x has ?L as its lexical representation for some XML Schema datatype

Now for the real semantic mappings.

Syntactic Structure Semantic Constraint
<rdf:type,?O,?C> IO(?O) <= IC(?C)
<rdf:type,?O,?D> <rdf:value,?O,?L> <rdf:type,?L,rdfs:Literal> for ?D an XML Schema datatype, IO(?O) is the singleton set containing the element of IC(?D) that has lexical representation ?L, provided that there is one, otherwise IO(?O) = { }
<?R,?O1,?O2> <x,y> in IR(?R), for some x <=IO(?O1) and y <= IO(?O2), provided that IO(?O1) <= AD
<equivalentTo,?A,?B> IC(?A) = IC(?B)
IR(?A) = IR(?B)
IO(?A) = IO(?B)
<rdfs:subClassOf,?C,?D> IC(?C) <= IC(?D)
<rdfs:subPropertyOf,?R,?S> IR(?R) <= IR(?S)
<sameClassAs,?C,?D> IC(?C) = IC(?D)
<samePropertyAs,?R,?S> IR(?R) = IR(?S)
<sameIndividualAs,?A,?B> IO(?A) = IO(?B)
<disjointWith,?X,?Y> IC(?X) ^ IC(?Y) = { }
<differentIndividualFrom,?A,?B> IO(?A) ^ IO(?B) = { }
<unionOf,?C,[?X1,...,?Xn]> IC(?C) = ( IC(?X1) v ... v IC(?Xn) ) ^ AD
<disjointUnionOf,?C,[?X1,...,?Xn]> IC(?C) = ( IC(?X1) v ... v IC(?Xn) ) ^ AD
IC(?Xi) ^ IC(?Xj) = { } for 1<=i<j<=n
<intersectionOf,?C,[?X1,...,?Xn]> IC(?C) = IC(?X1) ^ ... ^ IC(?Xn) ^ AD
<complementOf,?X,?Y> IC(?X) ^ IC(?Y) = { }
IC(?X) v IC(?Y) = AD
<oneOf,?C,[?O1,...,?On]> IC(?C) = ( IO(?O1) v ... v IO(?On) ) ^ AD
<rdfs:domain,?P,?C> if <x,y> in IR(?P) then x in IC(?C)
<rdfs:range,?P,?C> if <x,y> in IR(?P) then y in IC(?C)
<inverseOf,?P,?S> for y in AD, <x,y> in IR(?P) iff <y,x> in IR(?S)
<rdf:type,?P,TransitiveProperty> for y in AD, if <x,y> in IR(?P) and <y,z> in IR(?P) then <x,z> in IR(?P)
<rdf:type,?P,UniqueProperty> if <x,y> in IR(?P) and <x,z> in IR(?P) then y=z
<rdf:type,?P,UnambiguousProperty> for y in AD, if <x,y> in IR(?P) and <z,y> in IR(?P) then x=z
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <toClass,?R,?C> x in IC(?R) iff IR(?P)({x}) <= IC(?C)
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <hasValue,?R,?V> x in IC(?R) iff | IR(?P)({x}) ^ IO(?V) | > 0
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <hasClass,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | > 0
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <minCardinality,?R,?n> x in IC(?R) iff | IR(?P)({x}) | >= ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <maxCardinality,?R,?n> x in IC(?R) iff | IR(?P)({x}) | <= ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <cardinality,?R,?n> x in IC(?R) iff | IR(?P)({x}) | = ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <minCardinalityQ,?R,?n> <hasClassQ,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | >= ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <maxCardinalityQ,?R,?n> <hasClassQ,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | <= ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <cardinalityQ,?R,?n> <hasClassQ,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | = ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <toClass,?R,?C> x in IC(?R) iff IR(?P)({x}) <= IC(?C)
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <hasValue,?R,?V> x in IC(?R) iff | IR(?P)({x}) ^ IC(?V) | > 0
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <hasClass,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | > 0
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <minCardinality,?R,?n> x in IC(?R) iff | IR(?P)({x}) | >= ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <maxCardinality,?R,?n> x in IC(?R) iff | IR(?P)({x}) | <= ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <cardinality,?R,?n> x in IC(?R) iff | IR(?P)({x}) | = ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <minCardinalityQ,?R,?n> <hasClassQ,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | >= ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <maxCardinalityQ,?R,?n> <hasClassQ,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | <= ?n
<rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <cardinalityQ,?R,?n> <hasClassQ,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | = ?n

References

  1. DAML+OIL (March 2001) reference description
  2. An Axiomatic Semantics for RDF, RDF-S, and DAML+OIL (March 2001)
  3. Annotated DAML+OIL Ontology Markup
  4. DAML+OIL revised language specification
  5. A sample ontology
  6. Datatype definitions for sample ontology