# Re: RDF Semantics: RDFS entailment lemma

From: pat hayes <phayes@ai.uwf.edu>
Date: Thu, 10 Apr 2003 11:57:31 -0400
Message-Id: <p05111b17babb365cb10c@[10.0.100.86]>
To: herman.ter.horst@philips.com, Brian_McBride <bwm@hplb.hpl.hp.com>

```
Herman, many thanks for your email and the careful checking you have
done. Indeed I had not seen these inference paths. I am considering
the possible options and will get back to you and the WG as soon as

Brian, can you give this an ID (even though the last call is over,
this is a bug that must be fixed.)

Pat
-----------
>It seems that the RDFS entailment lemma as currently stated
>in the RDF Semantics document (last call or editor's version)
>is not entirely correct.
>
>Consider the RDF graph G:
>   x rdf:type rdfs:Class .
>   rdf:type rdfs:domain y .
>
>This RDF graph rdfs-entails the triple
>   x rdfs:subClassOf y .
>
>( Proof: let I be an arbitrary rdfs interpretation of G.
>Clearly I(x) and I(y) are in IC.  Suppose z in ICEXT(I(x)),
>so <z,I(x)> in IEXT(I(rdf:type)).  The second triple shows
>that  <I(rdf:type),I(y)> in IEXT(I(rdfs:domain)).
>With the semantic condition on rdfs:domain it follows
>that z in ICEXT(I(y)), so that <I(x),I(y)> in
>IEXT(I(rdfs:subClassOf)). )
>
>However, this triple is not in the rdfs closure of G,
>unless x = y.

Most ingenious.

>
>(Proof: this closure contains the subClassOf statements
>   x rdfs:subClassOf x .
>   y rdfs:subClassOf y .
>but no other subClassOf statements involving x or y.)
>
>This example could be used as another closure rule ("rdfs11"),
>but then the RDFS entailment lemma would still be false.
>Namely, a slightly more complicated proof shows that
>the graph H:
>   x rdf:type rdfs:Class .
>   rdf:type rdfs:subPropertyOf p .
>   p rdfs:domain y .
>rdfs-entails the triple
>   x rdfs:subClassOf y .,
>but that this triple is not in the (extended definition of)
>closure.

The most general form of the argument I can find is this:

type subProperty p .
p domain y .
x type z .

rdfs-entails

z subClass y .

which is a consequence of the '..and only if' condition on
rdfs:subClassOf. The inference rule which naturally corresponds to
this is rather more complicated than a closure rule: it is more like
the implication-introduction rule in a natural deduction proof
system, where one draws a conclusion from a entire subproof rather
than a set of antecedents. It would look like this:

IF x rdf:type y . |- x rdf:type z .
THEN  y rdfs:subClassOf z .

where it is understood that x here must be a variable, ie in effect
this antecedent amount so the proof that for all x, x type y implies
x type z. This corresponds to the 'only if' part of the semantic
condition on subClassOf.

Presumably there will be a similar phenomenon concerning
subPropertyOf, which will require a similar extension to the rule
base. I will try to cook up an example to illustrate this. As a first

subProperty subProperty p .
....

>I found these examples in an attempt to become completely convinced
>of the truth of the rdfs entailment lemma.
>In this attempt I did become convinced of the "soundness" part of
>the lemma.

Right. That is pretty simple, of course. All the difficulty is in the
completeness part.

>  For the "completeness" part of the lemma, it would perhaps
>be simpler, and still very useful, to restrict the lemma to
>"well-behaved" RDF graphs, which might be defined as RDF graphs which
>do not make (RDF) statements about built-in (rdf or rdfs) vocabulary
>in addition to the statements given by the axiomatic triples.

That is one possibility, although I am by no means sure that the
think you have found a more basic weakness in the rule base, and that
a 'well-behaved' graph could be constructed which would exhibit the
same problem. And in any case I would prefer to have a more general
solution if I can think of one in time :-)

I will get back to y'all in a few days when I get back from
travelling and have time to digest this properly.

Pat

>
>Herman ter Horst

--
---------------------------------------------------------------------
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 Thursday, 10 April 2003 11:57:35 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:44:02 UTC