response to comment pfps-05

The closure rules for RDFS are incomplete.  For example,
     ex:foo ex:prop "a" .
RDFS-entails
     ex:foo ex:prop _:x .
     _:x rdf:type rdfs:Resource .
However, this does not come out of the RDFS closure rules.
This means that the RDFS entailment lemma is false.

------
Indeed, good catch!

This is actually a deeper observation, which is that we need to treat 
the basic entailment operation of generalization (replacing a name 
with a bnode) as a genuine inference rule, and include it in the 
notion of closure. I therefore propose to add the following to 
section 2 (simple entailment), just after the statement of the 
instance lemma:

------
We can summarize the second of these as an inference rule on triples, 
in a style which we will use extensively later in the document. Here, 
ppp stands for any uriref, aaa for any uriref or bNode, and bbb for 
any uriref, bNode or literal.

Rule name se1:

If E contains
aaa ppp bbb .

then add
aaa ppp _:n .

where _:n is a new bNode.


Rule name se2:

if E contains
aaa ppp bbb .

then add
_:n ppp bbb .

where _:n is a new bNode.

'New' means 'not occurring in the graph'. The instance lemma 
guarantees that these rules are valid, so they can be safely used to 
add triples to any RDF graph. There is no inference rule 
corresponding to the subgraph lemma: it would amount to the 
observation that one can ignore a triple.

---

then, in the definition of the RDF (RDFS) closures, we require that 
the closure rules include SE1, SE2 and the RDF (and RDFS) rules.

This is actually a more unified treatment and solves this objection 
(I believe), by the following inference path:

ex:foo ex:prop "a" .
ex:foo ex:prop _:x . by rule SE1
_:x rdf:type rdfs:Resource . by rule RDFS4b

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