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

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 Sunday, 13 January 2008 18:19:46 UTC