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

Editors:: Peter F. Patel-Schneider

Abstract

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

1. Introduction

This document provides a terse specification of a model theory for DAML+OIL (March 2001), specified as an RDF graph. It builds directly on my variant of the new model theory for RDF(S).

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. They should be expanded to a collection of nodes and edges that use daml:List, daml:first, daml:rest, and daml:nil and that represents the list.

3. DAML+OIL Graph Syntax

A DAML+OIL graph is a core RDFS graph that contains nodes with the following labels:

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

and has the following edges (being a little bit lazy in using labels to identify nodes):

<daml:Class, rdf:type, rdfs:Class>
<daml:Class, rdfs:subClassOf, rdfs:Class>
<daml:Datatype, rdf:type, rdfs:Class>
<daml:Datatype, rdfs:subClassOf, rdfs:Class>
<daml:Thing, rdf:type, daml:Class>
for some r1 <daml:Thing,daml:unionOf,r1>
<r1, rdf:type, daml:List>
<r1, daml:first, daml:Nothing>
for some r2 <r1, daml:rest, r2>
<r2, rdf:type, daml:List>
for some c <r2, daml:first, c>
<c, rdf:type, daml:Class>
<c, daml:complementOf, daml:Nothing>
<r2, daml:rest, daml:nil>
<daml:Nothing, rdf:type, daml:Class>
<daml:Nothing, daml:complementOf, daml:Thing>
<daml:equivalentTo, rdf:type, rdf:Property>
<daml:sameClassAs, rdf:type, rdf:Property>
<daml:sameClassAs, rdfs:subPropertyOf, daml:equivalentTo>
<daml:sameClassAs, rdfs:subPropertyOf, rdfs:subClassOf>
<daml:sameClassAs, rdfs:domain, daml:Class>
<daml:sameClassAs, rdfs:range, daml:Class>
<daml:samePropertyAs, rdf:type, rdf:Property>
<daml:samePropertyAs, rdfs:subPropertyOf, daml:equivalentTo>
<daml:samePropertyAs, rdfs:subPropertyOf, rdfs:subClassOf>
<daml:sameIndividualAs, rdf:type, rdf:Property>
<daml:sameIndividualAs, rdfs:subPropertyOf, daml:equivalentTo>
<daml:sameIndividualAs, rdfs:domain, daml:Thing>
<daml:sameIndividualAs, rdfs:range, daml:Thing>
<daml:disjointWith, rdf:type, rdf:Property>
<daml:disjointWith, rdfs:domain, daml:Class>
<daml:disjointWith, rdfs:range, daml:Class>
<daml:differentIndividualFrom, rdf:type, rdf:Property>
<daml:differentIndividualAs, rdfs:domain, daml:Thing>
<daml:differentIndividualAs, rdfs:range, daml:Thing>
<daml:unionOf, rdf:type, rdf:Property>
<daml:unionOf, rdfs:domain, daml:Class>
<daml:unionOf, rdfs:range, daml:List>
<daml:disjointUnionOf, rdf:type, rdf:Property>
<daml:disjointUnionOf, rdfs:domain, daml:Class>
<daml:disjointUnionOf, rdfs:range, daml:List>
<daml:intersectionOf, rdf:type, rdf:Property>
<daml:intersectionOf, rdfs:domain, daml:Class>
<daml:intersectionOf, rdfs:range, daml:List>
<daml:complementOf, rdf:type, rdf:Property>
<daml:complementOf, rdfs:domain, daml:Class>
<daml:complementOf, rdfs:range, daml:Class>
<daml:oneOf, rdf:type, rdf:Property>
<daml:oneOf, rdfs:domain, daml:Class>
<daml:oneOf, rdfs:range, daml:List>
<daml:Restriction, rdf:type, daml:Class>
<daml:Restriction, rdfs:subClassOf, daml:Class>
<daml:onProperty, rdf:type, rdf:Property>
<daml:onProperty, rdfs:domain, daml:Restriction>
<daml:onProperty, rdfs:range, rdf:Property>
<daml:toClass, rdf:type, rdf:Property>
<daml:toClass, rdfs:domain, daml:Restriction>
<daml:toClass, rdfs:range, rdfs:Class>
<daml:hasValue, rdf:type, rdf:Property>
<daml:hasValue,daml: domain

