Lean 4 KnowledgeLean 4 Knowledge · 5 min read
A diagram of the semantic web can look like a ladder: triples at the bottom, ontologies above, logic near the top. For an implementation, it is more useful to ask what each layer promises. Parsing, query evaluation, entailment, and validation are different operations. A certificate must say which operation it justifies.
1. Represent statements without losing their meaning
RDF describes graphs using subjects, predicates, and objects, with IRIs, literals, and blank nodes. Blank nodes are not merely convenient global identifiers; their interpretation matters when comparing graphs and checking entailment. RDF 1.1 Semantics specifies interpretations and several entailment regimes, providing the mathematical target for a formalisation.
LeanRDF brings a native RDF model, N-Triples and Turtle parsing, and formal interpretations into Lean. The relevant question becomes precise: does every interpretation satisfying this graph also satisfy the query graph, under the selected regime?
2. Derive consequences with RDFS
Suppose a graph states that cats are mammals and that Tom is a cat. RDFS supplies the semantic connection that licenses Tom's membership in the mammal class. A derived triple should be traceable to its premises and the rule used. LeanRDF represents certificates as proof graphs, checks their steps, and connects successful checking to entailment through soundness theorems.
Elpi can perform the exploratory work of finding a derivation. The certificate checker does not need to trust that search procedure. Remember the converse: a failed search is not, by itself, a semantic proof of non-entailment.
3. Query, infer, and validate deliberately
SPARQL evaluates queries over data. LeanRDF includes a formal query algebra and an evaluator with a correctness relationship to its declarative semantics. This concerns query evaluation; it should not be described as an automatic proof that the original data is true.
OWL adds ontology vocabulary and richer entailments. The project develops rule reasoning for OWL 2 RL and EL. Name those supported profiles and rules explicitly: that is a narrower, more useful statement than claiming a universal OWL reasoner.
SHACL asks whether a data graph conforms to specified shapes. A requirement such as “every selected person has a name” belongs naturally to validation. It does not have the same meaning as an open-world ontology axiom. The SHACL specification defines this data-graph/shapes-graph relationship. LeanRDF develops SHACL Core semantics and a validator connected to them by proofs.
4. Keep the proof boundary visible
A sound checker theorem, an execution of compiled code, and a kernel-checked proof term are related but distinct artifacts. An executable verdict relies on its runtime path. If a theorem uses native evaluation, inspect the resulting assumptions and evaluation mechanism rather than presenting it as ordinary kernel reduction. The project examples document the available routes.
For a deployed agent, retain the input graph, entailment regime, query, certificate, and relevant software versions. That makes the claim reproducible and lets a later checker revisit it. Explore the LeanRDF book, documentation, and worked examples, and inspect the source definitions and soundness theorems when deciding exactly what your application can promise.