A Model-Theoretic Semantics for DAML+OIL

Feedback to www-rdf-logic, please.

Peter Patel-Schneider, ed.
$Revision: 1.3 $ of $Date: 2001/01/11 21:48:51 $ 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.)

Typographical conventions

In the document various typographical conventions are used to represent sets, set relationships, and other mathematical notations. These may not be the most elegant typographical conventions, but they should be renderable by just about all HTML browsers.

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.

Semantics

The semantics uses a non-empty 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 would be helpful. (Actually, this could be done by creating classes that imply that two individuals are the same or distinct, but a direct method would be better.)

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 arising from these mappings 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