Feedback to www-rdf-logic,
please.
Peter Patel-Schneider, ed.
$Revision: 1.4$ of $Date: 2001/01/09$
corresponding to the DAML+OIL version of 2001/01/10.
This document provides a terse specification of the model-theoretic semantics for DAML+OIL.
A DAML+OIL ontology (or knowledge base) is a collection of RDF triples. Some of these triples are relevant to DAML+OIL and some are not. This semantics 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. This document ignores all aspects of naming and importing. Thus it has nothing to do with the meaning of Ontology or versionInfo or imports. (The intended meaning of imports is that the RDF triples of the referenced ontology are included in the RDF triples of the current ontology.)
Names in this document are qualified if they come from other namespaces than the DAML+OIL namespace. (Think of the names as if the following XML namespace definitions are present:
Several DAML+OIL constructs accept a list. The semantic mappings show these lists as [x1,...,xn] in the interests of brevity and clarity.
The semantics is specified via mappings from syntactic structures to constraints on semantic structures. Most mappings have have formal parameters signified by means of a leading ``?''. Some mappings require the presence of several triples.
Consider a DAML+OIL ontology in the form of a collection of RDF triples. A semantic structure <DD,IC,IO,IR> is a model for the DAML+OIL ontology if the constraints resulting from the mappings from the ontology are true in the structure.
First we include a few redundant mappings. The semantic constraints rising from 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 | Semantic Constraint |
---|---|
<rdf:type,?C,rdfs:Class> | IC(?C) <= DD |
<rdf:type,?C,Restriction> | IC(?C) <= DD |
<rdf:type,?R,rdf:Property> | IR(?R) <= DD x DD |
IC(Thing) = DD | |
IC(Nothing) = { } |
Now for the real semantic mappings.
Syntactic Structure | Semantic Constraint |
---|---|
<rdf:type,?O,?C> | IO(?O) in IC(?C) |
<?R,?O1,?O2> | <IO(?O1),IO(?O2)> in IR(?R) |
<rdfs:subClassOf,?C,?D> | IC(?C) <= IC(?D) |
<rdfs: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) = { } |
<rdf: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) } |
<rdfs:domain,?P,?C> | if <x,y> in IR(?P) then x in IC(?C) |
<rdfs:range,?P,?C> | if <x,y> in IR(?P) then y in IC(?C) |
<inverseOf,?R,?S> | <x,y> in IR(?R) iff <y,x> in IR(?S) |
<rdf:type,?R,TransitiveProperty> | if <x,y> in IR(?R) and <y,z> in IR(?R) then <x,z> in IR(?R) |
<rdf:type,?R,UniqueProperty> | if <x,y> in IR(?R) and <x,z> in IR(?R) then y=z |
<rdf:type,?R,UnambiguousProperty> | if <x,y> in IR(?R) and <z,y> in IR(?R) then x=z |
<rdf:type,?R,Restriction> <onProperty,?R,?P> <toClass,?R,?C> | x in IC(?R) iff IR(?P)({x}) <= IC(?C) |
<rdf:type,?R,Restriction> <onProperty,?R,?P> <hasValue,?R,?V> | x in IC(?R) iff <x,IO(?V)> in IR(?P)> |
<rdf:type,?R,Restriction> <onProperty,?R,?P> <hasClass,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | > 0 |
<rdf:type,?R,Restriction> <onProperty,?R,?P> <minCardinality,?R,?n> | x in IC(?R) iff | IR(?P)({x}) | >= ?n |
<rdf:type,?R,Restriction> <onProperty,?R,?P> <maxCardinality,?R,?n> | x in IC(?R) iff | IR(?P)({x}) | <= ?n |
<rdf:type,?R,Restriction> <onProperty,?R,?P> <cardinality,?R,?n> | x in IC(?R) iff | IR(?P)({x}) | = ?n |
<rdf:type,?R,Restriction> <onProperty,?R,?P> <minCardinalityQ,?R,?n> <hasClassQ,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | >= ?n |
<rdf:type,?R,Restriction> <onProperty,?R,?P> <maxCardinalityQ,?R,?n> <hasClassQ,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | <= ?n |
<rdf:type,?R,Restriction> <onProperty,?R,?P> <cardinalityQ,?R,?n> <hasClassQ,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | = ?n |