Skip to content

lean-certificates.md

Latest commit

 

History

History
962 lines (804 loc) · 63 KB

lean-certificates.md

File metadata and controls

962 lines (804 loc) · 63 KB
Raw

Derivation certificates and the Lean checker

Every inference the forward-chaining reasoner makes can be written out with the rule that produced it and the premises the rule read, and a checker in lean/ verifies that record against a formal semantics. The checker's soundness is a machine-checked theorem, so a certificate it accepts contains only triples entailed by the asserted graph, whatever the Rust engine did to find them.

This page is the how-to. The design and its limits are in decision 0002.

Produce a certificate

# CLI: any of rdfs, owl-rl, owl-rl-ext. The tableaux path (owl-dl) refuses the flag.
open-ontologies load ontology.ttl
open-ontologies reason --profile owl-rl-ext --certificate /tmp/cert

# Batch, when the store is in-memory per process:
printf 'load ontology.ttl\nreason --profile owl-rl-ext --certificate /tmp/cert\n' \
  | open-ontologies --no-connect --data-dir /tmp/store batch -

Over MCP, onto_reason takes certificate_dir. The response gains a certificate object:

{
  "inferred_count": 268,
  "certificate": {
    "dir": "/tmp/cert",
    "format": "oo-cert/1",
    "asserted": 1128,
    "derivations": 268,
    "by_rule": {"rdfs2": 41, "rdfs9": 190, "scm-eqc1": 3, "...": "..."},
    "check_with": "cd lean && lake exe oo-cert <dir>/asserted.tsv <dir>/derivations.tsv",
    "scope": {"selector": "whole-store", "default_graph": true, "complete": true, "...": "..."},
    "scope_file": "/tmp/cert/scope.tsv"
  }
}

derivations always equals inferred_count: one line per inferred triple, recorded the first time it is derived.

