An RDFS-Compatible Model-Theoretic Semantics for DAML+OIL (March 2001)

Editors:: Peter F. Patel-Schneider

Abstract

The meaning of DAML+OIL constructs is provided by this terse model-theoretic semantics, which has been modified to follow the new model theory for RDF(S).

1. Introduction

This document provides a terse specification of a model theory for DAML+OIL, specified as an RDF graph. It is written in the same fashion as the recent model theory for RDF(S). However, it is not quite compatible with that model theory.

This document says nothing about how the RDF graph 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.)

This document has a slightly different treatment of literals and datatypes than does DAML+OIL (March 2001). There may be other differences, as well.

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.

<x1,...,xn> is an n-tuple with i'th element xi
X x Y is the cross product of X and Y
{x1,...,xn} is the set with elements xi
<= is the subset relationship
in is the element of relationship
^ is set intersection
v is set union
|.| is set cardinality
R(x) is the set of objects that form the image of x under R, for R a set of 2-tuples

Names in this document are qualified. Think of the names as if the following XML namespace definitions are present:

xmlns:rdf ="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
xmlns:xsd ="http://www.w3.org/2000/10/XMLSchema#"
xmlns:daml="http://www.daml.org/2001/03/daml+oil#"
xmlns: ="http://www.daml.org/2001/03/daml+oil#"

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

3. DAML+OIL Graph Syntax

A DAML+OIL graph is an untidy RDF graph.

A DAML+OIL vocabulary is an RDFS vocabulary with the following extra members:

daml:Class
daml:Datatype
daml:Thing
daml:Nothing
daml:equivalentTo
daml:sameClassAs
daml:samePropertyAs
daml:sameIndividualAs
daml:disjointWith
daml:differentIndividualFrom
daml:unionOf
daml:disjointUnionOf
daml:intersectionOf
daml:complementOf
daml:oneOf
daml:Restriction
daml:onProperty
daml:toClass
daml:hasValue
daml:hasClass
daml:minCardinality
daml:maxCardinality
daml:cardinality
daml:hasClassQ
daml:minCardinalityQ
daml:maxCardinalityQ
daml:cardinalityQ
daml:ObjectProperty
daml:DatatypeProperty
daml:inverseOf
daml:TransitiveProperty
daml:UniqueProperty
daml:UnambiguousProperty
daml:List
daml:nil
daml:first
daml:rest
daml:item

4. Interpretations

The datatype domain LV (called literals in RDF) for DAML+OIL is a set consisting of the (disjoint?) union of the value spaces of the primitive XML Schema data types. There is a map XLC from URIs to subsets of LV. URIs that ``point to'' an XML Schema datatype are mapped to the value space for the datatype by XLC. Other URIs are mapped to the empty set. There is a map XLS from RDF literals to subsets of LV that maps an RDF literal into the set of XML Schema datatype values that have the literal as a lexical representation. Note that each RDF literal is mapped into at least one XML Schema datatype value.

A DAML+OIL interpretation is an RDFS interpretation from the recent RDF(S) model theory over a DAML+OIL vocabulary and thus is a six-tuple <IR, IP, IC, IEXT, ICEXT, IS>, where

IR is the collection of resources,
IP is a subset of IR and the collection of properties,
IC is a subset of IR and the collection of classes,
IEXT is a mapping from IP to subsets of IR x ( IR v LV),
ICEXT is a mapping from IC to subsets of IR v LV, and
IS is a mapping from URIs to IR

