- From: Francis McCabe <fgm@fla.fujitsu.com>
- Date: Mon, 9 Jan 2006 11:15:14 -0800
- To: Dave Reynolds <der@hplb.hpl.hp.com>
- Cc: Enrico Franconi <franconi@inf.unibz.it>, public-rif-wg@w3.org
Please forgive my lack of arcane logic .. but it seems to me that the use of gensym here: > kb:works-with(Z,X) :- rdf:type(X,db:employee), gensym(Z). is not sound. Presumably, what is really meant is: kb:works-with(Sy,X) :- rdf:type(X,db:employee) where Sy is some gensym(). I.e., the skolemization should be done once and for all, not on each use of the rule. However, at the moment, I can't see why you would want to skolemize at all .. what is wrong with the rule with the universal quantifier in it? Frank McCabe On Jan 9, 2006, at 9:50 AM, Dave Reynolds wrote: > > Enrico Franconi wrote: > >> On 5 Jan 2006, at 15:51, Dave Reynolds wrote: >>> On the question of bNodes in the head, I hear the argument that >>> it is not sufficient to just treat these as new Skolem constants >>> but my intuitive understanding of the issue is too weak. It >>> would be really helpful if someone could construct a test case >>> which demonstrates the difference in results that arise between >>> correct treatment of bNodes in the head versus treatment as >>> Skolem constants. In the concrete cases I've seen where bNodes >>> are used in the head of rules they seem to be intended as a form >>> of anonymous gensym - so the Skolem constant semantics may be >>> the more practically useful interpretation. >> A a naive gensym would fail the use case <http://www.w3.org/2005/ >> rules/wg/wiki/Managing_incomplete_information>, where two >> examples (in section "9.4. (Rules involving generation of >> unknown)") show how you can make things wrong with a naive use of >> skolem constants to implement the existential variables in the head. > > Sorry to be slow on the uptake but I didn't follow why the examples > break with naive gensym. > > The example in 9.4 on that page shows the rules: > > [[[ > rdf:type(X,db:employee) :- kb:works-with(X,Y). > kb:works-with(Z,X) :- rdf:type(X,db:employee). > ]]] > > A naive implementation of bNodes-by-gensym would rewrite the unsafe > second rule to something like: > > kb:works-with(Z,X) :- rdf:type(X,db:employee), gensym(Z). > > where "gensym/1" returns some freshly minted bNode on each call; > > or, better, > > kb:works-with(Z,X) :- rdf:type(X,db:employee), gensym(X, Z). > > where "gensym/2" binds Z to some bNode which is a (skolem-)function > of X. > > As far as I can see either of these would return the same answer as > the classical semantics for both of your test cases 9.4.1 and 9.4.2. > > Dave > >
Received on Monday, 9 January 2006 19:15:46 UTC