Re: TEST: Re: notes for 6/6 until 1:10 (oneOf/sameClassAs)

Stepping off a small cliff here....

Text quoted in the following is excerpted from the full message at
http://lists.w3.org/Archives/Public/www-webont-wg/2002Jun/0183.html  Context
is given only where it is necessary to understand what I'm saying, not why or
who said what's quoted.

There were several examples in the cited email (and its predecessors) that I'd
like to propose restating with explicit assumptions about the implicit
existentials.  I want to know whether the restatements are unacceptable.  If
they are, then we may really have to deal with issues like
5.10-DAML+OIL-semantics-is-too-weak, but if the restatements are acceptable
maybe they provide a way out.

Example 1:
> >i.e. from nothing, conclude:
> >
> >[ owl:oneOf ( :a :a :b ) ] owl:sameClassAs [ owl:oneOf ( :b :a :a ) ] .

Restatement:

from
[owl:oneOf (:a :a :b)]                     the class owl:oneOf (:a :a :b)
exists
and
[owl:oneOf (:b :a :a)]                     the class owl:oneOf (:b :a :a)
exists
conclude
[ owl:oneOf ( :a :a :b ) ] owl:sameClassAs [ owl:oneOf ( :b :a :a ) ] .

or even

from
classExists :a
and
classEexists :b
conclude
[ owl:oneOf ( :a :a :b ) ] owl:sameClassAs [ owl:oneOf ( :b :a :a ) ] .


(where classExists is just a shorthand for a statement that the class exists,
either using existing owl vocabulary or through some new mechanism)

After all, if the classes :a and :b don't exist, what would the consequent
statement mean, anyway?



Example 2:
> ...the inference for (P and Q) from (Q and P)... in class
> language requires...:
> the existence of the class (P intersect Q) entails the existence
> of the class (Q intersect P).


Restatement:

from
exists P, exists Q, (P and Q)
conclude
(Q and P)

or

from
classExists (P intersect Q)
conclude
classExists P
and
classExists Q
and
classExists (Q intersect P)


Example 3:

>   (forall (?x ?L)
>     (=> (ow:item ?L ?x)
>         (exists (?ex1) (and (rdf:type ?x ?ex1) (owl:oneOf ?ex1 ?L))) ) )

Restatement:
pull the existential (as a special predicate) into the antecedent of the
implication, i.e.

 (forall (?x ?L ?ex1)
    (=> (and (classExists (?ex1))
                (ow:item ?L ?x))
         (and (rdf:type ?x ?ex1)
               (owl:oneOf ?ex1 ?L))) ) )


Again, if ?ex1 doesn't exist, then what on earth could the original statement
mean?  (And the existence as a class of ?ex1 could be derived automatically
from the existence as a class of each of the elements in ?L....)

Received on Wednesday, 26 June 2002 13:42:48 UTC