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

I actually quite like this ...

There is an issue in that some of these tests reverse tests decided upon 
by RDF Core a while ago, and which are out-of-charter for this WG.
(I think Peter's question picked this up).

I wonder if a liberal dose of phrases like "variable" semantics (or 
perhaps "existential" semantics) and ("skolem" semantics), and a brief 
account of how skolem semantics is weaker than existential semantics 
(for entailments only), but identical for consistency checking would 
quite possibly be workable, and not tread too much on RDF toes.

I would tend to imagine that the Full semantics would usually be 
existential; but introducing the terminology, we may find that full 
implementors actually prefer to implement skolem semantics.

I will try and chat with HP implementors. I think Bijan thinks that they 
actually implement Skolem semantics. If this is in fact the case, I 
personally would find it difficult to justify opposing this move - 
despite my ideological biases ... :)

Jeremy




Bijan Parsia wrote:
> 
> To help the discussion, here are a few test cases. I *would* put them 
> into the test case system pipe to discharge my action item, but I'm 
> waiting for instructions (nudge nudge! :))
> 
> To be clear on what's being tested, the proposal as I understand it is:
> 
> Structural Spec
>     1) We replace everywhere "individualURI" with "individualName"
>     2) We add a production for localName (or whatever you want to call 
> it) such that:
>     localName := BNode identifiers from Turtle.
>     4) We change the production
>         individualName := URI
>     to:
>         individualName := URI | localName
> 
> Semantics:
>     1) we add a set of terms N_ln which is disjoint from the other 
> categories
>         This is to restrict bnodes to naming individuals. Given the 
> syntax restrictions above this is probably a bit unnecessary, but it is 
> conservative.
>     2) we extend .^Ii to assign each individual a \in N_ln an element 
> a^II from \Delta_I
> 
> RDF Mapping (going to be a bit sketchier here because I'm not as 
> familiar with the mapping doc):
>     1) We replace everywhere "individualURI" with "individualName"
> 
> (I think that's enough...the intend that is that something like
>     _:x :p _:y.
> goes to
>     ObjectPropertyAssertion(:p _:x _:y)
> and vice versa. Some thought about declaration and typing needs to happen.)
> 
> TEST 1:
>     ObjectPropertyAssertion(:p :x _:y)
> 
> entails:
> 
>     ClassAssertion(:x ObjectSomeValuesFrom(:p, Thing))
> 
> TEST 2:
>     ClassAssertion(:x ObjectSomeValuesFrom(:p, Thing))
> 
> does not entail:
> 
>     ObjectPropertyAssertion(:p :x _:y)
> 
> Test 2 holds under variable (as opposed to skolem) semantics.
> 
> TEST 3:
>     ObjectPropertyAssertion(:p :x :y)
> 
> does not entail
> 
>     ObjectPropertyAssertion(:p :x _:G1)
> 
> Test 3 shows that simple entailment fails.
> 
> Ok, this raises an issue since we have to be able to "rename" BNodes. 
> I.e., given the semantics above:
> 
> TEST 4:
>     ObjectPropertyAssertion(:p :x _:y)
> 
> does not entail   
> 
>     ObjectPropertyAssertion(:p :x _:G1)
> 
> Which is another instance of simple entailment failure. The solution, I 
> think, is to point out that one is permitted to substitue 
> individualNames for fresh individualNames without changing the meaning 
> of an ontology. It might behoove us to define in the struc spec MERGE 
> and UNION operations on ontologies, or, perhaps better, MERGE_ADD and 
> UNION_ADD for axioms. MERGE_ADD treats same bnode id in different 
> ontologies as different (requiring renaming) where as UNION_ADD treats 
> BNode id as sharing scope across the operators. Imports then can be 
> defined in terms of MERGE_ADD.
> 
> Tree like patterns of existential variables can only be written using 
> SomeValuesAs, on this proposal.
> 
> Cheers,
> Bijan.
>

Received on Monday, 14 January 2008 13:00:14 UTC