W3C home > Mailing lists > Public > www-webont-wg@w3.org > June 2002

Re: layering (5.3,5.10): a first-order same-syntax model theory

From: Dan Connolly <connolly@w3.org>
Date: 28 Jun 2002 12:50:02 -0500
To: www-webont-wg@w3.org
Message-Id: <1025286603.22162.293.camel@dirk>
On Thu, 2002-06-20 at 10:55, Dan Connolly wrote:
[...]
> I'll see if I can spin another draft presently...

This revision integrates recent feedback:

  An OWL model theory layered on RDF
  $Id: owlsem55.txt,v 1.2 2002/06/28 17:41:12 connolly Exp $
  http://www.w3.org/2002/06/owlsem55.txt
  (contents attached, along with diffs
  from previous version).





-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/


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 <x,y> 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 | <y,x> 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:
<?s, ?o> is in IEXT(I(ont:complementOf)),
iff ICEXT(?s) is the complement of ICEXT(?o)
relative to IR.

differentFrom:
<?s, ?o> is in IEXT(I(ont:differentFrom)),
iff ?s is not equal to ?o.


disjointWith:
<?s, ?o> is in IEXT(I(ont:disjointWith)),
iff ICEXT(?s) is disjoint from ICEXT(?o).

equivalentTo:
<?s, ?o> is in IEXT(I(ont:equivalentTo)),
iff IEXT(?s) = IEXT(?o).


onProperty/hasClass:
if <?r, ?p> is in IEXT(I(ont:onProperty))
and <?r, ?a> is in IEXT(I(ont:hasClass)),
then
 ICEXT(?r) = { ?s : <?s,?x> in IEXT(?p) for some ?x in ICEXT(?a)  }


onProperty/hasValue:
if <?r, ?p> is in IEXT(I(ont:onProperty))
and <?r, ?a> is in IEXT(I(ont:hasValue)),
then the set
  ICEXT(?r) = { ?s: <?s, ?a> in IEXT(?p) }


imports:
none. imports doesn't constrain interpretations
(other than having the subproperty relationship
with rdfs:seeAlso).


intersectionOf1/intersectionOf2:

if <?a, ?b> is in IEXT(I(ont:intersectionOf1))
and <?a, ?c> is in IEXT(I(ont:intersectionOf2))
and ?x is in ICEXT(?b) and in ICEXT(?c)
then ?x is in ICEXT(?a).

conversely,

if <?a, ?b> is in IEXT(I(ont:intersectionOf1))
and <?a, ?c> is in IEXT(I(ont:intersectionOf2))
and ?x is in ICEXT(?a).
then ?x is in ICEXT(?b) and in ICEXT(?c)


inverseOf:

<?p, ?q> is in IEXT(I(ont:intersectionOf))
iff IEXT(?p) is the relational inverse of IEXT(?q);
  IEXT(?p) = { <y, x> | <x, y> in IEXT(?q) }.


oneOf1/oneOf2:

if  <?a, ?b> is in IEXT(I(ont:oneOf1))
and <?a, ?c> is in IEXT(I(ont:oneOf2))
then ?b is in ICEXT(?a)
and ICEXT(?c) is a subset of ICEXT(?a).

 conversely,
if  <?a, ?b> is in IEXT(I(ont:oneOf1))
and <?a, ?c> 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:
<?s, ?o> is in IEXT(I(ont:sameClassAs)),
iff ICEXT(?s) = ICEXT(?o).

samePropertyAs:
<?s, ?o> is in IEXT(I(samePropertyAs)),
iff IEXT(?s) = IEXT(?o).

toClass:
if  <?a, ?c> in IEXT(I(ont:toClass))
and <?a, ?p> in IEXT(I(ont:onProperty))
and <?x, ?y> 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 <?x, ?y> in IEXT(?p)
   and <?y, ?z> in IEXT(?p)
  then <?x, ?z> in IEXT(?p).

manyToOneOver:

<?p, ?c> in IEXT(I(ont:manyToOneOver))
iff for every ?x, ?y, and ?z in IR,
  if ?x in ICEXT(?c)
    and <?x, ?y> in IEXT(?p)
    and <?x, ?z> in IEXT(?p)
  then ?y = ?z.

ManyToOneProperty:

?p in IEXT(I(ont:ManyToOneProperty))
iff for every ?x, ?y, and ?z in IR,
  if    <?x, ?y> in IEXT(?p)
    and <?x, ?z> in IEXT(?p)
  then ?y = ?z.


manyToOneOver:

<?p, ?c> in IEXT(I(ont:manyToOneOver))
iff for every ?x, ?y, and ?z in IR,
  if ?x in ICEXT(?c)
    and <?x, ?y> in IEXT(?p)
    and <?x, ?z> in IEXT(?p)
  then ?y = ?z.


OneToManyProperty:

?p in IEXT(I(ont:OneToManyProperty))
iff for every ?x, ?y, and ?z in IR,
  if    <?y, ?x> in IEXT(?p)
    and <?z, ?x> in IEXT(?p)
  then ?y = ?z.

oneToManyOver:

<?p, ?c> in IEXT(I(ont:oneToManyOver))
iff for every ?x, ?y, and ?z in IR,
  if ?x in ICEXT(?c)
    and <?y, ?x> in IEXT(?p)
    and <?z, ?x> in IEXT(?p)
  then ?y = ?z.


unionOf1/unionOf2:

if <?a, ?b> is in IEXT(I(ont:unionOf1))
and <?a, ?c> is in IEXT(I(ont:unionOf2))
and ?x is in ICEXT(?b) or in ICEXT(?c)
then ?x is in ICEXT(?a).

conversely,

if <?a, ?b> is in IEXT(I(ont:unionOf1))
and <?a, ?c> 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

Index: owlsem55.txt
===================================================================
RCS file: /w3ccvs/WWW/2002/06/owlsem55.txt,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- owlsem55.txt	2002/06/28 17:40:41	1.1
+++ owlsem55.txt	2002/06/28 17:41:12	1.2
@@ -1,3 +1,7 @@
+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.
@@ -14,7 +18,8 @@
 
 Recall that ICEXT(x) abbreviates {y | <y,x> is in IEXT(I(rdf:type)) }.
 
-Additionally, owl reserves the following vocabulary:
+Each of the following terms is in the vocabulary (V) of every
+owl interpretation:
 
     * complementOf
     * differentFrom
@@ -44,10 +49,10 @@
     * versionInfo
 
 
-That is, it reserves the URI references
+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; in this document, we'll abbreviate these
+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:
@@ -79,17 +84,15 @@
 onProperty/hasClass:
 if <?r, ?p> is in IEXT(I(ont:onProperty))
 and <?r, ?a> is in IEXT(I(ont:hasClass)),
-then the set
-  { ?o: for some ?s in ICEXT(?r), <?s, ?o> is in IEXT(?p)
-        and ?o is in ICEXT(?a) }
-has at least one element.
+then
+ ICEXT(?r) = { ?s : <?s,?x> in IEXT(?p) for some ?x in ICEXT(?a)  }
 
+
 onProperty/hasValue:
 if <?r, ?p> is in IEXT(I(ont:onProperty))
 and <?r, ?a> is in IEXT(I(ont:hasValue)),
 then the set
-  { ?o: for some ?s in ICEXT(?r), <?s, ?a> is in IEXT(?p) }
-isn't empty.
+  ICEXT(?r) = { ?s: <?s, ?a> in IEXT(?p) }
 
 
 imports:
@@ -274,11 +277,25 @@
  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
-
-
Received on Friday, 28 June 2002 13:49:30 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:50 GMT