- From: pat hayes <phayes@ai.uwf.edu>
- Date: Tue, 4 Feb 2003 11:17:37 -0600
- To: "Massimo Marchiori" <massimo@w3.org>
- Cc: <w3c-rdfcore-wg@w3.org>, Ossi Nykänen <onykane@butler.cc.tut.fi>
> > Sure. Its kind of trivial, though. The basic RDF semantic rules >for simple entailment (in >> fact for any kind of entailment except linear logics) support the >>rule that if A entails B >> then A entails (A and B), since A entails A trivially. The >>inference cited is simply a >> special case of that. >That works in logic, but it's not at all a proof of the entailment. Yes, it is, since RDF *is* a logic in the required sense. >Because, what is the "and" you are referring to? In RDF, it amounts to the operation of forming a union of some sets of triples from those sets. >More specifically, as said in the Bag/Alt issue text, I think you >confused the "and" cited above with something you call "conjoin", I identified them, but that is not a confusion. They are the same. >which does a straight merge, but that is not a derived operation >from the entailment. It is always valid to take the union of two sets of triples, and the operation corresponds to simple propositional conjunction. >Remember the discussion we had about the presence in the RDF Model >Theory of a wrong definition of merge and blank node renaming? I remember the discussion, but it is not relevant to this point. Renaming bound variables is an issue that comes up in conventional logical notations when conjoining two expressions which implicitly come from different quantifier scopes. The entailments in question here all are *inside* the quantifier scopes; that is why the same bnode ID is used in the Ntriples notation. So renaming is irrelevant here. Here is a formal proof, if you really want to see it. Let us suppose that some valid process of inference is given the graph _:xxx rdf:type rdf:Bag . _:xxx rdf:_1 <ex:a> . _:xxx rdf:_2 <ex:b> . and infers the conclusion _:xxx rdf:_1 <ex:b> . where that nodeID indicates the *same* bnode, notice. (That is, intuitively, the conclusion is not merely that something exists which has the first element ex:b, but that the thing that has the first element ex:a also has the first element ex:b.) Then the graph (set of triples, recall) which contains all four triples is entailed by the first graph. Clearly, adding a triple which is validly entailed by a graph to that graph preserves the truth of the graph; that is how the closure rules work, for example. Similarly, if the first graph also entails _:xxx rdf:_2 <ex:a> . then the graph containing all five triples is entailed by the first graph (in fact, it is equivalent to it.) I am not sure how much more detail you need. I cannot give you a fully formal line-by-line proof since we have never defined a formal proof theory for RDF, but the above argument uses the concepts and results from the RDF semantics document rigorously. If we had a formal natural-deduction style proof theory, the point could be made as follows: renaming is a mechanism for handling the requirement that existential elimination always uses a new name. The conjunction-introduction rule has got nothing to do with existential elimination, however, and we are only talking about purely propositional inferences here. The point is so obvious that I am rather at a loss to explain it further, to be honest. If you feel it is in any way faulty, please explain why. Pat >This is a related consequence. > >So, I'll still await for a proof (no t-shirts allowed ;) >Thanks, >-M > > > >-----Original Message----- >From: pat hayes [mailto:phayes@ai.uwf.edu] >Sent: Tuesday, February 04, 2003 4:52 PM >To: Massimo Marchiori >Cc: w3c-rdfcore-wg@w3.org; Ossi Nykänen; Massimo Marchiori >Subject: RE: RDF Semantics: Interpretations and Modelling > > >Pat, this reply brought to my mind a lovely Sidney Harris' t-shirt >that Leslie Lamport showed me for the first time ten years ago or >so (wow, time flies....): http://www.scienceteecher.com/proof.htm >Can you please give a proof of your entailment? ;) >Thanks, >-M > > > >Sure. Its kind of trivial, though. The basic RDF semantic rules for >simple entailment (in fact for any kind of entailment except >linear logics) support the rule that if A entails B then A entails >(A and B), since A entails A trivially. The inference cited is >simply a special case of that. > > >Can you, in turn, say why you think this is wrong? > > >Pat > > > > > >Ossi, this is the Bag/Alt issue, raised in May 2002: > >http://lists.w3.org/Archives/Public/www-rdf-comments/2002AprJun/0112.html >AFAIK never replied yet. >Incidentally, the same wrong argument pointed therein appears again >in the current last call draft. > > > >Im not sure which 'wrong argument' you are referring to. I stand by >everything I said that is included in the above-referenced >message. In particular, > > >" If >_:xxx [rdf:type] [rdf:Bag] . >> _:xxx [rdf:_1] <ex:a> . > > _:xxx [rdf:_2] <ex:b> . >> >> entails >> > > _:xxx [rdf:_1] <ex:b> . > > _:xxx [rdf:_2] <ex:a> . >> >> then it also must entail >> >> _:xxx [rdf:type] [rdf:Bag] . >> _:xxx [rdf:_1] <ex:a> . >> _:xxx [rdf:_2] <ex:b> . >> _:xxx [rdf:_1] <ex:b> . >> _:xxx [rdf:_2] <ex:a> . >> >> and by suitable reordering, it will entail that ALL members of the >> bag are in ALL positions." > > >is a correct argument, and your response to it is incorrect. > > >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 > > > > >-- > >--------------------------------------------------------------------- >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 -- --------------------------------------------------------------------- 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
Received on Tuesday, 4 February 2003 12:16:13 UTC