An OWL model theory layered on RDF
$Id: owlsem55.txt,v 1.2 2002/06/28 17:41:12 connolly Exp $
As in [RDFMT], an interpretation I of a vocabulary V is
1. A non-empty set IR of resources, called the domain or universe of I.
2. A mapping IEXT from IR into the powerset of IR x (IR union LV)
i.e. the set of sets of pairs with x in IR and y in IR or LV
3. A mapping IS from V into IR
Every owl interpretations is an RDF interpretations (i.e. IR
contains IS(rdf:type)) and an RDFS interpretation (i.e.
the RDFS closure rules apply).
Recall that ICEXT(x) abbreviates {y | is in IEXT(I(rdf:type)) }.
Each of the following terms is in the vocabulary (V) of every
owl interpretation:
* complementOf
* differentFrom
* disjointWith
* equivalentTo
* hasClass
* hasValue
* imports
* intersectionOf1
* intersectionOf2
* inverseOf
* oneOf1
* oneOf2
* onProperty
* Ontology
* Restriction
* sameClassAs
* samePropertyAs
* toClass
* TransitiveProperty
* ManyToOneProperty
* manyToOneOver
* unionOf1
* unionOf2
* OneToManyProperty
* oneToManyOver
* versionInfo
That is, the URI references
http://www.w3.org/2001/10/daml+oil#complementOf ,
http://www.w3.org/2001/10/daml+oil#differentFrom ,
and so on are in V; in this document, we'll abbreviate these
as ont:cardinality, ont:complementOf and so on.
The following closure rules apply:
ont:imports rdfs:subPropertyOf rdfs:seeAlso.
ont:versionInfo rdfs:subPropertyOf rdfs:comment.
The following constraints on interpretations apply:
complementOf:
is in IEXT(I(ont:complementOf)),
iff ICEXT(?s) is the complement of ICEXT(?o)
relative to IR.
differentFrom:
is in IEXT(I(ont:differentFrom)),
iff ?s is not equal to ?o.
disjointWith:
is in IEXT(I(ont:disjointWith)),
iff ICEXT(?s) is disjoint from ICEXT(?o).
equivalentTo:
is in IEXT(I(ont:equivalentTo)),
iff IEXT(?s) = IEXT(?o).
onProperty/hasClass:
if is in IEXT(I(ont:onProperty))
and is in IEXT(I(ont:hasClass)),
then
ICEXT(?r) = { ?s : in IEXT(?p) for some ?x in ICEXT(?a) }
onProperty/hasValue:
if is in IEXT(I(ont:onProperty))
and is in IEXT(I(ont:hasValue)),
then the set
ICEXT(?r) = { ?s: in IEXT(?p) }
imports:
none. imports doesn't constrain interpretations
(other than having the subproperty relationship
with rdfs:seeAlso).
intersectionOf1/intersectionOf2:
if is in IEXT(I(ont:intersectionOf1))
and is in IEXT(I(ont:intersectionOf2))
and ?x is in ICEXT(?b) and in ICEXT(?c)
then ?x is in ICEXT(?a).
conversely,
if is in IEXT(I(ont:intersectionOf1))
and is in IEXT(I(ont:intersectionOf2))
and ?x is in ICEXT(?a).
then ?x is in ICEXT(?b) and in ICEXT(?c)
inverseOf:
is in IEXT(I(ont:intersectionOf))
iff IEXT(?p) is the relational inverse of IEXT(?q);
IEXT(?p) = { | in IEXT(?q) }.
oneOf1/oneOf2:
if is in IEXT(I(ont:oneOf1))
and is in IEXT(I(ont:oneOf2))
then ?b is in ICEXT(?a)
and ICEXT(?c) is a subset of ICEXT(?a).
conversely,
if is in IEXT(I(ont:oneOf1))
and is in IEXT(I(ont:oneOf2))
and ?x is in ICEXT(?a)
then either ?x = ?b or ?x is in ICEXT(?c).
onProperty:
[see hasClass, hasValue, toClass]
Ontology:
none. There are no constraints on interpretation
specific to Ontology.
Restriction:
none.
sameClassAs:
is in IEXT(I(ont:sameClassAs)),
iff ICEXT(?s) = ICEXT(?o).
samePropertyAs:
is in IEXT(I(samePropertyAs)),
iff IEXT(?s) = IEXT(?o).
toClass:
if in IEXT(I(ont:toClass))
and in IEXT(I(ont:onProperty))
and in IEXT(?p)
and ?x in ICEXT(?a)
then ?y in ICEXT(?c).
TransitiveProperty:
?p in ICEXT(I(ont:TransitiveProperty))
iff for every ?x, ?y, and ?z in IR,
if in IEXT(?p)
and in IEXT(?p)
then in IEXT(?p).
manyToOneOver:
in IEXT(I(ont:manyToOneOver))
iff for every ?x, ?y, and ?z in IR,
if ?x in ICEXT(?c)
and in IEXT(?p)
and in IEXT(?p)
then ?y = ?z.
ManyToOneProperty:
?p in IEXT(I(ont:ManyToOneProperty))
iff for every ?x, ?y, and ?z in IR,
if in IEXT(?p)
and in IEXT(?p)
then ?y = ?z.
manyToOneOver:
in IEXT(I(ont:manyToOneOver))
iff for every ?x, ?y, and ?z in IR,
if ?x in ICEXT(?c)
and in IEXT(?p)
and in IEXT(?p)
then ?y = ?z.
OneToManyProperty:
?p in IEXT(I(ont:OneToManyProperty))
iff for every ?x, ?y, and ?z in IR,
if in IEXT(?p)
and in IEXT(?p)
then ?y = ?z.
oneToManyOver:
in IEXT(I(ont:oneToManyOver))
iff for every ?x, ?y, and ?z in IR,
if ?x in ICEXT(?c)
and in IEXT(?p)
and in IEXT(?p)
then ?y = ?z.
unionOf1/unionOf2:
if is in IEXT(I(ont:unionOf1))
and is in IEXT(I(ont:unionOf2))
and ?x is in ICEXT(?b) or in ICEXT(?c)
then ?x is in ICEXT(?a).
conversely,
if is in IEXT(I(ont:unionOf1))
and is in IEXT(I(ont:unionOf2))
and ?x is in ICEXT(?a).
then ?x is in ICEXT(?b) or in ICEXT(?c)
versionInfo:
none.
Notes:
dropped per WG decision:
* cardinalityQ
* hasClassQ
* maxCardinalityQ
* minCardinalityQ
dropped re 'uniform treatment of literals'
* Datatype
* DatatypeProperty
* DatatypeRestriction
* ObjectClass
* ObjectProperty
* ObjectRestriction
* sameIndividualAs
* differentIndividualFrom (renamed differentFrom)
already specified by RDF MT:
* domain
* Property
* range
* Class
* subClassOf
* subPropertyOf
I have adopted the suggestion to drop...
* disjointUnionOf
cf suggestion from Mike Dean 30 May
http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0262.html
and I got a little lazy around
cardinality, cutting out
* cardinality
* maxCardinality
* minCardinality
leaving just OneToMany, ManyToOne,
oneToManyOver, and ManyToOneOver.
i.e. leaving just the maxcardinality 1 idioms.
This model theory takes a fairly conservative position
on "5.10 DAML+OIL semantics is too weak"
http://www.w3.org/2001/sw/WebOnt/webont-issues.html#I5.10-DAML-OIL-semantics-is-too-weak
cf # DDTF/layering: weak class theory seems good enough (5.3, 5.10)
Dan Connolly (Tue, May 28 2002)
http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0235.html
This model theory doesn't address issue
5.6 daml:imports as magic syntax
http://www.w3.org/2001/sw/WebOnt/webont-issues.html#I5.6-daml:imports-as-magic-syntax
Jos DeRoo reported some initial successful
implementation experience:
From: Jos De_Roo (jos.deroo.jd@belgium.agfa.com)
Date: Thu, Jun 20 2002
http://lists.w3.org/Archives/Public/www-webont-wg/2002Jun/0171.html
[RDFMT] RDF Model Theory
W3C Working Draft 29 April 2002
http://www.w3.org/TR/2002/WD-rdf-mt-20020429/
esp section
http://www.w3.org/TR/2002/WD-rdf-mt-20020429/#sinterp