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. 

Abbreviated syntax is used in some places, such as for lists.


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.


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) = { }
	NB: The above are redundant and are only here for emphasis.

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

<equivalentTo,?C,?D>		IC(?C) = IC(?D)
<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>		if <x,y> in IR(?R) then <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

<restrictedBy,?C,?P> 		IC(?C) <= IC(?P)

<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