From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Tue, 25 Mar 2008 21:01:25 -0400 (EDT)

Message-Id: <20080325.210125.241251968.pfps@research.bell-labs.com>

To: schneid@fzi.de

Cc: public-owl-wg@w3.org

Date: Tue, 25 Mar 2008 21:01:25 -0400 (EDT)

Message-Id: <20080325.210125.241251968.pfps@research.bell-labs.com>

To: schneid@fzi.de

Cc: public-owl-wg@w3.org

From: "Michael Schneider" <schneid@fzi.de> Subject: RE: ACTION-93 / ISSUE-63: Initiated work on OWL-1.1-Full semantics Date: Tue, 25 Mar 2008 23:30:12 +0100 > >-----Original Message----- > >From: Peter F. Patel-Schneider [mailto:pfps@research.bell-labs.com] > >Sent: Tuesday, March 25, 2008 8:00 PM > >To: Michael Schneider > >Cc: public-owl-wg@w3.org; jjc@hpl.hp.com > >Subject: Re: ACTION-93 / ISSUE-63: Initiated work on > >OWL-1.1-Full semantics [...] > >A few specific points: [...] > >2/ I do not believe that a comprehension principle is needed for > > owl11:disjointUnionOf (so long as there is a comprehension principle > > for lists of descriptions) and the syntax requires that the > > disjointUnion be a named class. > > I don't understand your last remark about the requirement of a named class. If a named class is required (and it currently is) disjointUnion := 'DisjointUnion' '(' { annotation } owlClassURI description description { description } ')' then there is no need to ever require the existence of a node on the "left hand side" of an owl:disjointUnionOf because the only nodes that are needed there to make entailment work out are named classes. > For your first point: AFAICT, this comprehension principle is redundant. If > I start from its premises: > > (1a) l is a sequence of d_1, ..., d_n over IOC, > (1b) CEXT_I(d_i) ^ CEXT_I(d_k) = {} for 1 <= i < k <= n > > then I will get from (1a) plus the comprehension principle for owl:unionOf > (1.0-Full semantics): > > (1c) EXISTS c in IOC: <c,l> in EXT_I(S_I(owl:unionOf)) > > So I receive from the semantic condition of owl:unionOf (1.0-Full semantics) > that for this class c holds: > > (1d) CEXT_I(c) = CEXT_I(d_1) u u CEXT_I(d_n) > > (1d) + (1b) plus the main semantic condition for owl11:disjointUnionOf now > leads to > > (1e) <c,l> in EXT_I(S_I(owl11:disjointUnionOf)) > > So we could drop the comprehension principle for disjointUnionOf for > technical reasons. Agreed. > However, having it doesn't seem to hurt (as long as there > is also one for owl:unionOf). And I prefer having a common style of > semantics for analog axioms. And I don't like to answer questions of the > kind: "Hey, did you forget to define the comprehension principle?". :) So I > would like to keep it in for "symmetry reasons". What do you think? Well it doesn't hurt, but it doesn't help either, and the more conditions, the more possibility for errors. [...] > >peter [...] > Here are a few question, which I are very important for me to know. > > (A) How do you think about my approach to introduce the "missing" axiomatic > triples? Was is intended to not include them, and if so, for what reason? Or > has it just been forgotton? It was intended not to include them. It's not as if there are any real problems if these are not included, and, again, putting them in just increases the chance of some unintended consequence. > (B) Why are there only "ONLY-IF" semantic conditions for restrictions? The > introduction of sec. 5.2 in the AS&S says: > > "The only-if semantic conditions for the [restrictions] are needed > to prevent semantic paradoxes and other problems with the semantics." > Can you please elaborate on this? Suppose all the conditions are IFF, including \forall y in IOC \forall x in IOR \forall p in IOOPuIODP ( <x,y> in EXTI(SI(owl:allValuesFrom)) and <x,p> in EXTI(SI(owl:onProperty)) ) iff CEXTI(x) = { u in IOT | <u,v> in EXTI(p) implies v in CEXTI(y) } \forall y in IOC \forall x in IOR \forall p in IOOPuIODP ( <x,y> in EXTI(SI(owl:someValuesFrom)) and <x,p> in EXTI(SI(owl:onProperty)) ) iff CEXTI(x) = { u in IOT | E <u,v> in EXTI(p) such that v in CEXTI(y) } Then consider an interpretation with p1/ EXTI(SI(p)) = { < SI(i),SI(v) > } p2/ EXTI(SI(q))(SI(i)) = { } p3/ EXTI(SI(q))(x) = { x } for x not SI(i) p4/ CEXTI(SI(c)) = { SI(i) } and some other less interesting stuff Then we get c1/ CEXTI(SI(c)) = { u in IOT | E <u,v> in EXTI(SI(p)) such that v in CEXTI(SI(owl:Thing)) } c2/ CEXTI(SI(c)) = { u in IOT | <u,v> in EXTI(SI(q)) implies v in CEXTI(SI(owl:Nothing)) } so from c1 c3/ <SI(c),SI(owl:Thing)> in EXTI(SI(owl:someValuesFrom)) c4/ <SI(c),SI(p)> in EXTI(SI(owl:onProperty)) and also c5/ <SI(c),SI(owl:Nothing)> in EXTI(SI(owl:allValuesFrom)) c6/ <SI(c),SI(q)> in EXTI(SI(owl:onProperty)) but then from c4 and c5 we get c7/ CEXTI(SI(c)) = { u in IOT | <u,v> in EXTI(SI(p)) implies v in CEXTI(SI(owl:Nothing)) } and then (with p4) c8/ <SI(i),v> in EXTI(SI(p)) implies v in CEXTI(SI(owl:Nothing)) which contradicts p1 and from c3 and c6 we get c9/ CEXTI(SI(c)) = { u in IOT | E <u,v> in EXTI(SI(q)) such that v in CEXTI(SI(owl:Thing)) } and then (with p4) c10/ Ev <SI(i),v> in EXTI(SI(q)) which contradicts p2. Which I suppose is not a complete collapse of the semantics, but is certainly not what you want. > Cheers, > Michael peterReceived on Wednesday, 26 March 2008 01:07:39 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Wednesday, 26 March 2008 01:07:41 GMT
*