RDF semantics you can prove

LeanRDF is a Lean 4 library with a native RDF 1.1 data model and the W3C model theory of RDF and RDFS. Elpi (λProlog) searches for derivations; a verified Lean checker turns them into theorems of the form g.RDFSEntails q.

Read the book Documentation See examples GitHub

Elpi finds, Lean checks

Search is large, fast-changing code; proofs should not depend on it. LeanRDF splits the work: the untrusted side computes the RDFS closure and a proof certificate, the trusted side checks the certificate against rules that are proven sound against the semantics. A wrong search can only produce a rejected certificate, never a wrong answer.

Pipeline: Turtle or N-Triples to Graph, Elpi saturation and certificate (untrusted), verified checker and the theorem g entails q (trusted)

What is in the box

A native RDF model

IRIs, blank nodes, literals that cannot be ill-formed, generalized triples and graphs used through membership lemmas only. No FFI, no dependencies.

N-Triples and Turtle

Native parsers with line and column in every error, a canonical serializer, RFC 3986 IRI resolution. All W3C syntax and evaluation tests pass.

The model theory

Simple, D-, RDF and RDFS interpretations transcribed from RDF 1.1 Semantics, one field per condition, with four entailment relations.

67 rules, all proven sound

Every RDFS 1.1 pattern, GrdfD1, the container rules and the axiomatic triples, as data with guards, each with a soundness proof.

Certificates and a verified checker

Proof DAGs in JSON. check_sound gives Derives; checkQuery_sound gives RDFS entailment. Exports to CertifyingDatalog.

Not vacuous, by proof

A concrete RDFS model and countermodels for non-entailments, checked by the kernel, show the semantics is neither empty nor trivial.

SPARQL 1.1, proven

The algebra, a declarative semantics and an evaluator proven to compute it, with paths, aggregates and subqueries. Passes the W3C query suite.

OWL 2 RL and EL

60 OWL 2 RL rules and 10 EL rules proven sound against the OWL 2 RDF-Based conditions, a model that shows they are consistent, and certified classification.

SHACL Core, both directions

The SHACL Core semantics and a validator proven to report a violation exactly when the data does not conform. Passes all 98 W3C core tests.

Certifying oxilite

oxilite finds and stores, LeanRDF proves: its answers and its OWL closure, checked from its own explanations or from Elpi.

Numbers

313 / 313W3C Turtle tests

70 / 70W3C N-Triples tests

354W3C SPARQL 1.1 query tests

98 / 98W3C SHACL Core tests

137RDFS, OWL 2 RL and EL rules proven sound

0sorry or new axioms

3standard axioms used: propext, Quot.sound, Classical.choice

A first taste

Run the demo on the example pet ontology: is there a person with a pet that is a mammal?

$ cd elpi
$ lake exe leanrdf-demo examples/pets.nt examples/query-mammal-owner.nt
LeanRDF: 11 data triples, 3 query triples
Elpi closure under 67 rules: 201 triples
Query instance: _:owner ↦ <http://example.org/bob>
Query instance: _:pet ↦ <http://example.org/tom>
Certificate: 6 nodes, goals [1, 4, 5]
  ...
  [4] <…/bob> rdf:type <…/Person>  (rdfs2 [2, 1])
  [5] <…/tom> rdf:type <…/Mammal>  (rdfs9 [0, 3])
Verdict: ENTAILED. The certificate was accepted by the verified checker (compiled).

And in Lean, the same pipeline ends in a theorem:

theorem g_entails_q : g.RDFSEntails q :=
  checkQueryB_sound (c := cert) (by native_decide)