v0.3.4 — nominal-reasoning lever + corpus expansion (wine, bibtex)

Highlights

Corpus expansion + a new saturator capability for nominal reasoning (#17).

Nominal-reasoning lever (saturator)

The EL fold now handles nominal-filler existentials (∃R.{a} / ObjectHasValue) via an opaque per-individual synthetic class (NomKey) at the lowering chokepoint, plus transitive-ABox propagation: X ⊑ ∃R.{a}, a R⁺ b (R transitive) ⟹ X ⊑ ∃R.{b}.

• Saturator-private (no tableau impact). Sound by 1:1 individual identity + transitivity gating; inverse×nominal soundness is a verified code invariant.
• wine MISSED 57 → 34 (region/colour cluster recovered), FP=0 across all 10 corpus fixtures; the 9 core parity fixtures stay MISSED=0.
• Canary nominal_transitive_abox_fold_classifies.

Corpus fixtures

• wine — W3C OWL-guide SHOIN(D), nominal/disjointness-heavy (207 value restrictions); the corpus's nominal/value-restriction stressor.
• bibtex — ORE-2015 datatype-heavy (41 DataMinCardinality + 40 DataPropertyDomain); FP=0, MISSED=0, validating Phase-D's sound under-approximation on real data.

Scoping (turning gaps into measured frontiers)

• docs/nominal-lever-scoping-2026-06-06.md — the lever + why the residual 34 (grape ≤1, sugar ∀) are tableau-grade.
• docs/corpus-datatype-2026-06-06.md — real datatypes don't drive non-redundant classification; synthetic suite remains the D4/D5 completeness test.
• docs/tableau-perf-scoping-2026-06-06.md — wine's residual is disjunction-branching interdependence (measured: 90/137 classes stall, restores=branches with precise deps). Every cheaper lever (relevance, blocking, dep-precision, completeness) is measured-out; conflict-driven nogood learning is the only remaining lever (multi-week, soundness-critical) — a deliberate future project.

Status

The 9 core corpus fixtures remain at full Konclude parity (FP=0, MISSED=0). wine sits at FP=0, MISSED=34 (sound; the residual is the documented hard-SROIQ-disjunction frontier). bibtex at full parity.

Full changelog: v0.3.3...v0.3.4

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

v0.3.2 — notgalen full Konclude parity (Phase 2e)

Highlights

notgalen MISSED 18 → 0 — full Konclude parity. The corpus completeness gap is now just SIO's 2 out-of-EL pairs. FP=0 held across the entire corpus.

Phase 2e — functional super-role witness-merge (#15)

The saturator's witness-merge rule back-propagated the merged synthetic to a subject's other functional-sub-role witnesses but skipped the merge-triggering role, wrongly assuming CR9 covered it (CR9 only lifts the original witness up to the super-role; it never pushes the merged synthetic down to the triggering sub-role). When an existential body lives on that sub-role — notgalen's Anonymous-349 ⊑ ∃hasIntrinsicPathologicalStatus.pathological, where hasIntrinsicPathologicalStatus/hasPathologicalStatus are siblings under the functional StatusAttribute — the merged filler must land there. Which sub-role triggers depends on processing order, so GALEN hit the good order (closed in 2d) while notgalen's equiv-vs-subclass structure hit the bad one, leaving 18 pairs unrecovered through Phases 2a–2d.

Fix: drop the skip. Sound by functionality of R_f (every sub-role witness coincides with the single R_f-successor carrying the full merged atom set). Verified three ways: saturator = rustdl tableau (minimal module) = Konclude (9 corpus ontologies).

Corpus gate (FP=0 throughout)

Fixture	FP	MISSED
alehif	0	0
galen	0	0
notgalen	0	18 → 0
ro	0	0
shoiq-knowledge	0	0
ore-10908-sroiq	0	0
sulo	0	0
sio	0	2 (out-of-EL)
ore-15672-shoin	0	0

Also included

• #14 — sub-tableau-caching lever scoping; corrects the stale "Lever C is dead" roadmap finding (the build-a-model premise is stale for the wedge, but the §2 reuse-soundness trap stands; the sound form already ships as the Phase 1b/1c snapshot cache).
• #13 — blocks_fired/block_eligible tableau counters + correction of the stale "blocking never fires" roadmap claim.

Full changelog: v0.3.1...v0.3.2

rustdl 0.3.1 (Python — bundled examples)

0.3.1 — 2026-06-05

Added

• Bundled example ontologies for a zero-setup, offline demo:
  rustdl.examples.pizza(), .sulo(), .sio() return local paths to
  ontologies shipped inside the wheel (gzip-compressed, decompressed
  into a per-user cache dir on first use — no network, works behind a
  proxy / air-gapped). Companion PIZZA_NS / SULO_NS / SIO_NS
  namespace constants. pizza() is the SULO-aligned ontostart pizza
  (88 classes, classifies instantly and completely).

rustdl 0.3.0

[0.3.0] — 2026-06-05

Changed

• Classification now bounds each subsumption test by default
  (pair_timeout_ms / per_pair_timeout_ms defaults to 1000 ms;
  previously unbounded). Pathological SROIQ ontologies (e.g. pizza) no
  longer hang by default. A timed-out pair is recorded as "not
  subsumed" — sound (never a false subsumption), but the result may
  be incomplete. Pass 0 for the complete, unbounded classification.
  1000 ms is the empirical knee on pizza: higher budgets buy no extra
  completeness (the remaining pairs are intractable at any reasonable
  bound) but cost proportionally more wall time.
• Incompleteness is now surfaced loudly, so a bounded run can't
  silently hand back a hierarchy missing real edges:
  • CLI rustdl classify prints a prominent ⚠ INCOMPLETE: N pair(s) exceeded the timeout … warning to stderr when any pair times out.
  • Python rustdl.classify / classify_bytes emit an
    IncompleteClassificationWarning (filterable via the warnings
    module), and the Classification object exposes .complete (bool)
    and .timed_out_pairs (int).

Added

• CLI multi-format input. rustdl <cmd> file.{owx,owl,rdf} now
  works — the reader is chosen by file extension (.owx → OWL/XML,
  .owl/.rdf → RDF/XML, .ofn/other → OWL Functional). Previously the CLI
  read OFN only; the Python bindings already auto-detected. Verified on
  the owlcs pizza ontology (RDF/XML) — 99 classes, 2 unsatisfiable
  (CheeseyVegetableTopping, IceCream), matching the canonical result.

rustdl 0.1.0

[0.1.0] — 2026-06-04

First tagged release. The engine is sound on every measured workload
and competitive (or winning) against HermiT and Konclude on most.

Added

• Sound OWL 2 DL (SROIQ) classifier with hybrid saturation+tableau
  orchestrator.
• Hypertableau wedge accelerator (default engine since 2026-05-29).
• Per-class label heuristic (Phase 7) — sound non-subsumption pruner
  via per-class wedge satisfiability.
• Cache-deadline decoupling (Phase 8) — independent deadline for the
  label-cache build, so SROIQ classes needing a few hundred ms of
  wedge satisfiability no longer get cut off at NoVerdict.
• Horn-shortcircuit fast path (Phase 2b) — Horn-fragment ontologies
  dispatch straight to saturation, skipping the per-pair tableau loop.
• ABox consistency check (Phase A1) — seven sound clash patterns:
  direct-Bot assertion, disjoint types per individual, NegOPA vs OPA
  with role-hierarchy propagation, SameAs ∩ DifferentFrom (transitive
  via union-find), Functional + two distinct witnesses,
  Asymmetric / Irreflexive violations, domain/range disjointness.
• Datatype preprocessing (D1–D5) — sound under-approximation for data
  axioms not directly supported; recognized patterns derived as TBox
  axioms (Functional + DataMin, DataMin > DataMax, DataPropertyDomain
  inference, SubDataPropertyOf transitivity,
  intersection-equivalence propagation, integer-range facet
  intersection).
• 9-corpus closure-diff regression harness — FP=0 invariant gated
  against Konclude on every commit.

Performance

Compared with the May 2026 baseline:

• GALEN: 445 s → 0.49 s (now beats Konclude — 0.24× ratio).
• notgalen: 1168 s → 0.78 s (now beats Konclude — 0.35× ratio).
• alehif: 2.28 s → 0.16 s (0.08× Konclude).
• ORE-10908: 17× Konclude → 3.1× (under the ≤5× target).
• sio-stripped: 4.3× absolute wall improvement (still 13.6×
  Konclude — out-of-EL fragment, timeout-bound; see dead-end §18).

Known limitations

• Data-axiom patterns outside the D4/D5 recognizers are silently
  dropped (sound under-approximation; missed positives possible).
• HasKey not supported (errors at parse time).
• SWRL rules silently skipped.
• Role chains of length > 2 error at parse time.
• family-class workloads need ABox saturation (open scoping target
  per dead-end §21).
• ore-15672 has a 3-class intrinsic intractability cluster — sub-model
  caching is the only known path (multi-month research-engineering;
  dead-end §18).

Dead-ends documented

21 entries in docs/hypertableau-dead-ends.md
covering soundness traps, perf optimizations that didn't materialize,
and design decisions that recon ruled out before implementation. The
ledger is the canonical record of "we tried X; here's what killed it."

Soundness contract

FP=0 vs Konclude verified on every release. The closure-diff tests in
crates/owl-dl-reasoner/tests/konclude_closure_diff.rs
are the soundness tripwire — any change that introduces a false-positive
subsumption fails CI.