A Model-Theoretic Semantics for DAML+OIL

Basic Assumptions:

A DAML+OIL knowledge base is a collection of RDF triples. Some of these triples are relevant to DAML+OIL and some are not. This semantics currently 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. Thus it has nothing to do with the meaning of Ontology or versionInfo or imports. This document ignores all aspects of naming and importing. It uses the ID of an RDF node as an identifier for the node.

Typographical conventions for sets:

<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

Semantics:

The semantics uses a domain of discourse, DD, which is the collection of all DAML+OIL semantic objects. The semantics assigns a meaning to various syntactic constructs by means of three interpretation functions

IC, which maps classes and restrictions (nodes) into subsets of DD
IR, which maps relationships (nodes) into subsets of DD x DD
IO, which maps individuals (nodes) into elements of DD

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

The semantics is specified via mappings from syntactic structures to (sets of) constraints. Most mappings have have formal parameters signified by means of a leading ?. Some mappings require the presence of several triples. Some mappings have side conditions.

A semantic structure <DD,IC,IO,IR> is a model for a DAML+OIL KB if all mappings from the KB are true in the structure.

In several places in the syntax lists are used. These are specified in a condensed form, as [l1,...,ln].

Let KB be a DAML+OIL KB in the form of a collection of RDF triples. The following mappings are specified mostly in the order that the DAML+OIL syntax is specified, with a few reorderings to place similar constructs together.

First we include a few redundant mappings. The semantic effects of these mapping 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 Mapping

<type,?C,CLASS> IC(?C) <= DD

<type,?C,RESTRICTION> IC(?C) <= DD

<type,?R,PROPERTY> IR(?R) <= DD x DD

IC(Thing) = DD

IC(Nothing) = { }

Syntactic Structure	Mapping
`<type,?C,CLASS>`	`IC(?C) <= DD`
`<type,?C,RESTRICTION>`	`IC(?C) <= DD`
`<type,?R,PROPERTY>`	`IR(?R) <= DD x DD`
	`IC(Thing) = DD`
	`IC(Nothing) = { }`

Now for the real semantic mappings.

Syntactic Structure Mapping

<type,?O,?C> IO(?O) in IC(?C)

<?R,?O1,?O2> <IO(?O1),IO(?O2)> in IR(?R)

<subClassOf,?C,?D> IC(?C) <= IC(?D)

<subPropertyOf,?R,?S> IR(?R) <= IR(?S)

<sameClassAs,?C,?D> IC(?C) = IC(?D)

<samePropertyAs,?R,?S> IR(?R) = IR(?S)

<disjointWith,?X,?Y> IC(?X) ^ IC(?Y) = { }

<type,[?X1,...,?Xn],Disjoint> IC(?Xi) ^ IC(?Xj) = { } for all 1<=i<j<=n.

<unionOf,?C,[?X1,...,?Xn]> IC(?C) = IC(?X1) v ... v IC(?Xn)

<disjointUnionOf,?C,[?X1,...,?Xn]> IC(?C) = IC(?X1) v ... v IC(?Xn)

IC(?Xi) ^ IC(?Xj) = { } for 1<=i<j<=n.

<intersectionOf,?C,[?X1,...,?Xn]> IC(?C) = IC(?X1) ^ ... ^ IC(?Xn)

<complementOf,?X,?Y> IC(?X) ^ IC(?Y) = { }

IC(?X) v IC(?Y) = DD

<oneOf,?C,[?O1,...,?On]> IC(?C) = { IO(?O1),..., IO(?On) }

<inverseOf,?R,?S> <x,y> in IR(?R) iff <y,x> in IR(?S)

<type,?R,TransitiveProperty> if <x,y> in IR(?R) and <y,z> in IR(?R) then <x,z> in IR(?R)

<type,?R,UniqueProperty> if <x,y> in IR(?R) and <x,z> in IR(?R) then y=z

<type,?R,UnambiguousProperty> if <x,y> in IR(?R) and <z,y> in IR(?R) then x=z

<type,?R,Restriction> <onProperty,?R,?P> <toClass,?R,?C> x in IC(?R) iff IR(?P)({x}) <= IC(?C)

<type,?R,Restriction> <onProperty,?R,?P> <hasValue,?R,?V> x in IC(?R) iff <x,IO(?V)> in IR(?P)>

<type,?R,Restriction> <onProperty,?R,?P> <hasClass,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | > 0

<type,?R,Restriction> <onProperty,?R,?P> <minCardinality,?R,?n> x in IC(?R) iff | IR(?P)({x}) | >= ?n

<type,?R,Restriction> <onProperty,?R,?P> <maxCardinality,?R,?n> x in IC(?R) iff | IR(?P)({x}) | <= ?n

<type,?R,Restriction> <onProperty,?R,?P> <cardinality,?R,?n> x in IC(?R) iff | IR(?P)({x}) | = ?n

