From: <herman.ter.horst@philips.com>

Date: Tue, 11 Mar 2003 13:54:20 +0100

To: pat hayes <phayes@ai.uwf.edu>

Cc: www-rdf-comments@w3.org

Message-ID: <OF8FAF9B7D.B88D197E-ON41256CE5.003BC80F-C1256CE6.00470DDB@diamond.philips.com>

Date: Tue, 11 Mar 2003 13:54:20 +0100

To: pat hayes <phayes@ai.uwf.edu>

Cc: www-rdf-comments@w3.org

Message-ID: <OF8FAF9B7D.B88D197E-ON41256CE5.003BC80F-C1256CE6.00470DDB@diamond.philips.com>

>> > >>>First, the truth of the axiomatic triple >>> >>>rdfs:range rdfs:domain rdf:Property . >>> >>>and the semantic conditions on rdfs:domain together require that >>> >>><x,y> inIEXT(I(rdfs:range)) implies x in ICEXT(I(rdf:Property)) >>> >>>which in turn, by applying the condition (definition if you like :) >>> >>>IP= ICEXT(I(rdf:Property)) >>> >>>means that >>> >>><x,y> in IEXT(I(rdfs:range)) implies x in IP >>> >>>Similarly y is in IC, using a different axiomatic triple. >>> >>>Is this more convincing? >> >>No: you use in this reasoning the conditions which >>I claimed are not complete in their statement. > >I do not think that I do use them. I will present the argument in more detail. > >1. I |= rdfs:range rdfs:domain rdf:Property . [axiomatic triple] >2. <I(rdfs:range), I(rdf:Property)> in IEXT(I(rdfs:domain)) >[1., basic RDF truthconditions] >3. <x,y> in I(rdfs:range) implies x in ICEXT(I(rdf:Property)) >[2., semantic conditions on rdfs:domain] >4. <x,y> in I(rdfs:range) implies x in IP [3., definition of IP] > >Note, step 3 does not depend on x being in any particular class; it >simply uses the semantic conditions in the form they have in the >document. None of this derivation implicitly assumes anything other >than what is stated, and it has as a conclusion the 'assumption' that >x is in IP. An exactly similar derivation (replace rdfs:domain by >rdfs:range, rdf:Property by rdfs:Class and IP by IC) shows that y is >in IC. So these assumptions are derivable, so are not needed. > >>The domain and range conditions as they are now formulated >>implicitly assume that x is in IP and y is in IC, > >If you still maintain that these assumptions are used implicitly, >please give details of where the above derivation fails. Your proof works, contrary to what I said earlier. It is satisfactory that this can be proved. I apologize that I did not look closely enough to your previous version of the proof. It still seems to me that the proof uses an implicit assumption. To be precise, in Step 3. The following description of the proof puts this step under the microscope. Claim: If I is an rdfs-interpretation and <u,v> is in I(rdfs:range) then u is in IP and v is in IC and similarly for rdfs:domain. Proof: >1. I |= rdfs:range rdfs:domain rdf:Property . [axiomatic triple] >2. <I(rdfs:range), I(rdf:Property)> in IEXT(I(rdfs:domain)) >[1., basic RDF truth conditions] 3a. If <x,y> is in IEXT(I(rdfs:domain)) [and x is in IP and y is in IC] and <u,v> is in IEXT(x) then u is in ICEXT(y) [full semantic condition on rdfs:domain] (Note: such an addition is needed because otherwise it is not clear that the function invocations IEXT(x) and ICEXT(y) are legal, as it is not yet proved that x is in IP (the domain of IEXT) and y is in IC (the domain of ICEXT). In my earlier mails I made the addition after 'then'. However, in the light of your proof this seems better.) 3b. x:=I(rdfs:range) is in IP [semantic condition] 3c. y:=I(rdf:Property) is in IC [semantic condition] 3d. <u,v> in I(rdfs:range) implies u in ICEXT(I(rdf:Property)) [2.,3a.,3b.,3c.] 4. <u,v> in I(rdfs:range) implies u in IP [3d., definition of IP] And similarly for the rest of the claim. So the addition "[and x is in IP and y is in IC]" to 3a seems to be needed as a kind of bootstrap to arrive at the claim. This bootstrap addition would not be needed if another proof of the claim can be given without the use of the domain and range conditions. It seems natural to add a lemma to the text for the claim and the proof. If the "bootstrap additions" are left out of the domain and range conditions in the table, then the full domain and range conditions 3a (and similarly for rdfs:range) should be mentioned with the lemma, in my view. A disadvantage of leaving these bootstrap additions out of the table would be that understanding a statement in the (normative) table would require an (informative?) lemma. > >Best wishes Same to you (I am sorry that I could not reply earlier, as I was away from my email. With this mail and the next I hope to finish our discussion about the last call semantics document as quickly as possible.) > >Pat > > >-- >--------------------------------------------------------------------- >IHMC (850)434 8903 or (650)494 3973 home >40 South Alcaniz St. (850)202 4416 office >Pensacola (850)202 4440 fax >FL 32501 (850)291 0667 cell >phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes >s.pam@ai.uwf.edu for spam > > HermanReceived on Tuesday, 11 March 2003 07:56:14 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:15:20 UTC
*