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

• From: Dan Connolly <connolly@w3.org>
• Date: Wed, 29 May 2002 18:57:44 -1000
• Message-Id: <E17DI0O-0005pJ-00@jammer.dm93.org>
```[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