- From: pat hayes <phayes@ihmc.us>
- Date: Wed, 12 Nov 2003 11:04:48 -0600
- To: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>
- Cc: w3c-rdfcore-wg@w3.org
>pat: >> > 8. (related). The definitions of rdf and rdfs entailment have been >> > simplified so that they do not make explicit reference to a >> > vocabulary. This is actually more conventional; and Herman pointed >> > out that the more complicated definitions meant that entailment might >> > not be transitive (aargh). The motive for introducing this >> > complication in the definition in the first place has been removed by >> > subsequent changes. This doesn't change any test cases. >> > >jeremy: >> My understanding is that test cases do change - in particular the >> test cases >> >> >> > rdfms-seq-representation/Manifest.rdf#test002 >> > rdfms-seq-representation/Manifest.rdf#test004 >> >> which were incorrect according to the LC2 semantics doc, now >> become correct. >> So this is a substantive rather than an editorial change. (I am awaiting >> feedback from HP implementors concerning this) >> > >Further, as far as I understand, the Last Call 2 doc had the empty document >entailing only a finite number of ground triples No, it has always entailed an infinite number of them of the form rdf:_n rdf:type rdf:Property . They weren't in the 'closure', as we once defined it in the closure lemmas - and that was the point of going through all this contortion involving crdfV - but they were entailed, in the sense that { } entails {rdf:_n rdf:type rdf:Property .} was a true statement (in LC2 and now.) Since the lemmas are no longer stated in terms of closures, and that was the only reason for the crdfV restriction, this change seemed to me to be purely internal to the semantics. >, whereas the current >editors draft has the empty document entailing an infinite number of ground >triples. >HP is unlikely to implement such a change, and would oppose it, if it were >formally proposed. Well, Im not sure what that word 'implement' means. The MT doesn't constrain a reasoner to be strongly complete wrt entailment, and certainly not a forward rule-based reasoner. But this is an issue with forward reasoners in just about any language. Such a reasoner for propositional calculus would have the same issue: the set of tautologies is infinite. >Moreover, since this substantive change (assuming my understanding is >correct) had not been highlighted before the PR vote, we may need to ask the >chairs to rewind history a little. > >I don't follow the transitivity argument ... > >G entails H if every interpretation of G is an interpretation of H. > >this is clearly transitive Yes, phrased this directly it is, which is why I like this direct phrasing. LC2 doesnt state it this directly, which is where the problems arose. Pat >, and a "counter-example" like > >*empty* > entails >rdf:_1 rdf:type rdfs:Resource > entails >rdf:_1 rdf:type rdfs:ContainerMembershipProperty > >is flawed because the first entailment is false according to the LC2 >semantics. > >Is it possible to undo some of the changes to semantics without it falling >apart, leaving hermann and/or peter dissatisfied? > >Jeremy -- --------------------------------------------------------------------- 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@ihmc.us http://www.ihmc.us/users/phayes
Received on Wednesday, 12 November 2003 12:04:49 UTC