RDF graph data model semantics in Lean

Stream: new members

[Andrew Berezovskyi]

Hello dear Lean community,

It's a pleasure to join you. My name is Andrew, my main interest lies in communication protocols and ontologies for integration of systems (thus, it should be clear that I am not a mathematician). I am starting to use Lean and my current idea is to use Lean to prove a number of invariants on protocols and ontologies in a certain area that relies on RDF, a graph data model that was developed as part of the semantic web research.

I would like to ask if anyone has modeled the semantics of RDF (https://www.w3.org/TR/rdf11-mt/) and/or Description Logic in Lean? I am interested in it for three reasons: a reusable building block will help me get started faster, might help me develop my definitions in a way that could later be reused, and because RDF model is a bit peculiar. In particular, an RDF resource may be an instance of multiple classes, which means (as far as I understand) that RDF type model would have to be formalized in Lean without primary reliance on Lean type system. I would be very thankful for any useful pointers.

Again, my pleasure to join the community and looking forward to stimulating discussions and helping each other (though I am likely going to be on the receiving side for a while, thus thank you in advance for your patience)!

Best regards,
Andrew