Fixes correctness of Appendix A (from issue #139) #160

franconi · 2025-10-02T13:32:03Z

Closes #139

w3cbot · 2025-10-02T17:00:02Z

This was discussed during the #rdf-star meeting on 02 October 2025.

View the transcript

Pull Request 160 Fixes correctness of Appendix A (from issue #139) (by franconi) [ms:CR]

enrico: this is similar to 139 that was discussed before

pfps: I'm worried that some members of the WG are asking for fundamental changes to the semantics
… there was something again on changing things related to asserted triples, but we need to close the discussion now

pchampin: the issue was closed, so what is still coming back?

<niklasl> It's w3c/rdf-concepts#220

<gb> CLOSED Pull Request 220 Annotations on asserted triples are based on operational semantics (by rat10) [ms:CR]

pfps: this is saying that there is something lacking in Semantics, but are we done now with it, or should we still do something about it

ktk: we said in previous meeting that the discussion should be closed

lisp: I made a respond but I did not reopened the issue

ktk: any other things on Semantics or Concepts?

<ktk> https://github.com/orgs/w3c/projects/20/views/11

ktk: there are a number of issues with "propose closing"

doerthe

We have a problem with Grdfs14. The rule cannot be applied to exhaustion. The process will not end.

We need to make that rule dependent on the triples occurring in E.

franconi · 2025-10-07T09:48:10Z

We have a problem with Grdfs14. The rule cannot be applied to exhaustion. The process will not end.

We need to make that rule dependent on the triples occurring in E.

Which is why I am proposing that IT is partial. Then Grdfs14 is terminating and complete if applied just to existing triple terms in the graph.
Something like:
if the triple term <<xxx yyy xxx>> appears in S then S RDFS entails <<(xxx yyy zzz)>> rdf:type rdfs:Proposition .

pfps · 2025-10-07T19:24:51Z

I don't see any problem with having an infinite completion.

doerthe · 2025-10-08T08:55:08Z

I don't see any problem with having an infinite completion.

For this appendix it is a problem because it describes a procedure to determine whether a graph S entails a graph E by applying the rules. In this case, the procedure should terminate, but that is not too difficult to get: we could say that we only construct the triple
<<(xxx yyy zzz)>> rdf:type rdfs:Proposition .
if <<(xxx yyy zzz)>> appears in E or something similar. Then we keep the procedure. We already do something similar with the literals.

doerthe · 2025-10-08T09:03:52Z

We have a problem with Grdfs14. The rule cannot be applied to exhaustion. The process will not end.
We need to make that rule dependent on the triples occurring in E.

Which is why I am proposing that IT is partial. Then Grdfs14 is terminating and complete if applied just to existing triple terms in the graph. Something like: if the triple term <<xxx yyy xxx>> appears in S then S RDFS entails <<(xxx yyy zzz)>> rdf:type rdfs:Proposition .

It should depend on E, then we can also do that without making IT partial.

The more I think about it, the more I am convinced that making IT injective overcomplicates things. But we had that discussion and I accepted it (while I still dislike it). But as mentioned in the other issue: proofs like the one for "Every graph is simply satisfiable." become more complicated while we do not gain anything from the injectivity. It could also be added as a condition when it is actually needed. I would prefer to keep simple entailment simple.
But: if we keep everything as is, we also need to look at ALL the proofs now.

pfps · 2025-10-08T14:48:11Z

There are a few problems with Appendix A. In my view they all boil down to the attempt to keep the rules from entailing an infinite number of consequences. But if you do this, then you have to be careful about completeness.

The RDF 1.1 Semantics document has a problem with this. The application of rule GrdfD1 has to change to include not just literals in S but also literals in E. Otherwise the empty graph does not entail
"2"^^xsd:integer rdf:type xsd:integer.

If the rules are to remain as they are, then Appendix A has to loosen them to include the contents of E in several places.

Rules that are impacted: rdfD1, rdfs1, rdfs4.
rdfs14 is also impacted, but needs to be fixed in a different way. This rule is more tricky because predicates in triples have to be properties.

Split rdfs14 into two rules, rdfs14 for the first conclusion and rdfs15 for the second

Define

RDFS-T entailment pattern from S towards E
Grdfs14
If S contains yyy rdf:type rdf:Property .
and xxx andy zzz appear in E
then S RDFS entails
<<(xxx yyy zzz)>> rdf:type rdfs:Proposition .

This leads to:

Add to S all the RDF (and RDFS) axiomatic triples which do not contain any container membership property IRI.
For rdf:_1 and each container membership property IRI which occurs in E, add the RDF (and RDFS) axiomatic triples which contain that IRI.
Apply the rule GrdfD1 (and rdfs1 and rdfs4) but using E instead of S in the antecedent.
Apply the rules GrdfD1, rdfD1a, and rdfD2
(and the rules rdfs1 through rdfs13 and Grdfs14), with D={rdf:langString, rdf:dirLangString, xsd:string},
to the set in all possible ways, to exhaustion.

This is a tiny but sloppy because it should mention E in the fourth step.

doerthe · 2025-10-09T12:06:35Z

Thank you for the analysis. I did not read RDF Semantics 1.1 carefully enough and was not aware of the fact that the entailment was already problematic there.

Your adaption looks good.

franconi · 2025-10-09T14:06:26Z

@pfps is fixing this PR according to his comment above.

pfps · 2025-10-09T14:22:03Z

I have a PR against your repository. I think you need to merge that.

franconi · 2025-10-09T14:28:08Z

I have a PR against your repository. I think you need to merge that.

I don't see any PR in my repo https://github.com/franconi/rdf-semantics-fork-enrico/pulls

fix problems in entailment closure

franconi · 2025-10-09T16:48:14Z

The modifications by @pfps have been incorporated in this PR.
@pfps and @doerthe please make a final check, so we can merge.

pfps

OK with the change

pfps · 2025-10-09T18:02:08Z

spec/index.html

+    In practice there is little utility in re-deriving these
    and a subset of the rules can be used to establish most entailments of practical interest.</p>

  <p>If it is important to stay within legal RDF syntax, rule <a>rdfD1</a> may be used instead of <a>GrdfD1</a>,


Suggested change

<p>If it is important to stay within legal RDF syntax, rule <a>rdfD1</a> may be used instead of <a>GrdfD1</a>,

<p>If it is important to stay within legal RDF syntax, rule <a>rdfD1</a> may be used instead of <a>GrdfD1</a> and <a>rdfs14</a> instead of <a>Grdfs14</a>,

Fixes correctness of Appendix A (from issue w3c#139)

92f2a8d

franconi requested review from doerthe and pfps October 2, 2025 13:32

franconi added the ms:CR Milestone: Candidate Recommendation label Oct 2, 2025

doerthe reviewed Oct 7, 2025

View reviewed changes

fix problems in entailment closure

09f18ce

franconi mentioned this pull request Oct 9, 2025

check correctness of Appendix A #139

Open

Merge pull request #1 from franconi/peter

5340b59

fix problems in entailment closure

pfps reviewed Oct 9, 2025

View reviewed changes

	<p>If it is important to stay within legal RDF syntax, rule <a>rdfD1</a> may be used instead of <a>GrdfD1</a>,
	<p>If it is important to stay within legal RDF syntax, rule <a>rdfD1</a> may be used instead of <a>GrdfD1</a> and <a>rdfs14</a> instead of <a>Grdfs14</a>,

Fixes correctness of Appendix A (from issue #139) #160

Are you sure you want to change the base?

Fixes correctness of Appendix A (from issue #139) #160

Uh oh!

Conversation

franconi commented Oct 2, 2025 • edited by pr-preview bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

w3cbot commented Oct 2, 2025

Pull Request 160 Fixes correctness of Appendix A (from issue #139) (by franconi) [ms:CR]

Uh oh!

doerthe left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

franconi commented Oct 7, 2025

Uh oh!

pfps commented Oct 7, 2025

Uh oh!

doerthe commented Oct 8, 2025

Uh oh!

doerthe commented Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pfps commented Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

doerthe commented Oct 9, 2025

Uh oh!

franconi commented Oct 9, 2025

Uh oh!

pfps commented Oct 9, 2025

Uh oh!

franconi commented Oct 9, 2025

Uh oh!

franconi commented Oct 9, 2025

Uh oh!

pfps left a comment

Choose a reason for hiding this comment

Uh oh!

pfps Oct 9, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

franconi commented Oct 2, 2025 •

edited by pr-preview bot

Loading

doerthe left a comment •

edited

Loading

doerthe commented Oct 8, 2025 •

edited

Loading

pfps commented Oct 8, 2025 •

edited

Loading