PROVENANCE.md

Where the HQDM inputs came from

HQDM is published as two files that disagree about what HQDM is. The figure draws both, under the same checks, and every count in it is recomputed from these inputs by tests/hqdm_audit_asset_test.rs.

asserted.tsv: the RDFS rendering

hqdmTop/hqdmFramework, path rdf/hqdm-0.0.1-alpha.ttl, 79,623 bytes.

MagmaCore vendors the same file at examples/src/test/resources/hqdm-0.0.1-alpha.ttl. The two are byte identical, verified with cmp, so the audit is of upstream HQDM and not of something MagmaCore changed.

asserted.tsv is that file with its three prefixes expanded and one triple per line, subject, predicate, object, tab separated. Nothing is added, removed or reordered: 1,094 triples in, 1,094 out. It parses as a flat S P O . grammar because the source uses no blank nodes, no lists and no literals. Its whole predicate inventory is rdf:type 210, rdfs:subClassOf 372, rdfs:domain 257, rdfs:range 255. It contains no owl: term and no disjointness axiom, so no named class in it can be unsatisfiable and a coherence check on it returns zero however carefully it is run.

hqdm.owl and owl-rows.tsv: the OWL rendering

gchq/HQDM, file hqdm.owl, RDF/XML, 366,581 bytes, Apache-2.0, Crown Copyright. sha256 be27ee353e2fefe7…47caff8, the same file the OM 2026 paper measured. It is vendored here unchanged so the test below can reason over it.

owl-rows.tsv is that file read by rdflib 7.6.0 and written one triple per line in the same tab-separated form: 3,127 triples in, 3,127 out. Blank nodes are written _:label and literals in double quotes; the well-formedness checks only read rows whose subject and object are IRIs, so neither matters to them. It carries 234 owl:Class declarations (229 named, the rest anonymous), 14 owl:disjointWith axioms and 268 qualified cardinality restrictions.

owl-dl.json: this engine's run over hqdm.owl

open-ontologies batch --data-dir <dir> <<'B'
load docs/assets/hqdm/hqdm.owl
reason owl-dl
B

with <dir>/config.toml raising the per-phase budget:

[reasoner]
tableaux_test_timeout_ms = 120000
classify_timeout_ms = 900000

The SHIQ tableaux checks 229 named classes, finds 190 satisfiable and 39 unsatisfiable, and leaves none undetermined, in 91 ms. complete is false and search_finished is true: the file has 23 restrictions on datatype properties, which this engine reads only approximately, and the run names them under constructs_not_modelled. The file keeps the fields the figure reads and drops the inferred subsumptions. the_reasoner_still_gives_the_committed_verdicts in the test recomputes this run in-process and requires the same two sets.

The budget block was replaced on 2026-10-28 (#339). Until then a one-shot batch ignored [reasoner] in config.toml, so the committed block reported the default 10000 ms phase and 180000 ms ceiling, not the budgets above. The same command rerun with the fix reports 120000 and 900000, and every verdict field (unsatisfiable_classes, undetermined_classes, consistent, complete, search_finished, named_classes, budget_exhausted_in, constructs_not_modelled) is identical, which is expected: the run never came near either budget.

Regenerated on 2026-10-13. The run committed before that checked 234 classes, found 195 satisfiable, refuted none and left these 39 undetermined on the tableaux's expansion cap. Two changes account for the difference. Five of the 234 were anonymous owl:Class nodes taken for named classes, which is why the count is now 229 and the satisfiable count 190. And absorption, backjumping and the absorption of owl:disjointWith as A ⊓ B ⊑ ⊥ let the search finish on the 39.

hermit-unsatisfiable.txt: the oracle's list

The 39 classes HermiT reports as unsatisfiable in hqdm.owl, as recorded by the OM 2026 crosswalk's reasoning run (hqdm_prerepair_results.json, deleted_classes). HermiT is an external reasoner and, in this repository's vocabulary, an opinion: nothing checks its proof. The figure does not repeat the paper's 39; it intersects this list with the engine's undetermined set and prints the size of the intersection with the engine's own unsatisfiable set, which is all 39: the engine and the oracle name the same classes.

What the checks find

Three things a coherence check cannot see, recomputed from the rows:

1. Terms used as a class and never declared rdf:type rdfs:Class or owl:Class, as a subject or object of rdfs:subClassOf, or as the object of rdfs:domain or rdfs:range. A datatype in range position (xsd:*, rdfs:Literal) is correct RDFS and is not counted. RDFS rendering: 23 (hqdm:thing is declared, at line 1067 of the source, so this is not a parsing artefact). OWL rendering: 0.
2. rdfs:range declarations naming a relation: terms that are never declared a class and never appear in the subclass hierarchy in either position, so they are relation names standing where RDFS requires a class. RDFS rendering: 12, at hqdm:part_of (9) and hqdm:participant_in (3). OWL rendering: 0.
3. Pairs of names one trailing underscore apart. RDFS rendering: 13, ten sharing a domain and differing in range, and three, contract_process_consists_of, offer_and_acceptance_for_goods_consists_of and sale_of_goods_consists_of, identical in domain and range. OWL rendering: 6, none identical.

And one thing only a reasoner can see, on the file that has enough axioms to carry it: the 39 classes above.