W3C home > Mailing lists > Public > public-owl-wg@w3.org > January 2008

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

From: Bijan Parsia <bparsia@cs.man.ac.uk>
Date: Wed, 16 Jan 2008 13:15:05 +0000
Message-Id: <C82B011B-E528-4AA7-8505-25172C9C2143@cs.man.ac.uk>
Cc: OWL Working Group WG <public-owl-wg@w3.org>
To: Jeremy Carroll <jjc@hpl.hp.com>

On 16 Jan 2008, at 12:18, Jeremy Carroll wrote:

> Hi Bijan,
>
> just to check I've undertstood I thought I would send some of my  
> own tests for your confirmation.

Thanks!

[snip]
> TEST 5:
>     ObjectPropertyAssertion(:p :x _:y)
>
> does not entail
>
>     ObjectPropertyAssertion(:p :x _:y)

I think there's a "there depends" on this one. It's a good test!

Call the first assertion (1) and the second (2).

If (1) and (2) are separate RDF graphs and the entailment question  
comes from parsing (1) (in the traditional way with regard to bnode  
identifiers) then parsing (2) (in the same way) then skolemizing (in  
the standard way) then, yes, Test 5 is correct. It's unfortunate  
because then (surface) syntactically identical graphs don't  
entailment don't entail themselves. It's the flip side of blocking  
things liek:


Test 7:
	ObjectPropertyAssertion(:p :x _:y)

not entailing:

	ObjectPropertyAssertion(:p :x _:z)

and

Test 8:
	ObjectPropertyAssertion(:p :x _:y)

not entailing

	ObjectPropertyAssertion(:p :x _:y)
	ObjectPropertyAssertion(:p :x _:z)

Pick your surprises and take your chances.

One can mitigate the surprise of test 5 by allowing users to set the  
scope of the bnode ids (essentially, where they put the existentials,  
e.g., if you think of the N3 (syntax) rule:
	{:x :p _:y} => {:x :p _:y}

You can put the quantifiers outside the whole rule:
	some Y({:x :p Y} => {:x :p Y})
and then you'll skolemize to a common constant, but if you read it as:
	some Y({:x :p Y}) => some Y({:x :p Y})
you won't.

Worth thinking about.

> TEST 6:
>     ObjectPropertyAssertion(:p :x _:y)
>     ObjectPropertyAssertion(:p :x :z)
>     ClassAssertion( :p ObjectExactCardinality( 1, :x ) )
>
> is consistent

Yes. But this may not be the kind of test you want to make. Since  
skolemization preserves satisfiability, anything that is satisfiable  
under the variable reading will be satisfiable under the skolemized  
reading. (It doesn't preserve entailment, hence the discrepency.)

Cheers,
Bijan.
Received on Wednesday, 16 January 2008 13:13:14 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Wednesday, 16 January 2008 13:13:16 GMT