LeanRDF

RDF semantics in Lean 4: a short book

From triples to model theory to certified entailment, with LeanRDF as the running example. Read it in order: each chapter builds on the previous one.

  1. Why RDF semantics in Lean
    What "entails" means for RDF, why reasoners disagree, and how LeanRDF makes each answer a theorem.
  2. RDF graphs in Lean
    Terms, literals that cannot be ill-formed, generalized triples, and graphs used through membership.
  3. Reading and writing RDF
    Native N-Triples and Turtle parsers, canonical output, IRI resolution and the W3C test suites.
  4. What a graph means
    Interpretations, satisfaction, existential blank nodes and entailment — the model theory of RDF, in Lean.
  5. RDF and RDFS interpretations
    Datatypes, the RDF and RDFS condition tables transcribed one field per row, and the core the proofs use.
  6. Rules, derivations and soundness
    RDFS entailment patterns as data, the Derives relation, and the proof that every derivation is an entailment.
  7. Is the semantics empty?
    Why soundness alone proves nothing if the conditions are contradictory, and the kernel-checked models that rule it out.
  8. Elpi finds
    Rules compiled to λProlog clauses, semi-naive forward chaining that terminates on cycles, and the closure read back into Lean.
  9. Lean checks
    Proof DAG certificates, the verified checker, and how an accepted certificate becomes the theorem g.RDFSEntails q.
  10. Adding a rule of your own
    The whole workflow on one new rule: write it as data, prove it sound, let Elpi saturate with it, and get an entailment theorem from the certificate.
  11. Certifying a database
    oxilite finds and stores, LeanRDF proves. Certifying the answers and the materialized closure of a real triple store, from its own explanations or from Elpi.
  12. SPARQL, specified and proven
    The SPARQL 1.1 algebra in Lean, a declarative semantics, and an evaluator proven to compute it.
  13. OWL 2 RL, sound rule by rule
    The OWL 2 RDF-Based conditions the OWL 2 RL rules need, 49 rules proven sound, a model that shows the conditions are consistent, oxilite's OWL closure certified, and certified OWL 2 EL classification.
  14. SHACL, proven in both directions
    The SHACL Core semantics in Lean, and a validator proven to report a violation exactly when the data does not conform.
  15. What is proven, what is trusted
    The exact guarantee of each package, the trusted base, the recorded simplifications, and what remains open.