Industry

Stream: general

[Henry Story]

The W3C is starting work on a charter for Linked Data Signatures as per mail to the Credentials Community Group today. There'll be graphs, hypergraphs, URIs and crypto discussions involved, and I mathematical proofs of correctness will play a central role.

This is following up on 14 or more years of ideas. One proposal is RDF Dataset Canonicalization - Formal Proof.

[Kevin Buzzard]

My reading of the Formal Proof document is that this is someone using the phrase "formal proof" the way that a mathematician would use the phrase "proof" and a computer formaliser person would use the phrase "paper proof".

[Henry Story]

Thanks @Kevin Buzzard , I thought that may be the case.
But in their defense, this is not a standard, only a proposal for one, and I guess they are still interested in getting feedback from the community, discovering if others have come up with better methods, etc... You can actually see quite a lively discussion on the mailing list on the RDF Dataset Canonicalization thread.

Btw. DataSets in RDF I believe form hypergraphs, as defined say in David Spivak's Higher-dimensional models of Networks. I think those are generalisations of simplicial sets. From that you can build multi agent modal logics as shown by this beautifuly illustrated Knowledge in Simplicial Complexes (I have an illustrated document that shows how one can get to such a conclusion with simple illustrations :-).
Also a number of links to this here.

I mention that because it is usually thought that RDF Graphs are only directed graphs. That these higher dimensions are needed for the web, which is a multi-agent system spanning the globe, is often lost on people, even logicians, mathematicians and programmers. (But that is fine, since those graphs are part of the larger space).

Also I mention that because someone might thinking of this see some powerful mathematical tool that can be used in this space, and that may have escaped those who thought about it till now. Also of course this may be an interesting and valuable exercise to try to see if one can prove this mechanically. As there are a lot of computer people in those groups, I think they would appreciate such proofs a lot.