Re: log:forSome (Was: Model-specific identity for anon resources, and its representation: A new issue?

>>>>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