W3C home > Mailing lists > Public > w3c-rdfcore-wg@w3.org > February 2003

RE: RDF Semantics: Interpretations and Modelling

From: pat hayes <phayes@ai.uwf.edu>
Date: Tue, 4 Feb 2003 11:17:37 -0600
Message-Id: <p05111b35ba659b2c968b@[10.0.100.86]>
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 EST

This archive was generated by hypermail pre-2.1.9 : Wednesday, 3 September 2003 09:55:48 EDT