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

• From: Dan Connolly <connolly@w3.org>
• Date: 19 Jun 2002 16:26:58 -0500
• Message-Id: <1024522018.26122.422.camel@dirk>
```This is an attempt to address feedback on:

layering (5.3,5.10): a same-syntax model theory
From: Dan Connolly (connolly@w3.org)
Date: Thu, May 30 2002
http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0264.html

in particular, issues around lists and recursive
definitions. This leaves lists out altogether.
I think the result is a little bit klunky,
so I'd like to figure out how to formalize
lists properly, but until I understand more about how
semantics for recursion/induction/whatever works,
I'd like to know if this is
a coherent model theory for OWL:

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

Additionally, owl reserves the following vocabulary:

* 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, it reserves 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
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 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.

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.

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)

* 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.

[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

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

Received on Wednesday, 19 June 2002 17:26:46 UTC