Re: substantive semantics change?

>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