Re: bnodeification

>Hi Pat,
>Sergio will send shortly a deep explanation on the list.
>We don't like your solution (a) because it does not work with any 
>ontology language above RDFS that has implicit existentials (like 
>OWL-Lite and above, DLP, or any fragment of FOL with existential 
>quantification),

It works for any ND proof theory for FOL because of the Craig 
interpolation lemma. I think it works for all of these if we relax 
the bnode-binding condition slightly, and IMO reasonably, for these 
more expressive languages where existential generalization is 
proof-theoretically trivial, and given that we have bnodes themselves 
as possible bindings. In the limit, we can allow bnodes to be 'bound' 
to themselves.

>and (b) because the introduction of the scoping graph breaks the 
>subsequent algebra when multiple basic graph patterns are involved 
>(e.g., UNION).

No, it only requires that the scoping graph be used properly. See my 
reply to Sergio.

>  BTW, we already found and discarded a similar solution long time ago :-)

Im not surprised you found it, it is rather obvious once one stops 
being dazzled by the syntactic difference between variables and 
bnodes :-) Its obviouslness is why it is so simple and clear, which 
is why I like it.

Pat

>
>cheers
>--e.


-- 
---------------------------------------------------------------------
IHMC		(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32502			(850)291 0667    cell
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes

Received on Thursday, 12 January 2006 16:14:38 UTC