Entailment Algorithm in Semantics Appendix is incomplete

[Antoine-Zimmermann]

There are several kinds of valid entailments that the algorithm cannot prove. One such kind is covered by @pfps's pull request #45 but there are the two following cases:

1. the empty graph (in fact, any graph) RDFS-entails ex:a rdf:type rdfs:Resource (in general, any graph S RDFS-entails any triple of the form aaa rdf:type rdfs:Resource for aaa an arbitrary IRI).
2. the graph S = {:bn rdf:type xsd:string . :bn rdf:type rdf:langString .} RDFS:entails every RDF graphs because S is inconsistent.

Note that these are only related to RDF 1.1 semantics. For RDF 1.2, additional rules for directional text and for quoted triples/triple terms/graph terms will be needed.

[pfps]

The second is covered by the condition "If S is RDF (RDFS) consistent" in the proposition.

The first was covered by rules rdfs4a and rdfs4b, but these need to be generalized, as does rule rdfs1. Then the completion process needs to be modified to restrict the application of the generalized rule rdfs4. The reason for this change is the change that all IRIs now have denotations.

The generalized rules are more like axioms, but leaving them as rules is the lesser change.

[Antoine-Zimmermann]

The rules don't need changes. My proposal would be: update the first enumerated list that appears in Appendix A by adding the following after step 2.:

3. For every IRI aaa used in E, add aaa rdf:type rdfs:Resource to S

and update the second enumerated list of the appendix by adding this after step 3.:

4. For every IRI or literal aaa used in E, add aaa rdf:type rdfs:Resource to S

Then the completeness result in the orange box should be correct. This could be generalised to cover inconsistent graphs by adding a step to the procedure. Before checking that the resulting graph contains an instance of E, it can be checked that the resulting graph contains an instance of {_:bn rdf:type xsd:string . _:bn rdf:type rdf:langString .} I believe, yet I haven't proved, that this is the only possibility for inconsistency in RDFS entailment recognising {xsd:string, rdf:langString}.

[Antoine-Zimmermann]

Last step of the algorithm could become:

If {_:bn rdf:type xsd:string . _:bn rdf:type rdf:langString .} is in the resulting graph, or if the resulting graph contains an instance of E, then S RDFS-entails E.

[doerthe]

4. For every IRI or literal aaa used in E, add aaa rdf:type rdfs:Resource to S

Is this correct? You actually add a blank node for the literal, right?

[Antoine-Zimmermann]

@doerthe What are you referring to when you say "this" in the question "Is this correct?"?

[doerthe]

@doerthe What are you referring to when you say "this" in the question "Is this correct?"?

@Antoine-Zimmermann: I maybe did not read enough in detail, but I read the part I cited as:

For every IRI or literal aaa used in E, add aaa rdf:type rdfs:Resource to S.

So, let aaa="test", then this says that I have to add the triple

"test" rdf:type rdfs:Resource.

But this is not a valid triple, therefore my question.

[Antoine-Zimmermann]

OK. I'm referring to a section of the appendix where it is said that we apply rules and materialise inferrences in generalized RDF where blank nodes and literals can be used anywhere. See the text after the first table in Appendix A of RDF Semantics.

[doerthe]

OK, that was the missing piece, I should have read more carefully. Thank you for the clarification.

[doerthe]

Do we the also need to add rdfs:Resource rdf:type rdfs:Resource. as axiomatic triple?

[pfps]

Do we the also need to add rdfs:Resource rdf:type rdfs:Resource. as axiomatic triple?

The replacement for rdfs4a and b does this.

[doerthe]

sorry again, that I was lost here, but I think I now understood: if the fact rdfs:Resource rdf:type rdfs:Resource. is relevant for E, then the iri rdfs:Resource already occurs in E. In that case the rule produces the triple, otherwise it won't, but that is not a problem either. Thank you for your patience explaining me the rules :)

[pfps]

Is there anything else that needs to be done here? I'm making this issue to be closed but if anyone thinks there is more to do, please speak up.

[Antoine-Zimmermann]

@pfps in my message with a suggestion, there is something that can be done to resolve the issue. Should I make a pull request myself with these changes or would you do it?

[pfps]

@Antoine-Zimmermann Please go ahead and create a PR.

[pfps]

As there has been no PR produced and the appendix is correct as it, I'm again proposing to close this issue.

[Antoine-Zimmermann]

@pfps I finally took the time to create a PR with the modifications I suggested above. It is PR #48.

[pfps]

This issue is closed with the merging of PR #48