Re: ACTION-93 / ISSUE-63: Initiated work on OWL-1.1-Full semantics

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

peter

Received on Wednesday, 26 March 2008 01:07:39 UTC