satisfying several conditions as an RDFS interpretation except that the meaning of a node with a literal label is not determined by a fixed XL. Instead I(n), for n a node with label l, a literal, is only restricted to be an element of XLS(l). (Yes, this means that there are many ways of extending an interpretation to a DAML+OIL graph. This is not so nice, and there are ways of fixing this, but I'm trying to stay close to RDFS interpretations.)

A DAML+OIL interpretation must also satisfy the extra conditions given below.

First some extra conditions that mirror RDFS statments setting up the DAML+OIL built-in objects: [NB: Missing the definitions of Thing and Nothing.]

IS(daml:Class) in ICEXT(IS(rdfs:Class))
<IS(daml:Class),IS(rdfs:Class)> in IEXT(IS(rdfs:subClassOf))
IS(daml:Datatype) in ICEXT(IS(rdfs:Class))
<IS(daml:Datatype),IS(rdfs:Class)> in IEXT(IS(rdfs:subClassOf))
IS(daml:Thing) in ICEXT(IS(daml:Class))
IS(daml:Nothing) in ICEXT(IS(daml:Class)))
IS(daml:equivalentTo) in ICEXT(IS(rdf:Property))
IS(daml:sameClassAs) in ICEXT(IS(rdf:Property))
<IS(daml:sameClassAs),IS(daml:Class)> in IEXT(IS(rdfs:domain))
<IS(daml:sameClassAs),IS(daml:Class)> in IEXT(IS(rdfs:range))
IS(daml:samePropertyAs) in ICEXT(IS(rdf:Property))
<IS(daml:samePropertyAs),IS(daml:subPropertyOf)> in IEXT(IS(rdfs:subClassOf))
IS(daml:sameIndividualAs) in ICEXT(IS(rdf:Property))
<IS(daml:sameIndividualAs),IS(daml:Thing)> in IEXT(IS(rdfs:domain))
<IS(daml:sameIndividualAs),IS(daml:Thing)> in IEXT(IS(rdfs:range))
IS(daml:disjointWith) in ICEXT(IS(rdf:Property))
<IS(daml:disjointWith),IS(daml:Class)> in IEXT(IS(rdfs:domain))
<IS(daml:disjointWith),IS(daml:Class)> in IEXT(IS(rdfs:range))
IS(daml:differentIndividualFrom) in ICEXT(IS(rdf:Property))
<IS(daml:differentIndividualAs),IS(daml:Thing)> in IEXT(IS(rdfs:domain))
<IS(daml:differentIndividualAs),IS(daml:Thing)> in IEXT(IS(rdfs:range))
IS(daml:unionOf) in ICEXT(IS(rdf:Property))
<IS(daml:unionOf),IS(daml:Class)> in IEXT(IS(rdfs:domain))
<IS(daml:unionOf),IS(daml:List)> in IEXT(IS(rdfs:range))
IS(daml:disjointUnionOf) in ICEXT(IS(rdf:Property))
<IS(daml:disjointUnionOf),IS(daml:Class)> in IEXT(IS(rdfs:domain))
<IS(daml:disjointUnionOf),IS(daml:List)> in IEXT(IS(rdfs:range))
IS(daml:intersectionOf) in ICEXT(IS(rdf:Property))
<IS(daml:intersectionOf),IS(daml:Class)> in IEXT(IS(rdfs:domain))
<IS(daml:intersectionOf),IS(daml:List)> in IEXT(IS(rdfs:range))
IS(daml:complementOf) in ICEXT(IS(rdf:Property))
<IS(daml:complementOf),IS(daml:Class)> in IEXT(IS(rdfs:domain))
<IS(daml:complementOf),IS(daml:Class)> in IEXT(IS(rdfs:range))
IS(daml:oneOf) in ICEXT(IS(rdf:Property))
<IS(daml:oneOf),IS(daml:Class)> in IEXT(IS(rdfs:domain))
<IS(daml:oneOf),IS(daml:List)> in IEXT(IS(rdfs:range))
IS(daml:Restriction) in ICEXT(IS(daml:Class))
<IS(daml:Restriction),IS(daml:Class)> in IEXT(IS(rdfs:subClassOf))
IS(daml:onProperty) in ICEXT(IS(rdf:Property)
<IS(daml:onProperty),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:onProperty),IS(daml:Property)> in IEXT(IS(rdfs:range))
IS(daml:toClass) in ICEXT(IS(rdf:Property)
<IS(daml:toClass),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:toClass),IS(rdfs:Class)> in IEXT(IS(rdfs:range))
IS(daml:hasValue) in ICEXT(IS(rdf:Property)
<IS(daml:hasValue),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
IS(daml:hasClass) in ICEXT(IS(rdf:Property)
<IS(daml:hasClass),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:hasClass),IS(rdfs:Class)> in IEXT(IS(rdfs:range))
IS(daml:minCardinality) in ICEXT(IS(rdf:Property)
<IS(daml:minCardinality),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:minCardinality),IS(xsd:nonNegativeInteger)> in IEXT(IS(rdfs:range))
IS(daml:maxCardinality) in ICEXT(IS(rdf:Property)
<IS(daml:maxCardinality),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:maxCardinality),IS(xsd:nonNegativeInteger)> in IEXT(IS(rdfs:range))
IS(daml:cardinality) in ICEXT(IS(rdf:Property)
<IS(daml:cardinality),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:cardinality),IS(xsd:nonNegativeInteger)> in IEXT(IS(rdfs:range))
IS(daml:hasClassQ) in ICEXT(IS(rdf:Property)
<IS(daml:hasClassQ),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:hasClassQ),IS(rdfs:Class)> in IEXT(IS(rdfs:range))
IS(daml:minCardinalityQ) in ICEXT(IS(rdf:Property)
<IS(daml:minCardinalityQ),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:minCardinalityQ),IS(xsd:nonNegativeInteger)> in IEXT(IS(rdfs:range))
IS(daml:maxCardinalityQ) in ICEXT(IS(rdf:Property)
<IS(daml:maxCardinalityQ),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:maxCardinalityQ),IS(xsd:nonNegativeInteger)> in IEXT(IS(rdfs:range))
IS(daml:cardinalityQ) in ICEXT(IS(rdf:Property)
<IS(daml:cardinalityQ),IS(daml:Restriction)> in IEXT(IS(rdfs:domain))
<IS(daml:cardinalityQ),IS(xsd:nonNegativeInteger)> in IEXT(IS(rdfs:range))
IS(daml:ObjectProperty) in ICEXT(IS(rdfs:Class))
<IS(daml:ObjectProperty),IS(rdf:Property)> in IEXT(IS(rdfs:subClassOf))
IS(daml:DatatypeProperty) in ICEXT(IS(rdfs:Class))
<IS(daml:DatatypeProperty),IS(rdf:Property)> in IEXT(IS(rdfs:subClassOf))
IS(daml:inverseOf) in ICEXT(IS(rdf:Property))
<IS(daml:inverseOf),IS(daml:ObjectProperty)> in IEXT(IS(rdfs:domain))
<IS(daml:inverseOf),IS(daml:ObjectProperty)> in IEXT(IS(rdfs:range))
IS(daml:TransitiveProperty) in ICEXT(IS(rdf:Class))
<IS(daml:TransitiveProperty),IS(rdf:ObjectProperty)> in IEXT(IS(rdfs:subClassOf))
IS(daml:UniqueProperty) in ICEXT(IS(rdf:Class))
<IS(daml:UniqueProperty),IS(rdf:Property)> in IEXT(IS(rdfs:subClassOf))
IS(daml:UnambiguousProperty) in ICEXT(IS(rdf:Class))
<IS(daml:UnambiguousProperty),IS(rdf:ObjectProperty)> in IEXT(IS(rdfs:subClassOf))
IS(daml:List) in ICEXT(IS(rdfs:Class))
IS(daml:nil) in ICEXT(IS(daml:List))
IS(daml:first) in ICEXT(IS(rdf:Property))
<IS(daml:first),IS(daml:List)> in IEXT(IS(rdfs:domain))
IS(daml:rest) in ICEXT(IS(rdf:Property))
<IS(daml:rest),IS(daml:List)> in IEXT(IS(rdfs:domain))
<IS(daml:rest),IS(daml:List)> in IEXT(IS(rdfs:range))
IS(daml:item) in ICEXT(IS(rdf:Property))
<IS(daml:item),IS(daml:List)> in IEXT(IS(rdfs:domain))

Now for the real semantic conditions:

IR and LV are disjoint
if c in ICEXT(IS(daml:Class)) then ICEXT(c) <= IR
if c in ICEXT(IS(daml:Datatype)) then ICEXT(c) = XLC(c)
if r in ICEXT(IS(daml:ObjectProperty)) then IEXT(r) <= IR x IR
if r in ICEXT(IS(daml:DatatypeProperty)) then IEXT(r) <= IR x LV
ICEXT(IS(daml:Thing)) = IR
ICEXT(IS(daml:Nothing)) = { }
if <a,b> in IEXT(IS(daml:equivalentTo)) then a = b
if <c,d> in IEXT(IS(daml:sameClassAs)) then ICEXT(c) = ICEXT(d)
if <r,s> in IEXT(IS(daml:samePropertyAs)) then IEXT(r) = IEXT(s)
if <a,b> in IEXT(IS(daml:sameIndividualAs)) then a = b
if <x,y> in IEXT(IS(daml:disjointWith)) then ICEXT(x) ^ ICEXT(y) = { }
if <a,b> in IEXT(IS(daml:differentIndividualFrom)) then I(a) ~= I(b)
if <c,[x1,...,xn]> in IEXT(IS(daml:unionOf))
then ICEXT(c) = ( ICEXT(x1) v ... v ICEXT(xn) ) ^ IR
if <c,[x1,...,xn]> in IEXT(IS(daml:disjointUnionOf))
then ICEXT(c) = ( ICEXT(x1) v ... v ICEXT(xn) ) ^ IR
and ICEXT(xi) ^ ICEXT(xj) = { } for 1<=i<j<=n
if <c,[x1,...,xn]> in IEXT(IS(daml:intersectionOf))
then ICEXT(c) = ICEXT(x1) ^ ... ^ ICEXT(xn) ^ IR
if <x,y> in IEXT(IS(daml:complementOf))
then ICEXT(x) ^ ICEXT(y) = { }
and ICEXT(x) v ICEXT(y) = IR
if <c,[o1,...,on]> in IEXT(IS(daml:oneOf))
then ICEXT(c) = { I(o1), ..., I(on) } ^ IR
if <p,s> in IEXT(IS(daml:inverseOf))
then for y in IR, <x,y> in IEXT(p) iff <y,x> in IEXT(s)
if p in ICEXT(IS(daml:TransitiveProperty)), <x,y> in IEXT(p), and <y,z> in IEXT(p)
then <x,z> in IEXT(p)
if p in ICEXT(IS(daml:UniqueProperty)), <x,y> in IEXT(p), and <x,z> in IEXT(p)
then y=z
if p in ICEXT(IS(daml:UnambiguousProperty)), <x,y> in IEXT(p), and <z,y> in IEXT(p)
then x=z
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:ObjectProperty)), and <r,p> in IEXT(IS(daml:toClass))
then ICEXT(r) = { x in IR : IEXT(p)({x}) <= ICEXT(c) }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:ObjectProperty)), and <r,v> in IEXT(IS(daml:hasValue))
then ICEXT(r) = { x in IR : v in IEXT(p)({x}) }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:ObjectProperty)), and <r,c> in IEXT(IS(daml:hasClass))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) ^ ICEXT(c) |> 0 }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:ObjectProperty)), and <r,n> in IEXT(IS(daml:minCardinality))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) | >= n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:ObjectProperty)), and <r,n> in IEXT(IS(daml:maxCardinality))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) | <= n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:ObjectProperty)), and <r,n> in IEXT(IS(daml:cardinality))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) | = n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:ObjectProperty)), <r,n> in IEXT(IS(daml:minCardinalityQ)), and <r,c> in IEXT(IS(daml:hasClassQ))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) ^ ICEXT(c) | >= n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:ObjectProperty)), <r,n> in IEXT(IS(daml:maxCardinalityQ)), and <r,c> in IEXT(IS(daml:hasClassQ))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) ^ ICEXT(c) | <= n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:ObjectProperty)), <r,n> in IEXT(IS(daml:cardinalityQ)), and <r,c> in IEXT(IS(daml:hasClassQ))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) ^ ICEXT(c) | = n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:DatatypeProperty)), and <r,p> in IEXT(IS(daml:toClass))
then ICEXT(r) = { x in IR : IEXT(p)({x}) <= ICEXT(c) }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:DatatypeProperty)), and <r,v> in IEXT(IS(daml:hasValue))
then ICEXT(r) = { x in IR : v in IEXT(p)({x}) }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:DatatypeProperty)), and <r,c> in IEXT(IS(daml:hasClass))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) ^ ICEXT(c) |> 0 }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:DatatypeProperty)), and <r,n> in IEXT(IS(daml:minCardinality))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) | >= n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:DatatypeProperty)), and <r,n> in IEXT(IS(daml:maxCardinality))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) | <= n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:DatatypeProperty)), and <r,n> in IEXT(IS(daml:cardinality))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) | = n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:DatatypeProperty)), <r,n> in IEXT(IS(daml:minCardinalityQ)), and <r,c> in IEXT(IS(daml:hasClassQ))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) ^ ICEXT(c) | >= n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:DatatypeProperty)), <r,n> in IEXT(IS(daml:maxCardinalityQ)), and <r,c> in IEXT(IS(daml:hasClassQ))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) ^ ICEXT(c) | <= n }
if r in ICEXT(IS(daml:Restriction)), <r,p> in IEXT(IS(daml:onProperty)), p in ICEXT(IS(daml:DatatypeProperty)), <r,n> in IEXT(IS(daml:cardinalityQ)), and <r,c> in IEXT(IS(daml:hasClassQ))
then ICEXT(r) = { x in IR : | IEXT(p)({x}) ^ ICEXT(c) | = n }

6. Models

A model of a DAML+OIL graph, G, is a DAML+OIL interpretation, I, for which I(G) = true.

5. Incompatibilities with the RDF Model Theory

There are the following incompatibilities with the RDF Model Theory:

the meaning of nodes with literal labels
ICEXT cannot be tied to IEXT(IS(rdf:type))
IR and LV are disjoint