Follow Modgil & Prakken 2018 Def 14 on mixed attack/defeat frameworks

[ctoth]

Implements the revised contract in #90: Modgil & Prakken 2018, Def 14, on mixed attack/defeat frameworks. Conflict-freeness is checked on attacks; defense and admissibility on defeats.

Core semantics (core/dung.py)

• Grounded: grounded_extension now returns the least complete extension. It computes the least fixed point of the defeat-based characteristic function, which is contained in every complete extension. If that set is conflict-free on attacks, it is the least complete extension. If it is not, no complete extension exists and the function raises ValueError. The new grounded_extensions() and extensions_for(..., "grounded") return () in that case instead, matching how complete and stable report no extensions.
• Complete and stable: already matched Def 14 (defeat-based labellings filtered by attack conflict-freeness), so they are unchanged.
• Preferred on mixed frameworks: preferred is the maximal Def 14 admissible sets. It is now computed by a pruned depth-first search (_mixed_preferred_search) instead of enumerating every subset.
• Operational contract (AGENTS.md): two 40-argument mixed fixtures, a set of failed-rebuttal pairs and a set of isolated arguments plus one failed-rebuttal pair, finish in 81 search nodes each (2N+1). The test bounds node count at 4N², and a monkeypatch makes any subset enumeration fail the test. Before this change the same call enumerated 2^40 subsets.

Solver layer (pre-existing Def 14 violations)

On mixed frameworks where some attack is a defeat in neither direction, the solver layer returned wrong results. It returned {a, c} although a attacks c, and it answered skeptical preferred acceptance with True where the answer is False. There were three causes:

• the grounded reduct fixed the defeat-based least fixed point as IN;
• the SCC recursion over defeats ignored attacks that cross SCC boundaries;
• the SAT kernels and preferred shortcuts assumed preferred = maximal complete.

The new attacks_resolved_by_defeats(framework) returns True when every attack is a defeat in at least one direction. It is used as a gate in several places:

• simplify_af applies the grounded reduct only when it holds.
• scc_extensions falls back to the flat Def 14 enumeration when it doesn't.
• The SAT single-extension and acceptance paths skip the dedicated kernels and the cone path when it doesn't.
• af_sat's preferred-skeptical shortcuts after the self-attack check run only when it holds.

When it holds (including every single-relation framework), the least fixed point is conflict-free on attacks and contained in every preferred extension, so those optimisations stay in place.

A random differential over 250 frameworks with 2–5 arguments compared native, sat and auto backends for enumeration, single extension, and credulous/skeptical acceptance. All agree with core Def 14 after the fix.

Audit of grounded_extension callers

• Converted to grounded_extensions (return () when there is no complete extension): extensions_for, which covers probabilistic worlds, dynamics, CAF and partial AF; semantics._dung_extensions; solver._dung_extensions; sat_encoding; the materialized ASPIC extensions; and ICCMA grounded witness validation, where a witness for a framework with no grounded extension is now rejected.
• Unaffected (they only ever build single-relation frameworks): bipolar_grounded_extension, ranking/weighted, and the af_sat acyclic fragment, which was already gated.
• Guarded: the af_sat preferred-skeptical shortcut and simplify_af.
• Propagate the documented ValueError (public grounded-only APIs on user frameworks): solve_aspic_grounded (docstring updated), cayrol_2014_classify_grounded_argument_addition, and gradual/sensitivity.
• A probabilistic test covers a sampled world with no grounded extension: that world accepts nothing, and exact acceptance is {a: 0, b: 0.5}.

Tests

New file tests/core/test_def14_mixed_semantics.py:

• The issue's reproduction: grounded raises ValueError; complete and stable are []; preferred is [{a}, {b}].
• The ASPIC+ control from the issue comment: premises p < q, strict rules p -> ~q and q -> ~p, closed under transposition. Grounded exists, is conflict-free on attacks and is the least complete extension; preferred equals the maximal complete extensions.
• Property on pairwise-well-formed mixed frameworks, where every attack is a defeat in at least one direction: grounded is complete and least, preferred equals the maximal complete extensions, and every extension is conflict-free on attacks.
• Property on arbitrary mixed frameworks: preferred equals brute-force maximal admissible, and grounded is the least complete extension or raises.
• Property: solver backends agree with core on arbitrary mixed frameworks.
• Differential on single-relation frameworks against tests/core/pre_def14_reference.py, a verbatim copy of the pre-change implementation.

Scope note on the property. The acceptance criterion "preferred equals the maximal complete extensions" is false for arbitrary mixed frameworks that do have a complete extension. Exhaustive checking over 3-argument frameworks found 540 counterexamples out of 10,664. One example: attacks {(a,b), (a,c), (b,a)} with defeats {(a,b), (b,a)} gives preferred {a}, {b,c} but maximal complete {b,c}. The criterion holds when every attack is a defeat in some direction: 0 counterexamples exhaustively at 3 arguments and in 4,000 random frameworks each at 4 and 5 arguments. So that property test uses such frameworks, and the separate arbitrary-framework property tests preferred as maximal admissible.

Two existing tests updated. Both asserted the withdrawn behaviour that grounded ignores attacks and returns {A, B}. They now expect ValueError, and one gains a failed-rebuttal control:

• tests/core/test_dung.py
• tests/core/test_bipolar_argumentation.py

Closes #90

🤖 Generated with Claude Code

https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg