W3C home > Mailing lists > Public > www-rdf-comments@w3.org > April to June 2003

Re: RDF Semantics: RDFS entailment lemma

From: <herman.ter.horst@philips.com>
Date: Wed, 23 Apr 2003 17:30:19 +0200
To: pat hayes <phayes@ai.uwf.edu>
Cc: www-rdf-comments@w3.org
Message-ID: <OFD4ADE49E.F756D268-ONC1256D11.004BC6A8-C1256D11.00555213@diamond.philips.com>

>>...
>>
>>>>>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'.

I was wondering about the question of validity, and about whether it
would be possible to stay within the current theoretical context
and within the current way of describing closure, as this might
keep things simpler.
It seems that the reasoning you describe might be captured without 
'real inference rules' and without 'genuine variables', purely within 
the context of current RDF semantic theory and closure rules, by proving
something like the following:

"Lemma A" If the merge of an RDF graph G and the RDF statement
x type A  rdfs-entails the RDF statement  x type B, 
where x is a uri not appearing in G, then G rdfs-entails the RDF
statement  A subclassof B.

A corollory of such a "lemma" would be that the following
more genuine closure rule would be rigorously valid:
If the rdfs closure of G merged with  x type A  contains  x type B,
then the following may be added to the rdfs closure of G: 
A subclassof B.
This resembles the deduction theorem of classical first-order logic
(Hilbert style reasoning, no natural deduction).
This "closure rule" might be applied at any time, using any pair of 
classes A and B.  However, it would indeed be a huge step in terms 
of complexity and sophistication.

Described in this way, it is not yet clear why a similar rule would not
be needed for subPropertyOf.


>
>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.

It seems that both lines of attack would need subtle reasoning with
subinterpretations.  For example, suppose that one wants to prove
"Lemma A" above.  Then an arbitrary rdfs interpretation I of G
should be proved to satisfy A subclassof B.
I can be extended to satisfy x type A, and be extended again to
get an rdfs interpretation J of G merged with x type A.
Then J satisfies x type B.  But how to conclude that its
subinterpretation I satisfies x type B?

>
>
>>(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.

It seems that this is not yet done in the version of yesterday.

>
>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
>
>

Herman
Received on Wednesday, 23 April 2003 11:44:35 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Friday, 21 September 2012 14:16:32 GMT