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

On Tue, 2002-06-25 at 12:46, pat hayes wrote:
> >On Thu, 2002-06-06 at 17:31, Jos De_Roo wrote:
> >>
> >>  [...]
> >>
> >>  > 3d) Proposal to close issue 2.4 - Enumerated Classes (daml:oneOf)
> >>  > issue:
> >[...]
> >>  > Dan will reconsider a test case posted by Jos.
> >>
> >>  that is actually the one in
> >>  http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0276.html
> >>  "TEST: sameClassAs testcase" [1][2][3]
> >
> >i.e. from nothing, conclude:
> >
> >[ owl:oneOf ( :a :a :b ) ] owl:sameClassAs [ owl:oneOf ( :b :a :a ) ] .
> >
> >
> >Well, my position on 5.10-DAML+OIL-semantics-is-too-weak
> >   http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0235.html
> >is that OWL shouldn't entail the existence of any
> >classes from an empty premise.
> 
> It would be useful to know what your basis is for taking this 
> position. It seems to me to be unreasonable and arbitrary.

It's not arbitrary; it's motivated by technical problems
that come up with theories involving comprehension rules.

Whether it's reasonable or not is what we're here to discuss.

I think it is reasonable; i.e. I think we can advance
the state of the art considerably in the next 6 months
to a year without using any such rules. Maybe we'll
work out the issues around comprehension rules in
future work.

> For 
> example, take the commutativity of conjunction, which when mapped 
> into FOL is the inference for (P and Q) from (Q and P), which seems 
> so blindingly obvious that it is hard to see how one could even 
> formulate a sensible formalism that didnt support it, but in class 
> language requires an inference of the kind you think should  be ruled 
> out: the existence of the class (P intersect Q) entails the existence 
> of the class (Q intersect P).

Well, yes, it's unaesthetic. I don't find that compelling, though,
or even convincing.

Until I looked at the cost of comprehension
rules, I thought it was unacceptably unaesthetic too.

But in actual implementation experience, I haven't run into
any practical uses of intersectionOf etc.
where I need the machine to conclude that classes other than
the ones I told it about exist.


> >i.e. there shouldn't be any axioms with existentials in
> >the conclusions. (there's a name for that fragment of FOL, no?
> >is that horn clauses? I often forget).
> 
> Given that we are talking about Horn clauses (no disjunctions in 
> conclusion), the subcase you are talking about seems to be that the 
> sentences are universal, ie there are no existentials at all. 
> (Existentials in the antecedent become universals over the whole 
> rule.)

OK, yes, those are the ones I want to stick to.

> >So I'm currently against rules such as:
> >   { :rule9o1 . ?L owl:item ?x } log:implies { ?x a [ owl:oneOf ?L ] } .
> >from
> >   http://www.agfa.com/w3c/euler/owl-rules
> 
> I don't follow. That rule doesn't have an existential in the 
> conclusion, does it?

Yes; []'s are short-hand for existentials; i.e. this
is another way to write that rule:

{ :rule9o1 . ?L owl:item ?x } log:implies
   { ?x a _:ex1.
      _:ex1 owl:oneOf ?L  } .

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

> Both the variables in the conclusion are also in 
> the antecedent. You seem to want to rule out any *terms* that refer 
> to classes in the conclusion, not just existentials.

no.

> That seems 
> capricious to me. And the answer is, no, there isn't any logical name 
> for that.
> 
> Pat

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

Received on Wednesday, 26 June 2002 13:08:40 UTC