- From: <jos.deroo.jd@belgium.agfa.com>
- Date: Fri, 22 Jun 2001 00:01:20 +0100
- To: phayes@ai.uwf.edu
- Cc: aswartz@upclink.com, Jan.Grant@bristol.ac.uk, w3c-rdfcore-wg@w3.org
>>>>I think/hack that both anonymous *terms* can be *unified* >>>>which is NOT the same as equality >>> >>> Then your hack only seems to works when we can unify anonymous >>> terms, or they have some sort of UniqueProperty attached. How do >>> we solve the general case? >> >>There was some related discussion in the telecon >>this afternoon, and I was kind of unable to explain >>my point...(I'm really hopeless in that respect) >> >>The thing about anonymous nodes is that they >>are ***variables*** >>if they would be constants, we would be able >>to identify them with ***URI constants*** >>Now they are actually existentially quantified >>variables, something like: there exists an _:a >>or (using existing vocab): this log:forSome _:a >>So I think we should say that *explicitly* >>is the testresults (and in the model theory) >>(the general case?) > >Well, logically they seem to be like existentially quantified >variables, yes. But you CANT unify distinct existentially quantified >variables (validly) ! They would be distinct skolem constants, which >do not unify in general. (They do if they are existential variables >bound by the same quantifier, but then they would be the same skolem >constant :-) I agree that you CANT unify distinct existentially quantified variables in the sense that one does with universally quantified variables i.e. computing a MGU (Most General Unifier) but what we actually compute is a LCU (Least Common Unifier) for those anonymous nodes (I mean what those nodes have in common w.r.t. their descriptions and taking into account daml:UniqueProperty properties to succeed/fail), and that seems to work in a logical sense but I'm also wondering why?-) -- Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Thursday, 21 June 2001 18:01:46 UTC