<type,?R,Restriction> <onProperty,?R,?P> <minCardinalityQ,?R,?n> <hasClassQ,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | >= ?n

<type,?R,Restriction> <onProperty,?R,?P> <maxCardinalityQ,?R,?n> <hasClassQ,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | <= ?n

<type,?R,Restriction> <onProperty,?R,?P> <cardinalityQ,?R,?n> <hasClassQ,?R,?C> x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | = ?n

<domain,?P,?C> if <x,y> in IR(?P) then x in IC(?C)

<range,?P,?C> if <x,y> in IR(?P) then y in IC(?C)

Syntactic Structure	Mapping
`<type,?O,?C>`	`IO(?O) in IC(?C)`
`<?R,?O1,?O2>`	`<IO(?O1),IO(?O2)> in IR(?R)`
`<subClassOf,?C,?D>`	`IC(?C) <= IC(?D)`
`<subPropertyOf,?R,?S>`	`IR(?R) <= IR(?S)`
`<sameClassAs,?C,?D>`	`IC(?C) = IC(?D)`
`<samePropertyAs,?R,?S>`	`IR(?R) = IR(?S)`
`<disjointWith,?X,?Y>`	`IC(?X) ^ IC(?Y) = { }`
`<type,[?X1,...,?Xn],Disjoint>`	`IC(?Xi) ^ IC(?Xj) = { } for all 1<=i<j<=n.`
`<unionOf,?C,[?X1,...,?Xn]>`	`IC(?C) = IC(?X1) v ... v IC(?Xn)`
`<disjointUnionOf,?C,[?X1,...,?Xn]>`	`IC(?C) = IC(?X1) v ... v IC(?Xn)`
`IC(?Xi) ^ IC(?Xj) = { } for 1<=i<j<=n.`
`<intersectionOf,?C,[?X1,...,?Xn]>`	`IC(?C) = IC(?X1) ^ ... ^ IC(?Xn)`
`<complementOf,?X,?Y>`	`IC(?X) ^ IC(?Y) = { }`
`IC(?X) v IC(?Y) = DD`
`<oneOf,?C,[?O1,...,?On]>`	`IC(?C) = { IO(?O1),..., IO(?On) }`
`<inverseOf,?R,?S>`	`<x,y> in IR(?R) iff <y,x> in IR(?S)`
`<type,?R,TransitiveProperty>`	`if <x,y> in IR(?R) and <y,z> in IR(?R) then <x,z> in IR(?R)`
`<type,?R,UniqueProperty>`	`if <x,y> in IR(?R) and <x,z> in IR(?R) then y=z`
`<type,?R,UnambiguousProperty>`	`if <x,y> in IR(?R) and <z,y> in IR(?R) then x=z`
`<type,?R,Restriction> <onProperty,?R,?P> <toClass,?R,?C>`	`x in IC(?R) iff IR(?P)({x}) <= IC(?C)`
`<type,?R,Restriction> <onProperty,?R,?P> <hasValue,?R,?V>`	`x in IC(?R) iff <x,IO(?V)> in IR(?P)>`
`<type,?R,Restriction> <onProperty,?R,?P> <hasClass,?R,?C>`	`x in IC(?R) iff \| IR(?P)({x}) ^ IC(?C) \| > 0`
`<type,?R,Restriction> <onProperty,?R,?P> <minCardinality,?R,?n>`	`x in IC(?R) iff \| IR(?P)({x}) \| >= ?n`
`<type,?R,Restriction> <onProperty,?R,?P> <maxCardinality,?R,?n>`	`x in IC(?R) iff \| IR(?P)({x}) \| <= ?n`
`<type,?R,Restriction> <onProperty,?R,?P> <cardinality,?R,?n>`	`x in IC(?R) iff \| IR(?P)({x}) \| = ?n`
`<type,?R,Restriction> <onProperty,?R,?P> <minCardinalityQ,?R,?n> <hasClassQ,?R,?C>`	`x in IC(?R) iff \| IR(?P)({x}) ^ IC(?C) \| >= ?n`
`<type,?R,Restriction> <onProperty,?R,?P> <maxCardinalityQ,?R,?n> <hasClassQ,?R,?C>`	`x in IC(?R) iff \| IR(?P)({x}) ^ IC(?C) \| <= ?n`
`<type,?R,Restriction> <onProperty,?R,?P> <cardinalityQ,?R,?n> <hasClassQ,?R,?C>`	`x in IC(?R) iff \| IR(?P)({x}) ^ IC(?C) \| = ?n`
`<domain,?P,?C>`	`if <x,y> in IR(?P) then x in IC(?C)`
`<range,?P,?C>`	`if <x,y> in IR(?P) then y in IC(?C)`

$Revision: 1.3$ of $Date: 2001/01/09$