derive-pipeline-is-exhaustive-and-terminating

OUT derived (depth 1)

The derive pipeline supports exhaustive exploration mode while guaranteeing termination: `--exhaust` enables automatic application of all discovered proposals, and depth-based cycle detection with pre-recursion memoization prevents infinite loops even when justification chains are cyclic.

Summary

The derive pipeline can automatically discover and apply all possible new conclusions in a loop without getting stuck in an infinite cycle. It does this by letting users run exhaustive derivation with a single flag, and by catching circular reasoning chains before they cause runaway recursion. This belief is currently marked OUT, meaning one or both of its supporting claims have been retracted, so this guarantee may not hold right now.

Justifications

SL — Depth-1 — completeness mode (exhaust) and termination guarantee (cycle guard) together yield the strongest usable exploration strategy: explore everything, stop safely

Antecedents (all must be IN):

  • exhaust-implies-auto — In `_derive_one_round`, proposals are auto-applied when either `args.auto` or `args.exhaust` is true; the `--exhaust` flag does not require the user to also pass `--auto`.
  • derive-depth-cycle-guard — `_get_depth` sets `memo[node_id] = 0` before recursing to prevent infinite recursion on cyclic justification chains; cycles resolve to depth 0

Dependents

These beliefs depend on this one:

Details