<daml:hasClass, rdf:type, rdf:Property>

<daml:hasClass, rdfs:domain, daml:Restriction>

<daml:hasClass, rdfs:range, rdfs:Class>

<daml:minCardinality, rdf:type, rdf:Property>

<daml:minCardinality, rdfs:domain, daml:Restriction>

<daml:minCardinality, rdfs:range, xsd:nonNegativeInteger>

<daml: rdf:Property, maxCardinality, rdf:type

<daml:maxCardinality, rdfs:domain, daml:Restriction>

<daml:maxCardinality, rdfs:range, xsd:nonNegativeInteger>

<daml:cardinality, rdf:type, rdf:Property>

<daml:cardinality, rdfs:domain, daml:Restriction>

<daml:cardinality, rdfs:range, xsd:nonNegativeInteger>

<daml:hasClassQ, rdf:type, rdf:Property>

<daml:hasClassQ, rdfs:domain, daml:Restriction>

<daml:hasClassQ, rdfs:range, rdfs:Class>

<daml:minCardinalityQ, rdf:type, rdf:Property>

<daml:minCardinalityQ, rdfs:domain, daml:Restriction>

<daml:minCardinalityQ, rdfs:range, xsd:nonNegativeInteger>

<daml:maxCardinalityQ, rdf:type, rdf:Property>

<daml:maxCardinalityQ, rdfs:domain, daml:Restriction>

<daml:maxCardinalityQ, rdfs:range, xsd:nonNegativeInteger>

<daml:cardinalityQ, rdf:type, rdf:Property>

<daml:cardinalityQ, rdfs:domain, daml:Restriction>

<daml:cardinalityQ, rdfs:range, xsd:nonNegativeInteger>

<daml:ObjectProperty, rdf:type, rdfs:Class>

<daml:ObjectProperty, rdfs:subClassOf, rdf:Property>

<daml:DatatypeProperty, rdf:type, rdfs:Class>

<daml:DatatypeProperty, rdfs:subClassOf, rdf:Property>

<daml:inverseOf, rdf:type, rdf:Property>

<daml:inverseOf, rdfs:domain, daml:ObjectProperty>

<daml:inverseOf, rdfs:range, daml:ObjectProperty>

<daml:TransitiveProperty, rdf:type, rdf:Class>

<daml:TransitiveProperty, rdfs:subClassOf, rdf:ObjectProperty>

<daml:UniqueProperty, rdf:type, rdf:Class>

<daml:UniqueProperty, rdfs:subClassOf, rdf:Property>

<daml:UnambiguousProperty, rdf:type, rdf:Class>

<daml:UnambiguousProperty, rdfs:subClassOf, rdf:ObjectProperty>

<daml:List, rdf:type, rdfs:Class>

<daml:nil, rdf:type, daml:List>

<daml:first, rdf:type, rdf:Property>

<daml:first, rdfs:domain, daml:List>

<daml:rest, rdf:type, rdf:Property>

<daml:rest, rdfs:domain, daml:List>

<daml:rest, rdfs:range, daml:List>

<daml:item, rdf:type, rdf:Property>

<daml:item, rdfs:domain, daml:List>

Note that a DAML+OIL graph should be the same as an RDF graph with daml+oil.daml loaded (modulo labels, comments, and the stuff at the end).
A DAML+OIL model of a DAML+OIL graph R is a core RDFS model of R with the following conditions. We define ICEXT(r) = { x : < x, rdf:type, r> } v XLS(r).

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

if <a,b> in IEXT(IS(daml:equivalentTo)) 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 a ~= 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) = { o1, ..., on } ^ IR

if <p,s> in IEXT(IS(daml:inverseOf))
then <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,c> 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 <c,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 }

References

DAML+OIL (March 2001) reference description

An Axiomatic Semantics for RDF, RDF-S, and DAML+OIL (March 2001)

Annotated DAML+OIL Ontology Markup

DAML+OIL revised language specification

A sample ontology

Datatype definitions for sample ontology

RDF Model Theory