Fix Datalog grounding projection: instance-specific defeaters, full provenance, fresh rule names

[ctoth]

Three fixes to the Gunray Datalog-to-ASPIC+ projection in structured/aspic/datalog_grounding.py. Each issue has its own commit with a failing regression test and a valid neighboring control.

• Grounded named defeater attacks every rule substitution instead of its matching instance #66: a named defeater ~r(t...) matched every ground instance of rule r and ignored its arguments, so ~birds_fly(a) also undercut birds_fly(b). Diller et al. 2025 ground each instance r-theta as its own rule. The defeater's arguments are now compared with the target instance's substitution values, in Gunray's variable order (sorted by variable name). A nullary ~r still names every instance. Convention to review: with more than one variable, the positions follow that sorted order.
• Datalog projection loses source provenance when distinct strict rules ground identically #67: two authored strict rules that ground to the same ASPIC+ Rule overwrote each other in the Rule-keyed origin map, so source_to_ground_rules dropped s1. The source-to-ground relation (which superiority projection also uses) is now built from every (rule, origin) pair. rule_origins still holds one origin per rule; it is now deterministic, keeping the first authored origin instead of the last.
• Generated Datalog rule names collide with authored predicates and introduce unintended undercuts #68: the generated names gr{i} and uc{i} were not reserved against the authored language. Because rule names are literals n(r) that undercuts target (Diller et al. 2025, Def 3), an unrelated fact ~gr0 undercut the first rule. Every authored predicate is now reserved, and a generated name gets a numeric suffix until it is fresh. Names that don't collide stay as gr0/uc0.

Gates:

• pytest (tree before the final merge of main): 3287 passed, 7 skipped, 1 xfailed, 1 deselected.
• The deselected test is tests/structured/aspic/test_aspic.py::TestAttackProperties::test_rebutting_targets_defeasible_conclusions. It hangs for more than 600s in compute_attacks. The file is unchanged here and the hang is reported separately.
• After merging current main: tests/structured/aspic gives 152 passed, 1 deselected. CI covers the full suite on the final tree.
• Static checks: pyright src reports 0 errors. lint-imports reports 2 kept, 0 broken. ruff check and ruff format --check pass on the changed files.

Closes #66
Closes #67
Closes #68

🤖 Generated with Claude Code

https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg

[ctoth]

Rework of #66: named-defeater arguments now bind variables in first-appearance order

Per the maintainer's decision on #66, a named defeater ~r(t1, ..., tn) binds t1..tn to rule r's variables in first-appearance order: the head's terms left to right, then each body literal left to right, default-negated ones included. Before this change the PR matched against Gunray's substitution, which is sorted alphabetically. For rel(Y, A) :- pair(Y, A) that meant ~r(a, b) undercut the instance Y = b, A = a, the opposite of the intended one.

Commit 1226159:

• rule_variable_orders(theory) (new): maps each rule id, including presumptions, to its variables in first-appearance order. It reads the order from the rule text with Gunray's own atom parser, so Gunray's alphabetically sorted substitution is not used for ordering.
• ground_defeasible_theory computes these orders and passes them to grounding_inspection_to_aspic through the new keyword argument rule_variable_orders.
• Bare inspection with no orders supplied: a GroundingInspection has no rule text, so the order can't be recovered from it. In that case a named defeater that has arguments raises ValueError rather than guessing an order. Nullary ~r, which names every instance of r, doesn't need the order and works as before.
• The convention is documented in the docstrings of rule_variable_orders, grounding_inspection_to_aspic and _defeater_targets.

Regression tests in tests/structured/aspic/test_datalog_grounding.py:

• rel(Y, A) :- pair(Y, A): ~r(a, b) undercuts Y = a, A = b. rel(a, b) is not accepted and rel(b, a) is. This failed before the fix.
• ok(Y) :- pair(Y, A): a body-only variable comes after the head's variables, giving order (Y, A). This failed before the fix.
• Control rel(A, Y), where the alphabetical and first-appearance orders coincide.
• A bare inspection raises without rule_variable_orders and gives the correct target when the orders are supplied. This failed before the fix.

The branch has also been merged with main 6441acd, which includes #99's Def 14 core semantics change.

Gates on 1226159:

• uv run pyright src: 0 errors
• uv run lint-imports: 2 kept, 0 broken
• ruff check and ruff format --check on the changed files: clean
• tests/structured/aspic: 168 passed
• Full suite, uv run pytest -q --timeout=600: 3445 passed, 7 skipped, 1 xfailed in 370.70s