A Model-Theoretic Semantics for DAML+OIL

Basic Assumptions:

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:

•  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

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) = { }

<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