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

Good.  A proposal.

From: Dan Connolly <connolly@w3.org>
Subject: layering (5.3,5.10): a first-order same-syntax model theory
Date: 19 Jun 2002 16:26:58 -0500

[...]

> Additionally, owl reserves the following vocabulary:

[...]

I have no idea what ``reserves the ... vocabulary'' could mean.

[...]

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

Completely wrong.  Something like
   then ICEXT(?r) = { ?o : exists ?x in ICEXT(?a) st <?o,?x> in IEXT(?p) }
is needed here.  Similarly for other restrictions.

[..]

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

Don't think so.  imports means that the OWL KB pointed to should be
considered to be part of this KB.

A treatment of imports would be something like

	if <?KB1,?KB2> in IEXT(owl:imports)
	then the models of ?KB1 are a subset of the models of ?KB2.

No particularly standard-first-order, however.

[...]


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

What if happens if there is another ont:intersectionOf1 link from ?a?

[...]

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

Hmm. How does a oneOf finish?  

Suppose we have 
	IEXT(I(ont:oneOf1)) = { <x,a> }
	IEXT(I(ont:oneOf2)) = { }
Then what is the class extension of x?

Suppose we have 
	IEXT(I(ont:oneOf1)) = { <x,a> }
	IEXT(I(ont:oneOf2)) = { <x,x> }
Then what is the class extension of x?

[...]

And, of course, there are no comprehension constraints, so

     x rdf:type _:y .
     _:y one:intersectionOf1 a .
     _:y one:intersectionOf2 b .

does not entail that

     x rdf:type _:z .
     _:z one:intersectionOf1 b .
     _:z one:intersectionOf2 a .


So, in sum, lots of problems.

peter

Received on Wednesday, 19 June 2002 18:21:29 UTC