New entailment pattern rdfD1

[doerthe]

I am currently going through RDF semantics to modify all our entailment patterns in such a way that also triple terms are covered. For most patterns, I can see how we could do that (putting aside the separate issue of whether we like a to have conditions like "if the triple structure appears in S"), but I am not sure how to handle rdfD1 (https://www.w3.org/TR/rdf12-semantics/#rdf_entailment_patterns).

Do we make the left side "if the triple structure appears in S" then "the following structure appears in S at the same position"?

That is really not an acceptable solution. So, how do we express that? To point to the exact issue, I go for an example:

bbb ccc <<( xxx aaa "sss"^^ddd )>>. should(?) entail bbb ccc <<( xxx aaa _:nnn )>>. _:nnn rdf:type ddd .

Now, the problem is that such a literal can occur deeply nested.

I'll try to write down a solution, but ideas are more than welcome.

[niklasl]

I propose the interpretation in w3c/rdf-star-wg#154 as a basis for solving this. (But I will continue to think about unwanted consequences of that approach, based on concerns by e.g. @franconi.)

[afs]

The _:nnn rdf:type ddd . triple is asserted but the reason is only a claim, not an assertion.

[doerthe]

Our current semantics (classical RDF+liberal baseline) says that the entailment
bbb ccc <<( xxx aaa "sss"^^ddd )>>. entails bbb ccc <<( xxx aaa _:nnn )>>. _:nnn rdf:type ddd .
holds.

That means our entailment pattern has to reflect that. Maybe we can add something like replacement of terms by blank nodes to our "Notation and Terminology" section (I did not check whether it even is there) and use it. Somehow, that makes our very simple entailment patters far more complex. But we will see.

I am not sure what exactly you are referring to @niklasl, maybe you can explain? The unstar-vocabulary will not immediately help, because we have to produce a deeply nested triple if we encounter the literal deeply nested. Or do you mean, we "un-star" and "star" again? mmm, maybe... Have to think about it. Advantage would be that we really stay on syntax level and that is what we want.

[doerthe]

The _:nnn rdf:type ddd . triple is asserted but the reason is only a claim, not an assertion.

yes, but the moment the triple term has an interpretation, the _:nnn rdf:type ddd . must be true. So here, it "leaks out". We can of course modify the semantics....

[niklasl]

@doerthe I refer to the entailment I suggest in that issue; i.e. that if bbb ccc <<( xxx aaa "sss"^^ddd )>>. entails (among other statements) _:ttt rdfs:propositionObject "sss"^^ddd., then by rdfD1 _:ttt rdfs:propositionObject _:nnn. _:nnn rdf:type ddd. is also entailed.

As we discussed this "unwraps" triple terms on any level of nesting. I think this is the sensible consequence of transparency?

But I'm also assuming that bbb ccc <<( xxx aaa "sss"^^ddd )>>. entails bbb ccc <<( xxx aaa _:nnn )>>....?

[doerthe]

The latter was indeed the point. I now think, it should be possible to find a nice wording for replacing part of a triple term by a blank node. But I am still interested in finding a more elegant solution.

[franconi]

The following is already a true SIMPLE entailment:
bbb ccc <<( xxx aaa "sss"^^ddd )>>. ⊨ bbb ccc <<( xxx aaa _:nnn )>>.
The standard RDF semantic condition says:
For every IRI aaa in D, < x, I(aaa) > is in IEXT(I(rdf:type)) if and only if x is in the value space of I(aaa)
and this RDF entails (in the generalised syntax):
"sss"^^ddd rdf:type ddd .
However we can not write this, so the best approximation is indeed:
bbb ccc <<( xxx aaa "sss"^^ddd )>>. ⊨ bbb ccc <<( xxx aaa _:nnn )>>. _:nnn rdf:type ddd .
There is no "leak", since this is based only on the identity of resources (i.e., transparency), without involving properties; moreover, I didn't use any special triple term stuff here.
The conclusion is that, yes, rdfD1 should have "if the triple structure appears in S".

[franconi]

We need to find a general solution to this, since it involves also rdfs14. There is a still unsatisfactory proposal for rdfs14 in PR #74.

[franconi]

It should be changed exactly like rdfs14:

If the triple appears in S: xxx aaa "sss"^^ddd . (for ddd in D)
then S RDF entails recognizing D:
the graph S with the appearance replaced with xxx aaa _:nnn .
_:nnn rdf:type ddd .

[franconi]

Once the issue w3c/rdf-semantics#86 in Semantics is solved, we can apply the solution to both rdfD1 and rdfs14.