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

[apologies if this is a duplicate; I'm using
a different mailer from the one I usually use.]

Jeremy wrote:
>> I think there are two proposals that I think we can be confident would
>> work: one in which all the ontology stuff is dark, and one in which no
>> sets necessarily exist.
Then peter wrote:

>The first definitely works.  There is not yet an existence proof that the
>second does indeed work, at least as an extension of the RDF model
theory.
[...]
> If you mean a same-syntax
>extension, then, again, that is impossible for the uppper layers without
> going to a very non-standard logic.
-- http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0236.html

So tonight I started writing up a model theory. I worked
out the details for about 10 of the 30 or so terms
in DAML+OIL; I'm pretty sure the rest are straightforward,
but it's getting tedious and I'm getting tired, so
I'm taking a break for the night...

Jeremy, wanna look this over and maybe fill in the next few terms?



==========

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)) }.


Likewise, let ICEXT(x) abbreviates {y | <y,x> is in IEXT(I(rdf:type)) }.

Additionally, owl reserves the following vocabulary:

    * cardinality
    * complementOf
    * differentIndividualFrom
    * disjointUnionOf
    * disjointWith
    * equivalentTo
    * hasClass
    * hasValue
    * imports
    * intersectionOf
    * inverseOf
    * maxCardinality
    * minCardinality
    * oneOf
    * onProperty
    * Ontology
    * Restriction
    * sameClassAs
    * sameIndividualAs
    * samePropertyAs
    * subClassOf
    * subPropertyOf
    * toClass
    * TransitiveProperty
    * UnambigousProperty
    * unionOf
    * UniqueProperty
    * versionInfo

    * first
    * rest
    * nil
    * item
    * List


That is, it reserves the URI references
  http://www.w3.org/2001/10/daml+oil#cardinality ,
  http://www.w3.org/2001/10/daml+oil#complementOf ,
and so on; in this document, we'll abbreviate these
as ont:cardinality, ont:complementOf and so on.

The following closure rules apply:

 ?l ont:first ?x.       ==> ?l ont:item ?x.

 ?l ont:rest ?r.
 ?r ont:first ?x.	==> ?l ont:item ?x.


The following constraints on interpretations apply:

cardinality:
if ?nl is a numeral for ?n (i.e. ?nl is a string that is a lexical
representation of the integer ?n), and <IS(?p), ?nl> is in
IEXT(I(ont:cardinality)) and <?s, ?o> is in IEXT(?p), then
the size of the set { ?x: <?s, ?x> is in IEXT(?p) } is ?n.


complementOf:
if <?s, ?o> is in IEXT(I(ont:complementOf)),
then ICEXT(?s) is the complement of ICEXT(?o)
relative to IR.

differentIndividualFrom:
if <?s, ?o> is in IEXT(I(ont:differentIndividualFrom)),
then ?s is not equal to ?o.


disjointUnionOf:
1. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)),
and <?l, ?a> is in IEXT(I(ont:item)),
then ICEXT(?a) is a subset of ICEXT(?s).

2. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)),
and <?l, ?a> is in IEXT(I(ont:first)),
and <?l, ?r> is in IEXT(I(ont:rest)),
and <?x, ?s> is in IEXT(I(rdf:type)),
then either ?x is in ICEXT(?a) or
there is a ?b where <?r, ?b> is in IEXT(I(ont:item)).

3. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)),
then ?l is a pairwise-disjoint list, defined
recursively as follows:
IEXT(I(ont:nil)) is pairwise-disjoint.
any ?l with <?l, IS(ont:nil)> in IEXT(I(ont:rest)) is pairwise-disjoint.
if ?r is pairwise-disjoint,
  and <?l, ?a> in IEXT(I(ont:first)),
  and for each ?b with <?r, ?b> in IEXT(I(ont:item)),
    ICEXT(?a) is disjoint with ICEXT(?b),
  then ?l is pairwise-disjoint.


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

equivalentTo:
if <?s, ?o> is in IEXT(I(ont:equivalentTo)),
then 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 the set
  { ?o: for some ?s in ICEXT(?r), <?s, ?o> is in IEXT(?p)
        and ?o is in ICEXT(?a) }
isn't empty.

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.


[... and so on...]


Notes:

dropped per WG decision:
    * cardinalityQ
    * hasClassQ
    * maxCardinalityQ
    * minCardinalityQ

dropped re 'uniform treatment of literals'
    * Datatype
    * DatatypeProperty
    * DatatypeRestriction
    * ObjectClass
    * ObjectProperty
    * ObjectRestriction

already specified by RDF MT:
    * domain
    * Property
    * range
    * Class

[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 Thursday, 30 May 2002 00:58:22 UTC