Re: RDF Semantics: RDFS entailment lemma

>...
>
>>>>In order to prove the closure lemma, I need to somehow show that this
>>>>is the *only* way that the above entailment rule could possibly be
>>>>invoked.
>>>
>>>Why?
>>
>>Because the entailment rule I mentioned
>>
>>(x type A |- x type B) |- A subClass B
>>
>>is in fact valid, and follows from the 'iff' in the semantic
>>condition on subClassOf.
>
>I would like to ask a further question and describe a simple example
>that seems relevant.
>What is the meaning of the antecedent of this rule,
>(x type A |- x type B), described in more detail on the level of the
>closure generation process in Section 4.2?
>It seems that the rule cannot mean the following:
>apply the closure generation process with the current rules
>rdfs1 - rdfs12; if, afterward, for each x type A, also x type B holds,
>then infer A subclass B.
>For example, the RDF graph
>   a type A .
>   a type B .
>   b type B .
>does not rdfs-entail the RDF statement
>   A subclass B . (*)

It does not mean that, indeed.

It is meant that a derivation exists of the following form:
xxx type A
....
xxx type B

ie *with the variable xxx (or indeed any other expression) in place* 
throughout the derivation. If one can do that, then that entailment 
must hold for *every* xxx (under any other assumptions that are used 
in the derivation); and if that is true, then A subClass B must also 
be true (or, a consequence of those other assumptions). Your example 
provides just such a subproof with a variable: given that we assume
rdf:type rdfs:subPropertyOf P .
P rdfs:domain yyy .
then we can derive as follows:
xxx type A .
xxx P A .
xxx type yyy .

But of course then one has to allow these inference rules to be 
treated not merely as closure rules, but more like real inference 
rules in a natural deduction logic where there are genuine variables 
in the language. I have no problems with this in principle; but we 
have gone to considerable lengths to try to keep the RDF semantics 
simple, and rules like this would be a huge step in terms of 
complexity and sophistication of the RDF 'proof theory'.

There is  a similar inference rule in natural deduction systems for 
classical logic, where the ability to derive Q from P is considered 
to be a proof of (P implies Q); in the above shorthand,
( P |- Q) |- (P implies Q).

>In terms of the proof in the appendix: the Herbrand interpretation
>of the RDFS closure of this graph is not an RDFS interpretation because
>the iff condition for subClassOf is not satisfied, in turn because
>the statement (*) is not in the RDFS closure.

Right, the proof needs to be modified. One way, sketched briefly in 
the document, is to talk about subinterpretations of Herbrand 
interpretations (which I may need to do in any case in order to 
handle the XMLLiterals properly). An alternative is to include the 
above inference rule in an extended rule set, prove the closure lemma 
with respect the the Herbrand interpretation of this extended notion 
of closure (which ought to be semi-obvious if it is stated properly), 
and the show that these 'extra' rules will produce the same extension 
as the existing rules, which will be tiresome but elementary.  But 
this is only a plan of attack: I havnt tried writing this out yet.


>(For this reason this example seems to contradict the last-call version
>of the RDFS closure lemma, which does not yet introduce
>sub-rdfs-interpretations for dealing with XMLLiterals.)
>
>>So in order to show that this rule can be
>>omitted from a complete rule base I have to show that any possible
>>application of it is already covered by some other inference path.
>>There is in fact a valid such rule for subPropertyOf as well, but no
>>way it could possibly be invoked by an RDFS subproof, so that one can
>>be safely omitted.
>>
>>>
>>>>The only way I can see how to do this at present is by an
>>>>exhaustive analysis of the rule base, but I bet there is some elegant
>>>>way to do it which I don't have time to think of.
>>>
>>>
>>>>
>>
>
>Another comment related the rdfs entailment lemma:
>the latest editor's versions contain another new rdfs closure rule,
>rdfs11.
>It seems that the validity of this rule is not yet guaranteed by
>a corresponding condition in the definition of rdfs interpretations.

Indeed, an editorial slip. Thanks for catching this, I will fix it at once.

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

Received on Wednesday, 16 April 2003 16:59:16 UTC