v0.3.3 — full measured-corpus Konclude parity
Highlights
Full Konclude parity across all 9 measured corpus fixtures — FP=0 AND MISSED=0. This release closes the last completeness gap (SIO).
| Fixture | FP | MISSED |
|---|---|---|
| alehif | 0 | 0 |
| galen | 0 | 0 |
| notgalen | 0 | 0 |
| ro | 0 | 0 |
| shoiq-knowledge | 0 | 0 |
| sulo | 0 | 0 |
| ore-10908-sroiq | 0 | 0 |
| ore-15672-shoin | 0 | 0 |
| sio | 0 | 0 |
SIO disjunction-common-subsumer pass (#16)
New preprocessing pass (crates/owl-dl-core/src/disjunction_existential.rs, run in convert_ontology): for X ⊑ ∃R.(D1 ⊔ … ⊔ Dn) with all disjuncts atomic, emit X ⊑ ∃R.C for each minimal common told-subsumer C. The EL saturator drops union-filler existentials; feeding it the case-split (D1⊔…⊔Dn) ⊑ C lets classify recover the subsumption via its saturation-closure short-circuit, sidestepping the per-pair tableau/wedge (which times out / doesn't close at SIO scale).
Closes SIO_010092 ⊑ SIO_001353 and ⊑ SIO_010410 (SIO MISSED 2 → 0).
Soundness (analytic + empirical): adding an entailed axiom is model-preserving — no verdict on any task can change, only previously-missed entailments become derivable. Only told subsumers of atomic disjuncts are used, so false positives are impossible. FP=0 held across all 9 fixtures (the pass runs on every convert). Independently attested by a textbook derivation and Konclude's ground truth.
Performance
No regression from the pass (A/B on the largest inputs, within run-to-run noise). Bounded classify (--pair-timeout-ms 200) walls: galen 0.59 s, notgalen 1.03 s (Horn fast path), pizza 2.07 s, go-basic 18.65 s, family 27.81 s, sio 31.79 s. See docs/perf-2026-06-06-corpus.md.
This is parity on the measured corpus, not a universal completeness guarantee — non-atomic disjuncts and derived-only common subsumers remain deliberately tableau-deferred.
Full changelog: v0.3.2...v0.3.3