Re: Proposal and Test cases (Re: skolems: visible differences?)

Thanks

so entailment with existential semantics is undecidable.

I don't see this as a problem if we do not specify a conformance label 
for entailment. We perhaps ought to have a disclaimer concerning 
entailment and non-entailment tests to that effect.

In terms of whether an ontology does or does not entail

(1)  hor(_:1,_:2)
(2)  ver(_:2,_:3)
(3)  ver(_:1,_:4)
(4)  hor(_:4,_:5)
(5)  _:3 != _:5

the naive explanation of bnodes as existentials - does this pattern of 
relationships occur or not? (with any labels, or not), seems not much 
less intuitive, and substantially more interesting than does this 
pattern of relationships between the given labels (once skolemized) 
occur (for which as Boris notes, is trivial).

As far as I can see, this example acts as a critique of entailment 
tests, and argues that we should be cautious with them, rather than a 
critique of existential semantics.

It doesn't seem to suggest there is a consistency test that is undecidable.

Jeremy





Bijan Parsia wrote:
> 
> On 17 Jan 2008, at 14:22, Jeremy Carroll wrote:
> 
>> Bijan Parsia wrote:
>>> Furthermore such variables have far reaching consquences both
>>> formally (e.g., on the data complexity of RDFS; undecidability of OWL 
>>> DL+ cyclic bnode patterns; what sorts of entailments occur)
>>
>> Remind me about the "undecidability of OWL DL+ cyclic bnode patterns" 
>> - I seem to vaguely remember briefly getting my head round it once, 
>> but it's gone.
> 
> See Boris' explanation:
>     http://www.w3.org/mid/000701c82200$d343cf00$2711a8c0@wolf
> 
>> Is the statement that say using the existential semantics with bnodes 
>> for individuals in OWL DL takes us into undecidability?
> 
> IIRC, you need inequality as well, but yes. Ah yes, see his even earlier 
> explanation:
>     http://www.w3.org/mid/000601c82176$e8a3b700$2711a8c0@wolf
> 
> It contains the reference.
> 
> Cheers,
> Bijan.
>

Received on Thursday, 17 January 2008 14:55:35 UTC