Re: skolems: visible differences?

On 12/10/07 7:22 AM, Jeremy Carroll wrote:
>
>
>
> Boris and Bijan, amongst others, seem to support the use of skolems 
> for bnodes.
>
> ===
>
> I think that this is an implementation detail, and hence not 
> appropriate for a specification. Since Boris and Bijan *are* 
> suggesting that it should be specified, I suspect I have misunderstood.

I think what is being suggested to use skolemization for defining the 
semantics but not for the syntax. At least, this would be my preference 
so we continue using bnodes and existing parsers but some entailments 
would change. But the change would be for the better and would match 
with how most (if not all) OWL users understand how bnodes work.

>
> ===
> So I have some questions:

Let me take a shot at answering this. The answers reflect my 
understanding and my preferences, any corrections are welcome.

> If we agree to specify the use of Skolems, what visible difference 
> does it make (e.g. in terms of tests)
>
> a) are Skolem constants permitted in a serialization of a ontology 
> read in with bnodes?

My personal perference would be to serialize them again using bnodes.

>
> b) would any document become consistent (or inconsistent) with bnodes 
> as skolems, whereas it is inconsistent (or consistent) with bnodes as 
> existentials

No, I don't think this would happen. The only difference would be in 
entailments.

>
> c) would any entailment (or non-entailment) with out bnodes in the 
> conclusion, become a non-entailment (or entailment) with bnodes as 
> skolems, as opposed to bnodes as existentials.

An entailment could become a non-entailment since skolemization is 
weaker than existentail bnode semantics. I don't think a non-entailment 
could become an entailment.

To give some specific example from OWL test suite the tests 
allValuesFrom-02 [1], someValuesFrom-01 [2] and someValuesFrom [3] use 
bnodes in the conclusions document. The test allValuesFrom-02 is a 
non-entailment and would stay a non-entailment (it tests that 
allValuesFrom restriction cannot infer an existence of a new individual 
which is still true under skolemization semantics). The other two tests 
are entailment tests that tests someValuesFrom restrictions can be used 
to infer the existence of new individuals (and also infer the types of 
those individuals). These tests would turn into non-entailments because 
the reasoner would assign a different skolem constants to the bnodes 
used in the conclusions files and the premises ontology would not infer 
the existence of such specific skolem constants.

>
> d)
> Does the following entailment hold with bnodes as skolems:
>
> _:a rdf:type owl:Thing
>
> entails
>
> _:a rdf:type owl:Thing
>
> ?
>
> If yes, why?

My understanding is, in the most general case, the entailment would not 
hold similar to the above case. The usage of bnode _:a could be assigned 
different skolem constants for the premises and conclusions triples. In 
a specific situation, it might be the case that the same skolem constant 
could be used for both bnodes and entailment would hold. One example I 
have in mind is the way Pellet-Jena coupling works right now. Jena 
assigns unique AnonId objects to identify bnodes and Pellet uses these 
AnonId's to create skolem constants for that bnode. In an API call, if a 
Resource with AnonId is used then the same skolem constant would be 
assigned and the entailment would hold.

>
> =====
>
> Any further hints as to why I may be misunderstanding would be helpful

Cheers,
Evren


[1] http://www.w3.org/2002/03owlt/allValuesFrom/Manifest002.rdf
[2] http://www.w3.org/2002/03owlt/someValuesFrom/Manifest001.rdf
[3] http://www.w3.org/2002/03owlt/someValuesFrom/Manifest003.rdf

>
> Jeremy
>
>
>

Received on Monday, 10 December 2007 14:22:04 UTC