- From: Dan Connolly <connolly@w3.org>
- Date: 26 Jun 2002 12:09:08 -0500
- To: pat hayes <phayes@ai.uwf.edu>
- Cc: www-webont-wg@w3.org
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