W3C home > Mailing lists > Public > www-webont-wg@w3.org > June 2002

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

From: pat hayes <phayes@ai.uwf.edu>
Date: Tue, 25 Jun 2002 12:46:01 -0500
Message-Id: <p05111b12b93e5a131b80@[65.217.30.113]>
To: Dan Connolly <connolly@w3.org>
Cc: www-webont-wg@w3.org

>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. 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).

>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.)

>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? 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. That seems 
capricious to me. And the answer is, no, there isn't any logical name 
for that.

Pat

-- 
---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes
Received on Tuesday, 25 June 2002 13:46:06 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:50 GMT