Implement prp-spo2 (owl:propertyChainAxiom), general n-hop, behind an opt-in feature

[styk-tv]

Implements OWL 2 RL rule prp-spo2 (owl:propertyChainAxiom) for chains of arbitrary length,
behind an opt-in Cargo feature. The default build is unchanged.

Closes #23.

Why

The rule was never implemented, so materialization reported success and derived nothing for chain
axioms — a caller could not distinguish fired from ignored without asserting the expected
triple and probing for it. The rule table already recorded this honestly as no; this changes the
answer rather than the documentation.

Design

The normative rule is a schema over chain length — LIST[?x, ?p1, ..., ?pn] with n ≥ 1 — so it
cannot be written as a fixed-arity join. Rather than unrolling each list into a per-axiom join,
the chain is encoded structurally and the existing semi-naive fixpoint walks it:

(base)  chain(L,u,v) :- first(L,p), rest(L,nil),  T(u,p,v)
(step)  chain(L,u,v) :- first(L,p), rest(L,R),    T(u,p,w), chain(R,w,v)
(emit)  T(u,p,v)     :- T(p, owl:propertyChainAxiom, L), chain(L,u,v)

Consequences worth noting:

• Arity is unbounded — the recursion descends the list, so every chain length shares one code
  path and no per-length specialisation exists.
• The step rule needs no R != nil guard. rdf:nil carries no rdf:first, so chain(nil,_,_)
  is empty and the join contributes nothing.
• Chains compose with the rest of the rule set. emit writes into all_triples_input, so a hop
  may be supplied by an inferred triple (inverseOf, subPropertyOf, another chain) — which the
  fixpoint semantics requires and a pre-pass could not see.
• Structure sharing is free — axioms with a common list suffix share chain tuples.

Why DisjointSets is not reused

The existing list reader behind cls-int/cls-uni unions every cell of a list into one disjoint
set and collects members by iterating a HashMap, so member order is nondeterministic between
runs. That is immaterial for intersection and union, which are sets. It is the entire meaning of a
chain: hasParent ∘ hasBrother is not hasBrother ∘ hasParent. An implementation routed through
it would be silently and unreproducibly wrong, so the rule reads rdf:first/rdf:rest directly.
There is a test that fails loudly for that mistake.

Cost when unused

A reachability gate restricts the chain relation to cells an axiom actually references, so
intersectionOf/unionOf/oneOf lists never enter it. On graphs that declare no chains the
relations stay empty and semi-naive evaluation makes the rule near-free.

Tests

Grounded in the W3C OWL 2 test suite rather than fixtures written to match the implementation.
Three published cases carry test:profile RL and bind a rules engine:

Test	Entailment
New-Feature-ObjectPropertyChain-001	hasMother ∘ hasSister ⊑ hasAunt → Stewie hasAunt Carol
New-Feature-ObjectPropertyChain-BJP-003	p ← [p,q], a p b, b q c → a p c
New-Feature-ObjectPropertyChain-BJP-004	must not entail p a owl:TransitiveProperty

BJP-003 is the sharp one — the chain head occurs inside its own chain, so derived triples
re-enter the fixpoint.

Two published cases are deliberately excluded: chain2trans1 and BJP-002 both conclude an
axiom rather than an assertion, which the RL/RDF rule set is knowingly incomplete for. They are
documented as excluded in the test module so neither is later chased as a bug nor counted as
conformance the rule set does not grant.

On proving n-hop: every property-chain entailment case in the published corpus uses a
two-element chain, so conformance alone cannot establish generality. An arity sweep over n ∈ 1..8,
paired with a tightness sweep asserting an (n−1)-hop path derives nothing, carries that claim
instead. Also covered: order significance, length-1 equivalence to subPropertyOf, a hop supplied
by inference, shared list suffixes, self-chain closure, the reachability gate, and cyclic
rdf:rest termination.

The Python binding is covered too, since the engine tests would not catch a break in the pyo3
layer where a working rule can still surface nothing.

Isolation

cargo test -p reasonable --features prp-spo2      # opt in
cargo test -p reasonable                          # default: rule and tests absent

The feature follows the structure of the existing rdf-12 feature — same comment form, same
strictly additive when off contract, same #[cfg(feature = ...)] gating.

Default cargo test --workspace	94 passed, 0 failed — unchanged
With --features prp-spo2	107 passed, 0 failed
New warnings in the default build	none

The CI addition is one step in the existing job, reusing the warm release target so only
reasonable recompiles — a few seconds, versus minutes for a second job. The Python extension
under test is built by uv through the PEP517 backend, which takes features from
[tool.maturin] rather than from the maturin build step, so MATURIN_PEP517_ARGS is the only
way to reach it; release wheels come from builds.yml and are unaffected.

Whether the rule should later become a default feature is your call — the flag is what makes it
safe to land now.