scope says which graphs the run READ, and scope.tsv carries the same thing as a file beside asserted.tsv. It exists because the checker cannot ask: oo-cert verifies that the derivations follow from the triples in front of it, which stays true whatever selected them, so a certificate over one snapshot of a bi-temporal register and a certificate over the union of every version are indistinguishable as files and only one is about a state that existed (#108). Over a store that uses the temporal vocabulary, onto_reason takes valid_at / as_of / all_versions and REFUSES a run that names none of them.

Check it

The checker needs a Lean 4 toolchain. elan installs the version lean/lean-toolchain pins; nothing else is downloaded, the project has no dependencies.

cd lean
lake build                      # builds the checker AND checks the proofs
lake exe oo-cert /tmp/cert/asserted.tsv /tmp/cert/derivations.tsv

Exit codes: 0 every step checks; 1 a step was rejected, and the JSON on stdout names the first one with its rule, conclusion and premises; 2 a file could not be read or parsed.

{"ok":true,"asserted":1128,"derivations":268,"theorem":"OOCert.certificate_sound"}

The files

Tab-separated. Terms are in N-Triples spelling, exactly as the engine's interner holds them, so a term is spelled identically wherever it appears and tabs and newlines cannot occur inside one.

  • asserted.tsv: one triple per line, s TAB p TAB o. Every triple the run started from — which means every triple in the graphs the run SELECTED, and scope.tsv is where that is written down.
  • scope.tsv: oo-scope/1, then one key TAB value line per fact about the selection, with one graph line per named graph read (graph TAB * for the whole store) and one excluded TAB graph TAB reason line per graph deliberately not read. No checker reads this file. It is there because none of them can: a certificate over a snapshot and a certificate over the union of every version are indistinguishable as asserted.tsv + derivations.tsv, and only one of them is about a state that existed (#108).
  • derivations.tsv: one step per line, rule TAB s TAB p TAB o for the conclusion, then the premises as further triples, in the order documented per rule in lean/OOCert/Rules.lean.
  • refutation.tsv, only when the run found a contradiction it can certify: the line oo-refute/1, then the derivation steps that reached the clash in the same spelling as derivations.tsv, then one refute TAB rule line with the clash rule's premises. See the refutation section below.

Carrying a certificate inside a pack

onto_pack writes a graph, a sha256 over it, and the lint and enforce results recorded at pack time. That evidence is what the SENDER'S engine said. Pass certificate_dir and the pack also carries the certificate for the run that produced the graph, and onto_unpack writes those files out and runs THIS machine's checker over them. The receiver then learns whether the derivations hold without trusting the engine that wrote the pack. See decision 0017.

Which files travel. Only the names a run of this engine writes: asserted.tsv, asserted.sha256, derivations.tsv, horn.tsv, rules.tsv, scope.tsv and refutation.tsv. The list is a whitelist in both directions. At pack time it stops whatever an earlier run left in the directory going under the digest; at unpack time the names come from the sender, and a pack naming ../../.ssh/authorized_keys would otherwise be written wherever the receiver's scratch directory resolves that to. The files travel as TEXT, not base64, so a pack stays diffable for the same reason the graph is sorted.

Which checker reads it is decided by the files present and never by the pack's format string: derivations.tsv means oo-cert, horn.tsv plus rules.tsv means oo-horn check. Reading the sender's string would let the sender choose the receiver's checker. A directory holding both is refused, because the two earn different verdicts.

What content_sha256 covers. sha256 still covers the graph text and nothing else. content_sha256 covers the tag oo-pack-content/1\n, the length and bytes of the graph, a presence byte for the certificate and, when one is present, the length-prefixed format, the length-prefixed profile_claimed_by_sender, the asserted and derivations counts, the number of files, then every (name, body) pair in BTreeMap order with both halves length-prefixed. Everything is length-prefixed so two different (graph, certificate) pairs cannot frame to the same bytes at a seam. A pack that carries a certificate and no content_sha256 is REFUSED rather than checked: without that rule, stripping the field and pasting in a certificate sound over another graph passes the old, weaker verification.

The seven verdicts, and none collapses into another.

verdict what happened loads?
certificate_accepted oo-cert accepted it under OOCert.certificate_sound yes
certificate_accepted_under_supplied_rules oo-horn accepted it over a table the SENDER supplied yes
certificate_refused the checker named a step it would not accept no
certificate_unreadable exit 2, an unknown file name, or files that form no certificate no
certificate_not_about_this_pack the checker accepted it and its premises are not all in the graph no
checker_absent_nothing_was_checked no checker here, or the caller turned the check off yes
no_certificate_in_pack the pack carries no proof, which every pack written before this does yes

certificate_not_about_this_pack is the gate the checker cannot be. oo-cert verifies the steps against the triples inside asserted.tsv and has no way to ask where they came from, so a certificate that is internally sound over somebody else's premises checks green. onto_unpack compares the certificate's asserted.tsv against the packed graph in the one spelling both sides use, reason::asserted_bytes, and refuses the load when the proof rests on assertions the pack does not contain. onto_pack refuses the same thing at pack time, so the sender learns rather than the auditor, and the receiver-side refusal stays either way.

What an acceptance does not settle. A certificate proves the materialised triples follow from the asserted ones under the rules that RAN. It proves nothing about whether the asserted triples are true, and it is silent about axioms outside the fragment: an axiom no rule fires on contributed nothing and is invisible here. Run onto_dlp_boundary over the loaded graph to see which of its axioms the rule table can read. Those sentences are in the receiver's report, under does_not_mean, because a limit stated only in documentation is a limit the person reading the verdict does not see.

Two limits that are named rather than closed. The receiver's checker is still a binary somebody chose: $OO_CERT pointing at a script that exits zero and prints the right theorem name earns the accepted word. That is now the receiver's own foot rather than the sender's, which is an improvement and not a closure; the report prints the checker block the binary says about itself so a reader can match its SHA-256 against a release's SHASUMS.txt. And the pack is built in memory with no streaming path. Measured on 28 September 2026: benchmark/reference/ies4.ttl, 3,976 asserted triples reasoned under owl-rl-ext with materialisation, packs to 4,514,931 bytes of which 3,015,113 are the certificate; benchmark/reference/pizza-reference.owl, 2,332 triples, packs to 1,422,749 bytes with a 843,870-byte certificate. onto_pack reports graph_bytes, the certificate's bytes and pack_json_bytes so the cost is visible.

What the file is NOT enough for

derivations.tsv is a derivation DAG and it is tempting to read explanations out of it. Do not. It records ONE step per inferred triple, the first the fixpoint reached, which is exactly what a checker that re-derives needs and exactly wrong for the question "which of my axioms did this". A triple derived two independent ways has two justifications and the file shows one, so an explanation built from it would be specific, confident and false.

onto_justify and onto_provenance therefore ask the reasoner for every applicable ground rule instance instead, and never open the file. See docs/explanation.md and decision 0009. What the certificate IS enough for, those tools use: with certificate_dir, each justification gets its own certified run over its own triples, so oo-cert can verify that the conclusion really does follow from that subset. Minimality is not in the theorem and is re-run instead.

What is proved

OOCert.certificate_sound in lean/OOCert/Soundness.lean:

if checkCert G steps = true then for every step, G ⊨ step.conclusion

where G ⊨ t is truth in every model of G under the semantics in lean/OOCert/Semantics.lean: the RDF-based reading of the twenty-nine rules' vocabulary, with each semantic condition the if direction of the W3C condition or a consequence of it, never more.

Weaker conditions admit more interpretations, so the result carries outward, and that transfer is now a theorem rather than a claim. lean/OOCert/W3C.lean states the OWL 2 RDF-Based Semantics conditions at full strength, one field per table cell quoted verbatim from the raw HTML of the specification, and OOCert.W3CEntails.of_entails proves that everything Entails gives is true in every W3CModel, which is an interpretation meeting those fields. OOCert.certificate_w3c_sound is certificate_sound restated over that class, with the same certificates and the same checker. It is not the sentence "true in every conforming interpretation", the file says so in its own docstring, and no document here may say otherwise. That sentence is OOCert.certificate_conforming_sound, a layer further out, and the section after next is about it.

Fourteen arms of the soundness proof used to be posited: the theorem that scm-dom1 is sound read a field off Conditions which said that scm-dom1 holds. All fourteen are now derived, and each derivation is a proof term that depends on no axiom at all. The cell that makes them derivable is Table 5.8's connective, which carries rowspan="4" in the source and so states an iff for rdfs:subClassOf, rdfs:subPropertyOf, rdfs:domain and rdfs:range. RDFS alone gives those rows only the if-then direction, and the twelve scm-* arms among the fourteen do not follow from it.

That step used to be an argument rather than a theorem. It is now a theorem, in lean/OOCert/Conforming.lean, and this section records both the result and what it does not cover.

An OWL 2 RDF-Based interpretation is a Lean structure there, OOCert.Interpretation: the parts of RBS Table 5.1, with IR as the carrier type so that Table 5.1's IP ⊆ IR, IC ⊆ IR, ICEXT(x) ⊆ IR and IEXT(x) ⊆ IR × IR hold by typing, plus IS, IL and the blank-node assignment of RDF 1.1 Semantics section 5.1. ICEXT and IC are definitions, per section 9's "ICEXT(y) is defined to be …" and "IC is defined to be ICEXT(I(rdfs:Class))". Truth is section 5's clause with its I(p) is in IP conjunct, and the bridge to Interp is chosen so that Interp.sat and Interpretation.Sat are the same proposition: OOCert.Interpretation.sat_eq is Iff.rfl.

OOCert.Conforming.toW3C then proves the reading that used to be prose, and OOCert.Conforming.toW3CModel carries it to W3CModel, which includes proving that every Chain G list is a semantic sequence in the specification's sense whenever G is satisfied (OOCert.Conforming.seq_of_chain). OOCert.certificate_conforming_sound is the end of it: a checked certificate's conclusions are true, in section 5's sense, in every such interpretation of the asserted graph.

The five IP memberships that bridge used to assume, namely I(rdf:type), I(rdfs:subClassOf), I(rdfs:subPropertyOf), I(rdfs:domain) and I(rdfs:range), are now discharged. Each is a field of OOCert.Conforming asserting one axiomatic triple whose OWN PREDICATE is the term in question, so section 5's truth clause hands the membership back as that triple's first conjunct, with no table consulted:

fact axiomatic triple table
I(rdf:type) ∈ IP rdf:type rdf:type rdf:Property . RDF 1.1 §8, RDF axioms
I(rdfs:subClassOf) ∈ IP rdfs:Datatype rdfs:subClassOf rdfs:Class . RDF 1.1 §9, RDFS axiomatic triples
I(rdfs:subPropertyOf) ∈ IP rdfs:isDefinedBy rdfs:subPropertyOf rdfs:seeAlso . same
I(rdfs:domain) ∈ IP rdf:type rdfs:domain rdfs:Resource . same
I(rdfs:range) ∈ IP rdf:type rdfs:range rdfs:Class . same

Taking axiomatic triples at all is licensed by a three-link chain, quoted in the file: RBS Definition 4.2 makes an OWL 2 RDF-Based interpretation a D-interpretation; RBS section 4.2 says a D-interpretation "has to meet … those for RDF interpretations and RDFS interpretations"; RDF 1.1 section 9 says an RDFS interpretation satisfies "all the triples in the subsequent table of RDFS axiomatic triples". Only five are taken rather than the whole tables, because importing more would shrink the model class for nothing.

The last row of that table is a correction. W3C.lean sourced I(rdfs:range) ∈ IP to rdfs:range rdfs:domain rdf:Property . with the note "whose truth puts its own predicate in IP". The predicate of that triple is rdfs:domain, so its truth gives I(rdfs:domain) ∈ IP and not I(rdfs:range) ∈ IP; the fact is still available from it, through Table 5.8's rdfs:domain row, but that step was not in the entry. The triple above needs no such step.

The second kernel makes three of the same assumptions explicitly, as c_type_IP, c_sco_IP and c_spo_IP in isabelle/OO_Semantics.thy, and needs no counterpart to the other two. An earlier version of this documentation and of W3C.lean claimed the Lean needed none of them and was therefore ahead of the Isabelle on this point; the opposite was true, and dropping the IP conjunct from Interp.sat moved the obligation into the bridge rather than removing it. The Lean is now ahead on this point for a different reason: it discharges all five where the Isabelle assumes three.

What is left, and it is a containment rather than a reading. OOCert.Conforming carries a SUBSET of the Recommendation's conditions, which is the safe direction. A subset admits more interpretations, so every conforming interpretation is one of these and a sentence true throughout is true of every one of them. That it is a subset is checked cell by cell by a reader, not by Lean, and the Recommendation has fifteen condition tables where this carries rows from six.

Three further items are named at their fields rather than folded into the word "conforming". Blank nodes are rigid, which makes the entailment relation strictly smaller and the theorem strictly stronger, the same decision and the same argument as OO_Semantics.thy's DECISION M4. IEXT is total on the carrier and every condition relativises to IP exactly where the specification's quantifier does, as in DECISION M6. And IL is total, following RBS section 4.2's wording rather than RDF 1.1 section 5's "partial mapping"; this one does not run in the safe direction, because it excludes RDF 1.1 interpretations in which a literal fails to denote. Closing it needs a term-occurrence lemma about checkStep, saying that every term of a checked conclusion occurs in the asserted graph, so that in any model of the graph every such term denotes. Nobody has written it.

One reading of a cell is load-bearing and is flagged at the field: RBS Table 5.4 at n = 0, where ICEXT(c1) ∩ … ∩ ICEXT(cn) is read as IR. Rules.lean's takeChain accepts an empty chain, so cls-int1 fires on c owl:intersectionOf rdf:nil and concludes x rdf:type c for every x, and Model.int quantifies over the whole domain, so the engine and the existing Lean already depend on that reading.

lean/OOCert/ConformingWitness.lean exhibits an interpretation satisfying every stated condition, plus every RDF and RDFS axiomatic triple in both tables and three identity rows of RBS Table 5.2 that W3CWitness.lean's model records itself as violating. It also states, as checked theorems, which conditions it leaves untested (all eleven OWL-vocabulary extensions are empty there) and which Table 5.2 row it breaks (owl:Nothing | = ∅).

W3CModel is also deliberately weaker than conformance, because W3C omits every table row no rule consumes, so its class is larger than the bridge image. Both gaps run in the safe direction for soundness, where a larger class makes the conclusion stronger, and neither runs in the safe direction for a non-entailment result.

The claim that the result carries over to the OWL 2 Direct Semantics read through triples is withdrawn. Nobody verified it, and it is false as written for those twelve arms, which need a backward direction the Direct Semantics has no rdfs:subClassOf triples to carry. Do not reinstate it without a formalisation of that translation.

The axioms the theorem depends on are pinned in the source by #guard_msgs: propext, Classical.choice, Quot.sound. A sorry, or a native_decide, fails lake build.

Why the theorem is not vacuous

A soundness theorem about an unsatisfiable semantics proves nothing: if no interpretation met the conditions, every triple would be entailed and the checker could accept anything. lean/OOCert/Witness.lean closes that by construction, and its own axiom lists are pinned the same way.

theorem says
saturated_is_a_model every graph has a model, so the conditions are satisfiable and no graph is inconsistent here
not_everything_is_entailed some triple is not entailed, so Entails is not the trivial relation
the_old_svf_derivation_is_not_entailed C ⊑ ∃p.D with x p y and y ∈ D does not entail x ∈ C
the_sound_half_survives the same premises do entail x ∈ ∃p.D, so the fix did not overshoot

The third is the one worth reading. It is a machine-checked refutation of the derivation this engine used to make: a model of the premises in which x is not a C. So the removed rule was unsound in fact, not merely unjustified by the rule set the checker implements. The witness is the Herbrand interpretation of the premises plus the single consequence the semantics does force.

Which model class a negative result is about

Entailment transfers outward and non-entailment does not. A triple true in every model of the weaker Conditions is true in every W3CModel, which is what W3CEntails.of_entails proves; a triple false in some model of Conditions need not be false in any W3CModel, because that model need not be one.

So a ¬ Entails, a ¬ Unsat or an exhibited Model I G is a statement about the Lean's own model class unless something restates it over W3CModel. What that does not mean is that such a restatement is hard. IP is a free parameter of W3C, not a field of Interp, and sp_bwd, dom_bwd and rng_bwd are the only fields that take an IP membership as a hypothesis, so IP := fun _ => False makes all three vacuous. sc_bwd is guarded by IC instead, and over a Herbrand interpretation IC is the set of things the graph types as rdfs:Class, so a witness graph with no such typing makes that field vacuous too. Nine statements here are a ¬ Entails or a ¬ Unsat. ALL NINE are now over W3CModel: four with their existing witness interpretations unchanged, four on a finite structure built for them, and one by unfolding.

result over W3CModel how
not_everything_is_entailed yes not_everything_is_w3c_entailed, the empty graph's Herbrand interpretation
the_natural_avf2_direction_is_not_entailed yes the_natural_avf2_direction_is_not_w3c_entailed, a thirty-five-element structure built for it
an_unlisted_individual_is_not_entailed yes an_unlisted_individual_is_not_w3c_entailed, ooWitness unchanged
membership_in_one_member_does_not_give_the_intersection yes membership_in_one_member_is_not_w3c_enough, intWitness unchanged
mix_not_absolutely_entailed yes mix_not_absolutely_w3c_entailed in Mixed.lean, mixH unchanged
the_old_svf_derivation_is_not_entailed yes the_old_svf_derivation_is_not_w3c_entailed, an eighteen-element structure built for it
feed_is_not_refuted yes feed_is_not_w3c_refuted, a thirteen-element structure that also satisfies RefuteConditions; the verdict is ¬ W3CUnsat, which is STRONGER than ¬ Unsat
and_the_old_verdict_does_not_notice yes the_old_verdict_does_not_notice_over_w3c, the same carrier with one row changed
not_unsat_of_joint_model yes not_w3cUnsat_of_joint_w3c_model, by unfolding

Mixed.lean's mix_relative_is_not_everything and HornWitness.lean's demo_not_everything_entailed are ¬ EntailsR, about the models of a graph that also satisfy a supplied rule table. There is no W3CEntailsR, none is invented, and nothing is claimed about those two beyond Conditions.

mix_not_absolutely_entailed is the one with a verdict hanging off it: it is the machine-checked basis for a run reporting entailed_under_supplied_rules rather than entailed, and it is now the strong version of that sentence rather than the one about this layer's own conditions.

The last four rows used to read "no", with the field that fails pinned as a decide-checked theorem: svfWitness carries R owl:onProperty p and types R as nothing, so RBS Table 5.3's owl:onProperty row fails on its first conjunct; feedClosure and grazeClosure carry Lion rdfs:subClassOf Carnivore and type nothing as an rdfs:Class, so Table 5.8 row 1 forward fails on the IC conjunct it concludes. Those theorems were true and they were about the HERBRAND WITNESSES rather than about the results. A witness that is not a W3CModel is a reason to build one, and svfI and refI are the structures that were built.

An earlier version of this section said the opposite, and the reason it gave was inverted. It read: "a Herbrand witness carrying no rdf:type triple has IC empty, so Table 5.8's backward direction forces rdfs:subClassOf and rdfs:subPropertyOf triples that the witness does not contain", and concluded that "every conforming countermodel has to be a hand-built finite structure". An empty IC is exactly what makes sc_bwd vacuous; sp_bwd, dom_bwd and rng_bwd are guarded by a parameter the refuter chooses; and four of the results above transfer with nothing hand-built.

One obstruction from that paragraph survives, and it says something narrower than it was used for. RefuteWitness.lean's Der, the repository's only general "every graph has a model" machine, cannot be extended to carry Table 5.8's backward halves: the constructor would put Der to the left of an arrow and Lean rejects the strictly negative occurrence. That is mathematical and not an artefact of Lean, because sc_bwd is antitone in ICEXT(a) and there is no least fixed point by monotonicity. What follows is that there is no general closure operator taking any graph to a W3CModel. What does not follow is that no particular Herbrand interpretation is one.

The live witness, in lean/OOCert/W3CWitness.lean:

theorem says
live_is_a_w3c_model a thirty-five-element interpretation meets the quoted cells of Tables 5.2, 5.3, 5.6, 5.8, 5.9, 5.12 and 5.13, so W3C is satisfiable
live_is_live and it is not degenerate: IC is not the carrier, one class extension is everything, another is a proper subset witnessed on both sides, the filler extension is non-empty and proper, and IEXT(p1) is non-empty and a proper subset of IEXT(p2)
live_exercises_every_arm all fourteen derivations fire at concrete instances of it, which is stronger than any field being non-empty
live_fires_every_field a satisfied antecedent for each of the twenty-one fields of W3C, guards and quantified clause together for the four backward ones, so no field holds for want of anything to check
sameAs_has_no_off_diagonal_instance the one residual limit, and it is about every interpretation rather than this one: RBS Table 5.9 row 1 is an iff whose right side is an equation, so same_fwd can be exercised and can never be exercised at a ≠ b
sameAs_diagonal_needs_an_off_diagonal_subproperty and what that cell costs a model builder: with owl:sameAs carrying the diagonal, IEXT(rdfs:subPropertyOf) cannot be the diagonal too, so a countermodel needs two distinct properties one below the other
the_natural_avf2_direction_is_not_w3c_entailed the reversed scm-avf2 conclusion fails in that interpretation
not_everything_is_w3c_entailed W3CEntails is not the trivial relation either

The first version of that model was vacuous where it mattered most and is recorded in the file as such. IEXT(p1) and ICEXT(Y) were both empty, nine of the twenty-one fields of W3C held because nothing was in the extension their antecedent reads, six of the fourteen arms rested entirely on those nine, and the refutation's own premise p1 rdfs:subPropertyOf p2 held because sp_bwd had nothing to check. Worse, the two emptinesses were conjuncts of live_is_live, the theorem whose job is to catch exactly that. The rebuilt model gives p1 a pair, Y a member, and each of the six dead arms a configuration to fire on. It left five fields still vacuous, and a second rebuild closed those too: owl:sameAs, owl:inverseOf, owl:hasValue, owl:SymmetricProperty and owl:TransitiveProperty had been falling through the denotation table to the junk element, and they now denote elements with rows of their own. The note that came with the five said owl:sameAs "cannot be exercised by any model at all", which is false: RBS section 4.2 makes IR nonempty and Table 5.9 row 1 makes the extension the whole diagonal on it, so a model that leaves it empty is failing to model that cell rather than obeying it.

the_natural_avf2_direction_is_not_w3c_entailed is still not a proof that the triple fails to be OWL 2 RDF-Based entailed, and nobody should write that sentence. W3CModel's class is larger than the conforming interpretations, because W3C omits every table row no rule consumes: the model violates Table 5.2's owl:Thing | = IR and rdf:Property | = IP rows, and the axiomatic triple tables are absent entirely. It is closer to the specification than anything else here and it does not arrive.

What is not proved

  • Completeness. The checker rejects anything it cannot re-derive by pattern, including valid inferences in an order it does not expect. A rejection is a false alarm at worst, never a false pass.
  • The parser and the file format (lean/OOCert/Parse.lean, lean/Main.lean). A parse error rejects.
  • Anything outside the forward-chaining family: the SHACL validator (the pyshacl differential in tools/shacl_differential.py is its gate), the SHIQ tableaux reasoner, the RDF parsers.
  • Datatype semantics. Two spellings of one literal value are two terms. No rule compares literals by value, so nothing is lost, but do not read Entails as datatype-aware.

What it caught on day one

An adversarial audit of the whole layer on 13 September 2026 found nine more defects, seven of them predating the certificate work: a false clean from unscoped prefix declarations, an ignored sh:deactivated, a truncation that silently disabled any constraint mentioning a typed literal, a blank-node shape acting as a wildcard, a reasoner that was not a fixpoint, four rules that could emit an unserialisable triple, and a CI job that could not pass. All are fixed and pinned; the CHANGELOG lists them.

cls-svf1 in the owl-rl-ext profile derived x rdf:type C from C rdfs:subClassOf ∃p.D, x p y and y rdf:type D. That is the converse of the axiom. It also treated x p D, with D the filler class IRI itself, as a witness. Neither has a sound rule, so neither could be given one in the checker, and both are gone (tests/reason_rl_ext_soundness_test.rs). The old derivation is kept in tests/lean_certificate_test.rs as a forged certificate the checker must reject.

In CI

The lean job builds lean/ (which is the proof check), then runs tests/lean_certificate_test.rs with OO_REQUIRE_FIXTURES=1. Every RDF file the repository tracks, enumerated from git ls-files, is loaded, reasoned under owl-rl-ext with a certificate, and the certificate checked. Files over 4 MB and files that do not parse are listed with the reason, never dropped silently. The same test appends three forgeries and requires each to be rejected.

The corpus was 122 files and 37,133 derivations when that was written. Counted on 14 September 2026 under the test's own SKIP_DIRS filter it is 290 tracked RDF files, 21,256,445 bytes (20.3 MiB), one of which (case-studies/skills-england-occupational-maps/ontology/occupational-map.ttl, 5.70 MB) is over the 4 MB cap and is therefore already excluded and named. The derivation count is not restated here, because the only honest source for it is the run's own output.

The corpus used to be five hand-named directories, three of which hold no RDF, so 46% of the repository's RDF was never walked and was excluded without being named. Widening it is what surfaced the literal-subject defect in prp-symp, prp-inv1, prp-inv2 and eq-sym, which lived in benchmark/.

Refutations: certifying that a graph has NO model

A derivation certificate says a triple follows. A refutation says the graph contradicts itself, and it needs a second format because there is no triple to conclude. lean/OOCert/Refute.lean holds it, oo-refute checks it, and OOCert.refutation_sound is proved about it.

The reasoner now writes one. reason --certificate DIR looks for a contradiction in the closure it reached and, when it finds one the checker can judge, writes DIR/refutation.tsv beside the other two files.

open-ontologies reason --profile owl-rl --certificate /tmp/cert
cd lean
lake exe oo-refute check /tmp/cert/asserted.tsv /tmp/cert/refutation.tsv
lake exe oo-refute guard /tmp/cert/asserted.tsv /tmp/cert/derivations.tsv /tmp/cert/refutation.tsv

check exits 0 when the refutation is valid, which is a good exit code reporting bad news. guard runs both checkers and REFUSES the derivation certificate when the refutation succeeds, because over a refuted graph every triple is entailed under the disjointness reading and an ordinary certificate carries no information (OOCert.a_certificate_adds_nothing_when_the_graph_is_refuted). oo-cert will still accept that certificate and will still be telling the truth: its verdict quantifies over a model class that ignores disjointness, and that class is never empty.

The response gains an inconsistency object:

{
  "inconsistency": {
    "found": true,
    "verdict": "clash_found_by_this_engine",
    "checked_by_lean": false,
    "by_rule": {"cax-dw": 1},
    "refutation": {
      "written": true,
      "rule": "cax-dw",
      "prefix": 2,
      "verdict": "refutation_written_not_yet_checked",
      "check_with": "cd lean && lake exe oo-refute check /tmp/cert/asserted.tsv /tmp/cert/refutation.tsv"
    }
  }
}

Read the two verdicts apart. clash_found_by_this_engine is this engine saying so, with nothing behind it. unsatisfiable_under_disjointness is what oo-refute prints when it has ACCEPTED a refutation, and the engine never states it. tests/lean_refutation_producer_test.rs::the_engine_never_states_the_checkers_verdict fails if any string in the response is ever that verdict, on the pattern the Horn layer's laundering guard set.

Which rules conclude false, and which of them can be certified

Seventeen rules of the OWL 2 RL profile conclude false rather than a triple. None of them is in the forward-chaining table, and none could be: a certificate step's conclusion is a triple. They are looked for once, after the fixpoint.

rule detected certifiable
cax-dw (c1 owl:disjointWith c2, x a c1, x a c2) yes yes
cls-com (owl:complementOf) yes no
cls-nothing2 (x a owl:Nothing) yes no
cls-maxc1 (owl:maxCardinality 0) yes no
eq-diff1 (owl:sameAs and owl:differentFrom) yes no
prp-irp (owl:IrreflexiveProperty) yes no
prp-asyp (owl:AsymmetricProperty) yes no
prp-pdw (owl:propertyDisjointWith) yes no
prp-npa1, prp-npa2 (negative property assertions) yes no
cax-adc, prp-adp, eq-diff2, eq-diff3 no, they read an RDF list no
cls-maxqc1, cls-maxqc2 no, qualified cardinality is not implemented no
dt-not-type no, an ill-typed literal needs a datatype value space no

Only cax-dw is certifiable, and the reason belongs to the checker rather than to the engine. OOCert.RefuteConditions carries exactly one semantic field, for cax-dw, and oo-refute refuses a refutation naming any other clash rule with exit 2 rather than guessing at it. So the producer writes a refutation for that rule alone. For the other nine it detects, the response says a clash was found and "refutation": {"written": false} with the reason. Every rule the engine does not look for is listed in rules_not_detected with its own reason, so a run with no clash is never a consistency result: most of the table was not tried.

lean/OOCert/Refute.lean says sixteen rules conclude false. Counted against the W3C tables it is seventeen; the difference is dt-not-type, which that file excludes elsewhere on the stated ground that the Lean semantics has no datatype value space. Nothing computes with the number.

The limit, which is real

cax-dw needs an INDIVIDUAL in two disjoint classes. A TBox that is unsatisfiable with no individual asserted cannot be seen this way at all. :Lion rdfs:subClassOf :Carnivore, :Herbivore with those two disjoint makes :Lion unsatisfiable, and until something is asserted to BE a :Lion the rule-based route has nothing to fire on. That is a boundary of forward chaining, not a defect in the producer.

The SHIQ tableau (--profile owl-dl, src/tableaux.rs) does see it, and reports unsatisfiable_classes. Its answer carries no certificate, which its own report already states ("not_covered": "unsatisfiability and inconsistency carry no certificate"). No refutation is emitted from it, and the obstruction is precise rather than a matter of effort:

  • oo-refute/1 can express exactly one contradiction, cax-dw, whose three premises must each be asserted or concluded by a step of the 29-rule forward-chaining prefix. A tableau clash reached through ∃/∀ expansion, node merging or a cardinality bound is not three triples of that shape and there is nothing in the format to write it as.
  • Where a tableau clash IS a cax-dw instance over triples the forward-chaining rules can reach, the rule-based producer has already found it, so the tableau adds nothing that can be certified.
  • Feeding the tableau's inferred subsumptions back into the store and re-reasoning would let more clashes surface, but those subsumptions would then appear in asserted.tsv as axioms with nothing marking them derived. That is the assumption-laundering failure this layer exists to prevent, so it is not done.
  • Adding a clash rule to the format means a new field in OOCert.RefuteConditions, a new arm in OOCert.checkRefuteStep and a new soundness case. That is a change to lean/, not to the producer.

tests/lean_refutation_producer_test.rs::the_tbox_only_case_is_invisible_here_and_the_tableau_sees_it computes this boundary on one ontology rather than asserting it here.

onto_defects asks a different question again, and the three do not substitute for one another. It checks the ontology against ITSELF with no data present, so disjoint_with_ancestor and inherited_disjoint catch the schema that will contradict itself the moment an instance arrives. This layer needs the instance to be there. The tableau needs neither and certifies nothing.

User-written rules

The twenty built-in rules were twenty arms in the checker, which does not extend to rules you write. lean/OOCert/Horn.lean makes a rule into data: a body and a head over triple patterns with variables. A certificate step cites a rule by index into a table you supply and gives a binding, and one theorem, OOCert.horn_certificate_sound, covers every rule table at once.

cd lean
lake build
lake exe oo-horn rules                                    # the built-in table, as data
lake exe oo-horn check RULES.tsv ASSERTED.tsv HORN.tsv    # check a certificate

The verdict tells you what it is relative to, and you must read it.

table verdict theorem means
exactly the built-ins entailed OOCert.entails_of_builtin_horn true in every model of the asserted graph
anything else entailed_under_supplied_rules OOCert.horn_certificate_sound true in every model that also satisfies your rules

The second is weaker and the difference is not academic. A rule reading "every supplier is compliant" makes certificates that check green for ever, because the certificate certifies the inference and never the premises. The report carries a digest of the table that was in force so two runs can be compared, and tests/lean_horn_certificate_test.rs fails if a user-rule run ever reports the absolute verdict.

Twenty-seven of the engine's rules are Horn rules and appear in the built-in table, the count the_built_in_rules_are_emitted_as_data pins. Four are not: cls-int1, cls-int2, cls-uni and cls-oo each read an RDF list off the graph, so the LIST is a premise and the premise count is data rather than fixed by the rule. They remain hardcoded arms. A user rule language stops at the same boundary.

What a binding must look like

A step's binding is a list of var TAB term pairs and it is data before it is a substitution. Two shapes are refused, on both checkers:

shape example why
a key bound twice x <http://ex.org/a> x <http://ex.org/zzz> the two pairs demand two different values for one variable, so NO substitution satisfies both and there is nothing for a checker to read: first-wins (Lean's List.lookup, Isabelle's map_of) and last-wins (Python's dict(), Rust's HashMap::from_iter) are two conventions for discarding half the certificate, not two readings of it
a variable of the cited rule with no binding binding s, o for the rule ?s <p> ?o -> ?s <q> ?z the checker would otherwise have to invent a value, and the only one available is the variable's NAME, so the conclusion would carry a term nobody wrote

A binding for a variable the cited rule never mentions is accepted: it is never consulted, so it cannot make a certificate mean two things.

Both refusals are strictness and neither carries soundness content. What they buy is that a certificate has ONE meaning, which OOCert.wellFormed_determines_instantiation states and the Lean kernel checks. Read the binding as a set of demands, "this variable is that term", one per written pair. Distinct keys make those demands SATISFIABLE and coverage makes every substitution satisfying them instantiate the cited rule the SAME WAY, so one refusal buys existence and the other buys uniqueness. The defect they close was found by running this checker and the independent Isabelle/HOL one in isabelle/ over 1,718 certificates: 47 rows disagreed, all from this one cause. See decision 0008.

This does not make a conclusion writable RDF. Binding z to the bare term z is required and still accepted, so a certificate can still conclude a triple no serialiser can write; what changed is that the term must be written by the certificate's author rather than minted by the checker. reason --rules cannot emit either refused shape, which tests/reason_horn_emit_test.rs::no_emitted_binding_is_one_the_format_now_refuses checks against the bytes rather than asserting.

reason --rules TABLE --certificate DIR evaluates a supplied table to a fixpoint over the loaded graph and writes the three files oo-horn check reads. Nothing is materialised: a conclusion drawn under a table nobody has checked holds only in models that satisfy that table, and writing it into the store beside the assertions would lose exactly that distinction. See decision 0003.

Rules you wrote in SWRL or RIF Core

rules.tsv is an internal encoding, not a language anybody writes in. rules-import reads two standard rule syntaxes into it.

open-ontologies load ontology.ttl
open-ontologies rules-import --from swrl --out rules.tsv              # SWRL, out of the loaded graph
open-ontologies rules-import --from swrl --file rules.owl --out rules.tsv
open-ontologies rules-import --from rif  --file rules.xml --out rules.tsv
open-ontologies reason --rules rules.tsv --certificate cert/
cd lean && lake exe oo-horn check ../cert/rules.tsv ../cert/asserted.tsv ../cert/horn.tsv

Only part of each language is a Horn table over triple patterns, and the exact fragment is in docs/rule-syntax-front-ends.md and in every response. A rule outside it is named, counted and refused; by default one refusal fails the whole import and writes nothing, because a table that quietly lost a rule still reaches a fixpoint and still produces a certificate that checks green, which is a sound proof about a rule set nobody wrote. --allow-partial imports the rest and flags the result certifies_a_weaker_rule_set.

Every imported rule is a rule you wrote, so it lands on the second row of the table above without exception: imported rules are named swrl/… and rif/…, no built-in rule is, and oo-horn awards the absolute verdict only to a table that renders identically to the built-in one. The Rust reasoner evaluates a supplied rule table through reason --rules RULES.tsv --certificate DIR, which writes rules.tsv, asserted.tsv and horn.tsv and states no verdict of its own. Nothing is materialised into the store: a conclusion drawn under a table you wrote holds only in models that satisfy that table, and merging it in beside the assertions would lose exactly the distinction this is about. See decision 0003.

What the checker assumes about the engine

The theorem is conditional. It says that IF the asserted graph is G and IF these steps check, THEN the conclusions hold in every model of G. Everything to the left of that is the Rust writing down the truth, and the checker cannot see any of it: it reads files, not the store and not the run. docs/trusted-computing-base.md enumerates that boundary as thirty checkable properties and says for each what checks it. Read it before relying on a certificate, because a certificate is a claim about a file and the file's relationship to the store is the part nobody proved.

First-order model certificates: oo-folmodel

A solver's sat answer is worth nothing on its own and everything once the model comes with it. lean/Fol/ holds a checker for a finite first-order structure, and Fol.satisfiable_of_check says that a structure it accepts really does satisfy every formula of the problem, so the problem is satisfiable. Fol.not_entails_of_check is the sharper form: a checked model of ¬φ together with Γ is a machine-checked proof that Γ does not entail φ.

cd lean
lake build                                                  # builds the checker AND checks the proofs
lake exe oo-folmodel PROBLEM.tsv MODEL.tsv
{"verdict":"model_checked","formulas":5,"domain":2,"closed":true,
 "goal_negated_present":true,"source":"z3","cardinality_search":"1,2",
 "problem_digest":"4403d8aaa0c422f7","theorem":"Fol.satisfiable_of_check",
 "non_entailment_theorem":"Fol.not_entails_of_check"}

The two file formats, with a worked example whose digest is pinned by the build, are documented in lean/Fol/Syntax.lean. Runnable copies of every case below are in tests/fixtures/folmodel/.

Exit codes, and the fixture that demonstrates each.

exit verdict reason fixture
0 model_checked problem.tsv + model.tsv
1 rejected the checker rejected the structure model_no_edge.tsv
1 rejected problem_digest_mismatch model_wrong_digest.tsv, problem_other.tsv
1 rejected undeclared_symbol model_undeclared.tsv
2 unreadable the carrier is empty model_empty_domain.tsv
2 unreadable a row contradicts a declared arity model_bad_arity.tsv
2 unreadable an index is outside the carrier model_index_out_of_range.tsv
2 unreadable a declared symbol has no row model_missing_row.tsv
2 unreadable the problem carries no formulas problem_empty.tsv

The verdict tells you what it is relative to, and you must read it. These four are the SOLVER level, and a driver that collapses any two of them is reporting a falsehood from correct solver output.

solver said encoding verdict theorem means
sat, with a model the checker accepted either model_checked Fol.satisfiable_of_check the problem has a model, exhibited
sat, no checkable model either satisfiable_oracle none trust the solver
unsat finite(k) no_model_up_to_size_k none not unsatisfiability
unsat unbounded unsatisfiable_oracle none trust the solver, and never more

no_model_up_to_size_k is the one people get wrong. ∀x∃y (r(x,y) ∧ x≠y) is unsat at carrier 1 and sat at carrier 2, so a bounded unsat is frequently not evidence of anything. A solver that answers sat whose model the checker then REJECTS is satisfiable_oracle with checker_exit: 1, never rejected as though the ontology were at fault.

Two gates that are not soundness gates, and are labelled so.

  • undeclared_symbol is an ATTRIBUTION gate. Fol.FinModel's three fields are total, so an undeclared symbol is still interpreted and the theorem holds without the gate. What it buys is that the structure certified is the structure the solver described rather than that structure completed with defaults. The JSON carries "gate":"attribution" so a report cannot quietly promote it.
  • problem_digest_mismatch binds model.tsv to problem.tsv. The digest is FNV-1a 64 over the canonical re-serialisation of the parsed formula list, specified in lean/Fol/Parse.lean so a Rust writer can reproduce it. It identifies; it does not commit.

Cost, measured on this machine (Apple silicon, compiled oo-folmodel, 2000 formulas at quantifier depth 3, so carrier^3 evaluation points per formula):

carrier evaluation points user time
8 1.0M 0.14 s
16 8.2M 0.92 s
24 27.6M 2.93 s
32 65.5M 6.80 s

About 9M points per second, cubic in the carrier at this depth. Solvers return carriers in the single digits on real ontologies, so this is a cap to state rather than a problem to solve: --max-domain defaults to 16 and the flag goes higher with the cost documented.

Driving all of it in one command: fol-model

oo-folmodel checks a model somebody already has. open-ontologies fol-model produces one: it exports the ontology, runs Z3 or Mace4, reads the structure back, runs the checker, and reports the verdict with the five fields above.

cd lean && lake build && cd ..                     # the checker, and its proofs
printf 'load case-studies/blast-furnace-ironmaking/blast-furnace-ontology.ttl\n\
fol-model --out /tmp/solve --solver z3 --max-domain 8\n' \
  | open-ontologies --no-connect --data-dir /tmp/store batch -
{"verdict":"model_checked","solver_verdict":"sat","encoding":"finite(1)","checker_exit":0,
 "owl_reading":null,"theorem":"Fol.satisfiable_of_check","formulas":45,
 "problem_digest":"27751aa61e9de6fd","cardinality_search":[1],
 "bounded_search":"a model was reported at carrier 1","dropped_symbols":[],"seconds":0.084}

Every intermediate file lands in --out, so a run is reproducible by hand from what it leaves behind: problem.tsv and its digest, problem_k1.smt2 (or problem.in plus symbols.tsv for Mace4), the solver's raw output, model.tsv, and checker.json.

Pass --goals a TSV of triples — derivations.tsv from reason --certificate is the intended input, with --goals-skip-columns 1 — and each becomes its own run asking whether the ontology FAILS to entail it. A model_checked there carries owl_reading: "not_entailed_under_unproved_translation", which is Fol.not_entails_of_check plus two things this layer does not prove: OwlLean.adequacy lives in a sibling project, and the Rust-to-Lean translation correspondence is pinned by tests and not proved. Never shorten it to "not entailed".

A rejected model stops the line. If a solver answers sat and the checker rejects the structure, the verdict stays satisfiable_oracle — it is not a fact about the ontology — but the report carries a disagreement block with severity: STOP_THE_LINE, the run summary counts it, and the command exits non-zero. That is the treatment tools/shacl_differential.py gives a FALSE_CLEAN, for the same reason: a disagreement between a checker and the thing it is checking is the one result that must fail a pipeline.

The two finders differ in what they can be asked, and the verdict rules read the difference.

Z3 Mace4
format SMT-LIB 2 (fol --format smtlib) LADR (fol --format ladr)
smallest carrier 1 2 — mace4 -n 1 is a FATAL error, measured
unbounded question yes, so unsatisfiable_oracle is reachable no, it is a finite model finder
symbols quoted with vertical bars MANGLED to p0/r0/c0, table in symbols.tsv
reduct auxiliary functions Skolem functions and constants

Mangling is not a style choice. LADR reads a name whose first letter is in {u,v,w,x,y,z} as a VARIABLE, so an IRI beginning with one of those becomes universally quantified and Mace4 silently searches a different problem. Measured on LADR 2009-11A: p0(w0). -p0(k0). is echoed in Mace4's own CLAUSES FOR SEARCH block as p0(x). and -p0(k0)., and the run reports exit (exhausted) with no error at all.

What is proved, and what is not, on this layer

Every result in lean/Fol/ has axiom footprint [propext, Quot.sound] or smaller, pinned by #guard_msgs in the source. Classical.choice appears nowhere in the layer, which is tighter than the triple the older layers carry.

theorem says
Fol.eval_iff the Boolean evaluator and the Prop satisfaction relation agree, at every formula and environment
Fol.satisfiable_of_check an accepted structure is an existence proof: the problem is satisfiable
Fol.check_complete the gate can fail: a rejection is about the structure, not the checker's patience
Fol.check_complete_closed for a problem of sentences, a rejected structure is not a model under any assignment
Fol.not_entails_of_check a checked model of ¬φ :: Γ proves Γ does not entail φ

lean/Fol/Witness.lean closes the vacuity question by construction: employment_is_satisfiable accepts a real structure, the_model_does_not_satisfy_everything shows that same structure refuses a formula, not_everything_is_satisfiable shows Satisfiable is not the trivial predicate, and five named forgeries are each rejected on their own through check_complete, so it is the checker's own rejection that is certified rather than an independent argument.

Not proved, and named next to the verdict rather than in a footnote:

  • Nothing about unsatisfiability, in any direction, ever.
  • The absence of a finite model implies nothing. SHIQ lacks the finite model property, so a satisfiable ontology can have only infinite models and will never receive a certificate.
  • The OWL-level reading rides on OwlLean.adequacy in the sibling project and on the Rust-to-Lean translation correspondence, which decision 0005 states is pinned by tests and not proved. It carries its own word, not_entailed_under_unproved_translation, which must never be shortened to "not entailed".
  • The parser and the file formats (lean/Fol/Parse.lean, lean/FolMain.lean). A parse error is exit 2 and never a verdict in either direction.

Nothing in src/ writes either file yet, so today this layer checks certificates rather than producing them. See decision 0006.

Does a retrieved slice still support the answer?

A certificate says the engine's inferences over ONE graph are entailed by it. A GraphRAG pipeline asks a different question: an answer was grounded in a retrieved slice, so does that slice still entail the claims the answer rests on?

preserve and graph_projection_entailment_check ask it per claim, and every preserved-and-derived claim gets a SUB-CERTIFICATE extracted from the projection's own derivations.tsv and checked by oo-cert against the projection's own asserted.tsv. No new Lean was written: OOCert.certificate_sound covers it unchanged, and the sub-certificate's line order is valid because run_full computes a round's conclusions from the closure as it stood at the start of the round, so every premise was asserted or concluded strictly earlier.

The verdict table follows the one above.

verdict theorem means
preserved_checked OOCert.certificate_sound the projection entails the claim, machine-checked
preserved_under_supplied_rules_checked OOCert.horn_certificate_sound true in every model of the projection that also satisfies your rules. Carries the table's digest. Never shortened
preserved_asserted none the claim is literally in the slice. A lookup, not a theorem
preserved_unchecked none the ENGINE derived it and no checker looked
lost_under_profile_unchecked none not derivable from the slice under this profile, bounded by a rule table covering 29 of the profile's 78 rules
ungrounded_in_source none NEITHER graph derives it, so the generator invented it and a better retriever will not help

Every run also checks monotonicity: OWL RL is monotone and a projection is a subset, so anything the projection entails and the source does not is a soundness bug in this engine, reported at STOP_THE_LINE rather than as a retrieval result. It is disarmed, loudly and with its own reason, when the projection is not a subset, when blank nodes could not be matched, or when either run stopped at the iteration cap instead of a fixpoint.

Run over the shipped corpus, 275 ontologies swept with the gate armed on all 275 and every source certificate accepted by oo-cert, it found nothing.

See docs/projection-entailment.md and decision 0007.

Known limitations

Stated rather than discovered later.

  • A conclusion no RDF serialiser can write is refused, not derived. A literal in subject position or a non-IRI in predicate position produces a triple the store cannot hold. Such a conclusion is not materialised, not certified, and not used as a premise, so a run that hits one derives LESS than its rule set licenses. The count and up to three examples come back as skipped_unserialisable and skipped_examples. This is reachable from ordinary OWL: :p rdfs:subPropertyOf [ owl:inverseOf :q ] is what the OWL 2 mapping to RDF produces for SubObjectPropertyOf(:p ObjectInverseOf(:q)), and it makes rdfs7 conclude a triple with a blank node in predicate position.
  • The rule table is this engine's, not W3C's. by_rule describes what this engine did. It is not an OWL 2 RL conformance claim, and the engine does not implement every rule in the profile.
  • The Rust and Python reasoners are NOT independent, so their agreement is worth less than it reads. tools/horn_differential.py runs src/reason.rs, the pure-Python engine in python/src/open_ontologies_lite/horn/ and oo-horn over every RDF document the repository tracks, and reports a clean sweep. The two ENGINES run the same semi-naive forward-chaining algorithm over the same rule table; the Python was written with the Rust open and its comments cite src/reason.rs by file and line. That makes their agreement STRONG evidence against a transcription slip in one of the two — an index off by one, a guard dropped, a join in the wrong order — and CLOSE TO NO evidence against a shared misreading of a W3C rule, which both would implement and agree on for ever. The independent leg is the Lean checker, written from the W3C rules with a machine-checked soundness theorem. The tool prints this caveat next to its agreement count on every run. Never quote the sweep as "two independent reasoners agree".
  • Seven of the twenty-seven rules fire nowhere in the repository's own RDF. Measured on 14 September 2026: the corpus exercises 20 of 27, and prp-inv2, eq-sym, cls-avf, cls-hv1, cls-hv2, scm-svf2 and scm-avf2 never fire in it, so the differential compared the two engines on them zero times. tests/fixtures/horn-coverage/ holds one deliberately built graph per silent rule, each the smallest thing that makes exactly that rule fire, and the differential runs them as a separate labelled set. The two figures are reported apart and must not be added: 20 of 27 on real ontologies, 27 of 27 once fixtures written for the purpose are included. A rule covered only by its own fixture has been compared on one graph made to fire it and on no real data. Re-measured on 15 September 2026 over a corpus that had meanwhile grown to 291 documents and 203,825 asserted triples: the same 20, the same seven silent, and all seven fixtures firing exactly their own rule once. No rule in the table is unreachable, so the seven were a gap in the corpus and not a defect in the engine.
  • asserted.tsv is the store, not your file. Quads are flattened, so a triple present in two named graphs appears on two lines. Literals are as the store gives them back, which since #335 is as they were written: "01"^^xsd:integer stays "01" (under Oxigraph 0.5.9 it was written "1"^^xsd:integer). The guarantee is relative to that file.
  • asserted.tsv is the store the run SELECTED, and the checker cannot see the selection. By default that is every graph. Over a store that keeps several versions of an entity in several named graphs, the union of every version is a state that held at no instant, and a certificate over it is a valid proof about a graph that never existed — oo-cert accepts it, correctly, and oo-refute will accept a cax-dw refutation drawn from two versions that never coexisted. That is issue #108. Two things changed: a run over a store that uses the temporal vocabulary is REFUSED unless the caller names an instant (valid_at / as_of) or asks for every version by name (all_versions), and every certificate directory now gets scope.tsv, an oo-scope/1 record of which graphs the run read. No Lean checker reads scope.tsv. It is evidence for a person, not a proof; see docs/trusted-computing-base.md items 11 to 13 for what it does not cover.
  • Reasoning twice into one store. The run now reaches a fixpoint, so a second run adds nothing, but if you materialise into a store that already held inferences they appear in asserted.tsv as assumptions with nothing marking them derived. Use inference_graph: true (decision 0001) when that distinction matters — and note that this separates the SAVE, not the certificate: an unscoped run reads every named graph, the inference graph included. A SCOPED run does not: it drops the inference graph from what it reads, records the drop in scope.tsv, and materialises nothing of its own.
  • No clash found is not consistency. Seven of the seventeen clash rules are not looked for at all and eight of the ten that are cannot be certified, so a clean reason run means "none of the ten rules tried fired", never "this ontology is consistent". A rejected refutation means the same: oo-refute's own report says so in every verdict it prints.
  • One clash is reported per refutation, and only the first certifiable one is written. A graph with twenty disjointness clashes gets one refutation.tsv. clash_count and by_rule carry the rest; ten are listed in full under clashes. Refuting a graph once is enough to invalidate every derivation over it, so a second refutation would add nothing.
  • The refutation's derivation prefix is not byte-stable across runs. Which of several valid derivations of a premise the fixpoint recorded first depends on the same hash iteration order that already decides the line order of derivations.tsv. The contradiction itself IS stable: clashes are sorted on their N-Triples spelling before one is chosen.
  • A SHACL report double-counts a node selected by two target declarations of one shape. Both focus_nodes and violation_count are affected. Collapsing identical results is not the fix: SHACL emits one result per SPARQL solution, pyshacl does too, and deduplicating breaks an exact agreement with it. The fix is to union a shape's focus nodes across its declarations, which is a change to the evaluation loop and is not done.