Re: skolems: visible differences?

On 14 Jan 2008, at 09:54, Jeremy Carroll wrote:
> Hmmm, interesting ....
> a very simple question.
>
> Bijan Parsia wrote:
>> On Jan 12, 2008, at 11:52 PM, Alan Ruttenberg wrote:
>>> Testing my understanding of the skolem constant proposal for  
>>> anonymous individuals:
>>>
>>> If we adopted the treatment of bnodes as skolem constants, would  
>>> it be the case that we no longer had the tree-shape restriction  
>>> for related anonymous individuals?
>> Correct. You could still get *them*, but you would have to encode  
>> them as
>
> The *them* I marked refers to what. I found I couldn't understand  
> this sentence.

Sorry. You could still get tree like patterns of existentially  
quantified variables. So you could have arbitrary graphs of skolem  
constants (syntactic and practice compatibility with RDF) and still  
be able to express everything you could express in OWL 1.0 DL, only  
you have to use a different syntax in some cases.

> But the rest of the message looked very promising.
>
> Maybe give an example, with a non-tree, and explain how it differs.

With a *non* tree?... I don't understand. In OWL Full, you can write:

(1) _:x p _:y. :y p _:z. :z :p _:x.

Where the FOL translation is:

(1') \exists(x, y, z)(p(x, y) \land p(y,z ) \land \p(z, x))

This is not in OWL 1.1 or OWL DL and, as Boris has explained, leads  
to undecidability.

I propose we translate it as:

(1'') p(skol(x), skol(y)) \land p(skol(y),skol(z)) \land \p(skol 
(z),skol(x))

1'' and 1' are equisatisfiable but not equivalent, 1'' entails 1' but  
not vice versa.


>> existential restrictions, or using Carsten's proposed universal role.
>
> ====
>
> I have no in principle opposition to skolemization. On the  
> contrary, given that many implementations use the technique, the  
> specs should, in my view, permit such an implementation (and do so  
> explicitly if there is  any room for doubt). I always understood  
> the OWL 1.0 specs as permitting such an implementation.

This is not an implementation technique issue. It's whether 1  
translates to 1' or 1''. Reasoning is much easier with 1'' and the  
results are more in line with what RDF systems actually do and what  
(I think, given my experience even in the DAWG) users expect.

> However, the relationship with RDF semantics, which treats bnodes  
> as existentials rather than skolems, needs to be clear.

The semantics are weaker in known ways and perfectly clear, afaict.

> [Concerning the HP position, I am not wholly sure what it would be,  
> and if there was what may be thought of as a significant change, I  
> would need to refer back to my colleagues. My expectation at this  
> stage is that there may be differences of opinion, resulting in a  
> formal abstention from HP. i.e. at this stage, I can't promise to  
> deliver an HP vote, but Bijan's message seems to indicate a design  
> change that addresses some of HP's concerns]

FWIW, I don't see that this is a design change from the any  
"skolemization" proposal on the table. It *is* a design change from  
OWL 1.0 and from RDF but, I have argued, in a beneficial way.

Cheers,
Bijan.

Received on Monday, 14 January 2008 12:57:44 UTC