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