- From: Pat Hayes <phayes@ihmc.us>
- Date: Thu, 12 Jan 2006 10:14:21 -0600
- To: Enrico Franconi <franconi@inf.unibz.it>
- Cc: tessaris <tessaris@inf.unibz.it>, Bijan Parsia <bparsia@isr.umd.edu>, souripriya.das@oracle.com, public-rdf-dawg@w3.org
>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