Every earlier post showed the engine passing tests: 1662 W3C conformance tests, 0 failures. Tests certify behaviour on the inputs somebody thought to write down. This post shows something stronger, landed across 2026-08-05/07: for a precisely-stated fragment of RDFS, the engine's query answers are theorems — machine-checked equivalent to model-theoretic entailment, on every input in the fragment, including the ones nobody thought to write down.
The chain, each link an F* theorem about the shipping code:
model theory ⟷ entailment ⟷ closure ⟷ termination test ⟷ index ⟷ BGP matching ⟷ query answers
The fragment is corerdfs: rdf:type, rdfs:subClassOf,
rdfs:subPropertyOf, rdfs:domain, rdfs:range — the working core
of RDFS schema reasoning. That is this project's API name for the
fragment the literature calls ρdf ("rho-df" in our code and
theorem names), introduced by Muñoz, Pérez & Gutierrez in
Simple and Efficient Minimal RDFS
(J. Web Semantics 7(3), 2009), who proved it captures exactly the
inferential core of RDFS once the self-referential and infinite rows
are set aside. Everything below runs live in your browser against the
same extracted engine the theorems are about.
fn.coreRdfsClosure(data) takes an RDF document (Turtle or
N-Triples text) and returns {ok, ntriples, rounds}: the same graph
with every fact the five schema properties imply added as an
explicit triple. That is all "closure" means. If your data says
:Engineer rdfs:subClassOf :Employee and :ada rdf:type :Engineer,
the output also contains :ada rdf:type :Employee — and every other
consequence, chained to any depth (rounds reports how many passes
that took). You run it once, store or query the result, and from then
on plain SPARQL — no reasoner, no entailment setting — sees every
schema-implied fact, because the facts are physically there.
fn.coreRdfsCheck(data) answers one question before you
rely on that: does the proved guarantee apply to this data? It
returns {ok, fragment}. fragment: true means every triple in the
document is inside the shape the theorems quantify over, so the
closure's answers carry the machine-checked soundness and
completeness guarantee — nothing false added, nothing implied
missed. fragment: false means the data steps outside that shape
(for example a literal where the theorems require an IRI); the
closure still runs and is still sound, but the completeness theorem
no longer vouches for it.
Together they replace "trust the vendor's reasoner settings" with a two-call contract: check whether the guarantee applies, then materialise the consequences — with both steps' behaviour stated and proved in the theorem registry.
An ordinary org-chart ontology. Note one thing: object positions hold IRIs, not literals — that is a real boundary of the proved fragment, and the checker below will tell you so rather than leaving you to find out.
PREFIX : <http://example.org/org#>
:Engineer rdfs:subClassOf :Employee .
:Employee rdfs:subClassOf :Agent .
:manages rdfs:domain :Manager .
:manages rdfs:subPropertyOf :worksWith .
:Manager rdfs:subClassOf :Employee .
:ada a :Engineer .
:grace :manages :ada .
ttl = `
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
PREFIX : <http://example.org/org#>
:Engineer rdfs:subClassOf :Employee .
:Employee rdfs:subClassOf :Agent .
:manages rdfs:domain :Manager .
:manages rdfs:subPropertyOf :worksWith .
:Manager rdfs:subClassOf :Employee .
:ada rdf:type :Engineer .
:grace :manages :ada .
`
Step 1 — ask whether the guarantee applies. The fragment predicate is a decidable check, extracted from the same F* definition the theorems quantify over. This is the difference between fine print and an API: you can ask before trusting an answer.
return pretty(await fn.coreRdfsCheck(ttl));
// {ok: true, fragment: true} — the certified path applies to this data
Step 2 — run the certified closure. Six rules, not the engine's full twelve: exactly the six the rho-df theorems cover (rdfs2/3/5/7/9/11). The stopping test is the ordinary length-equality check — which is itself proved to be a faithful proxy for semantic saturation on freshly-parsed data, not a heuristic.
closed = fn.coreRdfsClosure(ttl) // a promise: dependent cells receive it awaited
Step 3 — query it. Is Ada an :Agent? No triple says so; two
subclass steps entail it.
const dataset = await fn.parse(closed.ntriples, {format: "ntriples"});
const rows = await fn.query(dataset, `
# Does the closure make Ada an Agent, via two chained subclass steps?
PREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>
PREFIX : <http://example.org/org#>
ASK { :ada rdf:type :Agent }
`);
return pretty(rows); // true — and that "true" is the theorem below
Step 4 — say more, get more (RDFS-Plus). Ask the closure who
works with whom, and it answers one row: grace → ada (derived by
rdfs7 from manages ⊑ worksWith). But working-with is naturally
mutual, and RDFS cannot even say that. One OWL triple can —
:worksWith rdf:type owl:SymmetricProperty — and the RDFS-Plus
tier (RDFS plus the practical OWL subset: sameAs, inverseOf,
symmetric/transitive/functional/inverse-functional properties,
class/property equivalence — "RDFS-Plus" in Allemang & Hendler's
Semantic Web for the Working Ontologist, "RDFS++" in AllegroGraph)
acts on it:
const withSym = ttl + `\n :worksWith rdf:type <http://www.w3.org/2002/07/owl#SymmetricProperty> .\n`;
const plus = await fn.rdfsPlusClosure(withSym);
const dataset2 = await fn.parse(plus.ntriples, {format: "ntriples"});
const rows = await fn.query(dataset2, `
# Who works with whom, now that the symmetric property makes it mutual?
PREFIX : <http://example.org/org#>
SELECT * WHERE { ?x :worksWith ?y } ORDER BY ?x
`);
return pretty(rows); // TWO rows now: grace→ada and ada→grace
The warrant changes with the vocabulary, and the page says so
plainly: every rule rdfsPlusClosure runs carries a proved
licensing and truth-preservation lemma (the symmetric step here is
row prp-symp, prp_symp_licensed, in the
registry) — nothing invented, every
derivation certified rule-by-rule. What this tier does not carry is
corerdfs's chain-level completeness: owl:sameAs is equality, and
the Herbrand construction behind the completeness theorem does not
survive it. Three regimes, three precisely-stated warrants — corerdfs
(sound and complete), RDFS-Plus (every step certified), OWL RL
(the full engine, 1662 W3C tests) — each labelled with exactly what
is proved.
What makes this true different: the landed theorem
theorem_rdfs_regime_bgp_exact_answer (with its ASK corollaries,
stated on the literal eval_ask_query entry point) says the answers
computed this way are exactly the rho-df-entailed consequences —
sound and complete, an if-and-only-if. Not "we tested it a lot":
checked by z3 for every graph in the fragment, under hypotheses that
are themselves decidable checks or theorems (the fragment check you
ran in step 1; saturation-class facts proved for freshly-parsed
data). The full chain, theorem by theorem, lives in the
theorem registry.
The strongest evidence a proof system is doing work is not the theorems it proves — it is the claims it rejects. Three from this program, each caught before it could mislead anyone:
The goal statement itself was false. We first asked for:
"rdfs_closure g computes exactly the RDFS-entailed fragment
triples." F* produced counterexamples, now machine-checked theorems:
[X subClassOf Y] RDFS-entails [X subClassOf X] (reflexivity is
semantically forced), yet no closure rule derives it — and
cond_resource entails [Z rdf:type rdfs:Resource] for every IRI
Z, including ones absent from the graph, which no finite closure can
enumerate. The honest theorem quantifies over the six rho-df semantic
conditions instead — the same reduction the published rho-df
literature makes, rediscovered here by refutation.
Fragment preservation is false. It is natural to assume a fragment graph stays in the fragment after closure. It does not:
const escape = `
PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>
PREFIX : <http://example.org/x#>
:P rdfs:subPropertyOf rdfs:subPropertyOf .
:a :P _:b1 .
`;
const before = await fn.coreRdfsCheck(escape);
const closedEsc = await fn.coreRdfsClosure(escape);
const after = await fn.coreRdfsCheck(closedEsc.ntriples);
return pretty({fragmentBefore: before.fragment, fragmentAfter: after.fragment});
// true, then false — one rdfs7 step derives ':a rdfs:subPropertyOf _:b1',
// whose blank-node object leaves the fragment. Machine-checked as
// rho_df_frag_preservation_fails; the theorems state their hypotheses
// on the closure RESULT because of exactly this graph.
"The solution list contains μ" is false. The evaluator emits bindings in a planner-determined order, so the intuitive completeness statement — a caller-constructed solution appears in the result list — is refutable with two triple patterns. The true statement is at the answer level: the engine returns a solution instantiating to the same triples. Nothing downstream inspects binding order, so nothing weaker was proved — but a subtly false statement was kept out of the registry.
Analysts / users. Within the fragment, "no missed inferences" is
now a theorem, not a vendor claim. A false ASK answer means the
fact is genuinely not entailed — completeness is the half tests can
never give you, because a test suite only checks the entailments its
authors enumerated. And the fragment checker means you always know
which regime you are in.
Developers. Two new API calls (fn.coreRdfsCheck,
fn.coreRdfsClosure) plus a contract that is unusual in this space: the
registry names every theorem, every
hypothesis, and every boundary, in one table. The planner lemma
(lemma_choose_best_tp_cover) is a developer guarantee too: query
reordering is proved answer-preserving, so optimizer changes cannot
silently alter results on this path.
Auditors / standards people. The claims language is calibrated — "proved sound and complete with respect to an independent F* formalisation of the rho-df conditions, under stated hypotheses" — and the trust surface (three string-ordering axioms, the extraction step, the assume-val realisations) is enumerated in the same registry. The refutation section above is reproducible: the counterexamples are theorems in the tree you can re-check.
Yes — in three ways, one of which you can time right now.
Fewer rules, same answers, with a warrant. For fragment data, the six-rule closure provably yields the same fragment query answers as running more machinery — so the cheaper path needs no safety margin. The cell below builds a subclass chain, runs both the certified six-rule closure and the engine's full twelve-rule RDFS closure, times them in your browser, and checks the fragment answers agree:
// A 60-class subclass chain with typed members: fragment-only data.
let chain = "PREFIX rdfs: <http://www.w3.org/2000/01/rdf-schema#>\nPREFIX rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>\nPREFIX : <http://example.org/c#>\n";
for (let i = 0; i < 60; i++) chain += `:C${i} rdfs:subClassOf :C${i+1} .\n`;
chain += ":x rdf:type :C0 .\n";
const t0 = performance.now();
const six = await fn.coreRdfsClosure(chain);
const t1 = performance.now();
const full = await fn.owlClosure(chain, "RDFS"); // the full twelve-rule RDFS set
const t2 = performance.now();
return pretty({
sixRuleMs: +(t1 - t0).toFixed(1),
fullClosureMs: +(t2 - t1).toFixed(1),
derivedTriples: six.ntriples.split("\n").filter(l => l.trim()).length,
note: "timings are measured in YOUR browser just now — not vendor numbers"
});
The point is not the specific ratio your machine shows; per this project's measurement discipline no static number is printed here at all. The point is the warrant: dropping half the rules is usually a correctness gamble, and here it is a theorem.
A faithful stopping test. The closure stops when an iteration adds nothing. That test is now proved equivalent to semantic saturation (no "one extra round to be safe" needed) — and the same theorems are the safety net for the planned round-count optimization of the closure loop (issue #340): any rewrite that preserves the proved saturation predicate is answer-preserving by composition, so the optimizer can be aggressive where it used to be conservative.
Index-only paths. The index well-formedness and completeness theorems (all six buckets) mean a bucket probe provably serves every matching triple — no defensive fallback scans on the certified path.
Stated here exactly as the theorems state them: the fragment excludes
literals and RDF 1.2 triple terms in object position (a consequence of
RDF's own syntax forbidding literal subjects — the REC's lg/gl
surrogate rules are a future milestone, not a patch we skipped), and
rdfs:subClassOf reasoning covers IRI-named classes (blank-node
classes are a recorded engine narrowing). Reflexivity rows
(rdfs6/rdfs10) are outside rho-df by definition. Data can
contain literals freely — labels and values simply ride along
outside the entailment claim. Every boundary traces to a named
finding in the registry, most of them
machine-checked counterexamples rather than prose caveats.
Everything above ran against the extracted engine certified at
commit 17eb2df: combined 1662 pass, 0 fail (out of 1662) on the
W3C suites, hub cells 253 pass, 0 fail (out of 253 — 262 after
this post's own 9 pins landed).