Semantics tweaks in http://www.ihmc.us/users/phayes/RDF_Semantics_LC2.html

In addition to removing the Lbase appendix and stitching up the 
resulting patches, I have slightly re-phrased (simplified) some of 
the terminology in the proofs appendix, and inserted the following 
just after the interpolation lemma. This may help address some of 
Peter's complaints about the rule sets being incomplete. I prefer to 
keep it inside an informative appendix, however.

Comments, suggestions for improvements, etc., send them fairly 
quickly, obviously. Jeremy, I would prefer to cite an actual paper of 
yours if there is one: send me details (again?? Sorry if so) and I 
will patch it in early Monday if you like.

This seems to pass all the filters, apart from the this-version stuff 
in the header obviously.  I guess the references will need to be 
updated before final release also. Otherwise its done, as far as Im 
concerned right now.

-Pat

--

Interpolation Lemma. S entails E if and only if a subgraph of S is an 
instance of E. QED.

This lemma can be used as the basis for several different mechanical 
processes for checking simple entailment. One way to characterize 
entailment syntactically is in terms of inference rules which apply 
to a set S and can be used to derive E just when S entails E. For 
example, a slight modification of the simple entailment rules 
described in section 7.1 will suffice, where we allow new blank nodes 
to be allocated to existing blank nodes as well as to URI references 
and literals:

extended simple entailment rules.

Rule name

If E contains

then add

xse1

uuu aaa xxx .

uuu aaa _:nnn .

where _:nnn is a blank node identifier allocated to xxx by rule xse1 or xse2.

xse2

uuu aaa xxx .

_:nnn aaa xxx .

where _:nnn is a blank node identifier allocated to uuu by rule xse1 or xse2.

These rules allow blank nodes to proliferate, producing highly 
non-lean graphs; they sanction entailments such as

ex:a exp ex:b .
ex:a ex:p _:x . by xse1 with _:x allocated to ex:b
ex:a ex:p _:y . by xse1 with _:y allocated to _:x
_:z ex:p _:y . by xse2 with _:z allocated to ex:a
_:u ex:p _:y . by xse2 with _:u allocated to _:z
_:u ex:p _:v . by xse1 with _:v allocated to _:y

It is easy to see that if S is an instance of T then one can derive S 
from T by applying these rules in a suitable sequence; the rule 
applications required can be discovered by examination of the 
instance mapping. So, by the interpolation lemma, S entails E iff one 
can derive (a graph containing) E from S by the application of these 
rules. However, it is also clear that applying these rules naively 
would not result in an efficient search process, since the rules will 
not terminate and can produce arbitrarily many redundant derivations 
of equivalent triples.

The general problem of determining simple entailment between 
arbitrary RDF graphs is decideable but NP-complete. This can be shown 
by encoding the problem of detecting a subgraph of an arbitrary 
directed graph as an RDF entailment, using blank nodes to represent 
the graph (observation due to Jeremy Carroll.)


-- 
---------------------------------------------------------------------
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 Friday, 26 September 2003 17:31:17 UTC