fix(query): correct explain/what-if/why-not diagnostics for variable rules #35

Merged

anuna-02 merged 0 commits from refs/pull/35/head into main

2026-07-15 02:37:36 +00:00

anuna-02 commented

2026-07-15 02:04:56 +00:00

(Migrated from codeberg.org)

Three user-visible correctness gaps in the query/explanation diagnostics,
surfaced by an elephant-3000 agent tour. All three are specific to theories
with variable-headed rules — spindle's own query tests only exercised
ground rules, so the gaps were untested.

Fixes

explanation: explain contradicted itself on a proven defeasible conclusion.
A conclusion derived by a variable rule carries a grounded instance label
(pn_1) that is absent from the template theory, so explain_inner's
theory.get_rule(label) missed and no proof tree was built. The
natural-language formatter then printed a self-contradiction:

Explanation for +d ~flies(tweety)
This was proven using defeasible rules and was not defeated by any conflicting rule.

No derivation found.

resolve_rule now recovers the template from the grounded label
({template}_{instance}), so the proof tree builds; the formatter's
positive-but-no-tree fallback is also made non-contradictory.

what_if: newly_provable listed a literal once per derivation path.
new_conclusions mapped the modified conclusion set to literals with no
dedup, so a literal proven at two positive tags (+D and +d) appeared
twice. newly_provable is a set of literals — deduplicated on the same
injective canonical key already used for the baseline.

why_not: reported the misleading "no rule concludes …" for variable rules.
The deriving-rule, missing-premise, and attacker scans iterated the template
rules while conclusions are ground, and the family matchers compare
argument values — so a ground query (flies opus) never matched a template
head (flies ?x), found_rule stayed false, and blocked_by came back empty.
why_not_with_conclusions now reasons over the grounded rules
(ground_theory), so head / body-premise / attacker matching is consistent
with the conclusion set. Superiority still resolves via template_label().
The ambiguity case now reports the real contradiction, e.g.
rule r1_1: Contradicted by r2_2, instead of an empty result.

Tests

Each fix ships a regression test confirmed to fail without it:

explain_builds_proof_tree_for_grounded_variable_rule
what_if_deduplicates_new_conclusions
why_not_finds_variable_headed_rules_in_ambiguity

Full workspace suite: 2077 passed, 0 failed, 28 ignored. spindle-core
clippy clean (the one pre-existing warning in reason/defeasible.rs is
untouched).

🤖 Generated with Claude Code

Three user-visible correctness gaps in the query/explanation diagnostics, surfaced by an elephant-3000 agent tour. All three are specific to theories with **variable-headed rules** — spindle's own query tests only exercised ground rules, so the gaps were untested. ## Fixes **`explanation`: `explain` contradicted itself on a proven defeasible conclusion.** A conclusion derived by a variable rule carries a grounded instance label (`pn_1`) that is absent from the template theory, so `explain_inner`'s `theory.get_rule(label)` missed and no proof tree was built. The natural-language formatter then printed a self-contradiction: ``` Explanation for +d ~flies(tweety) This was proven using defeasible rules and was not defeated by any conflicting rule. No derivation found. ``` `resolve_rule` now recovers the template from the grounded label (`{template}_{instance}`), so the proof tree builds; the formatter's positive-but-no-tree fallback is also made non-contradictory. **`what_if`: `newly_provable` listed a literal once per derivation path.** `new_conclusions` mapped the modified conclusion set to literals with no dedup, so a literal proven at two positive tags (`+D` and `+d`) appeared twice. `newly_provable` is a set of literals — deduplicated on the same injective canonical key already used for the baseline. **`why_not`: reported the misleading "no rule concludes …" for variable rules.** The deriving-rule, missing-premise, and attacker scans iterated the **template** rules while `conclusions` are **ground**, and the family matchers compare argument values — so a ground query `(flies opus)` never matched a template head `(flies ?x)`, `found_rule` stayed false, and `blocked_by` came back empty. `why_not_with_conclusions` now reasons over the grounded rules (`ground_theory`), so head / body-premise / attacker matching is consistent with the conclusion set. Superiority still resolves via `template_label()`. The ambiguity case now reports the real contradiction, e.g. `rule r1_1: Contradicted by r2_2`, instead of an empty result. ## Tests Each fix ships a regression test confirmed to fail without it: - `explain_builds_proof_tree_for_grounded_variable_rule` - `what_if_deduplicates_new_conclusions` - `why_not_finds_variable_headed_rules_in_ambiguity` Full workspace suite: **2077 passed, 0 failed, 28 ignored**. `spindle-core` clippy clean (the one pre-existing warning in `reason/defeasible.rs` is untouched). 🤖 Generated with [Claude Code](https://claude.com/claude-code)

No reviewers

No labels

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

anuna-research/spindle-rust!35

No description provided.

Rows
Columns