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

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 UTC