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:

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