Skip to content

structured-argumentation.md

Latest commit

 

History

History
308 lines (205 loc) · 21.4 KB

structured-argumentation.md

File metadata and controls

308 lines (205 loc) · 21.4 KB

Structured Argumentation (ASPIC+)

propstore implements ASPIC+ structured argumentation following Modgil & Prakken (2018). Where flat Dung AFs treat arguments and defeats as atomic primitives, ASPIC+ decomposes arguments into their internal inference structure: premises, inference rules, and sub-arguments. This makes the reason for a conflict visible and allows preference-based defeat filtering that considers the quality of each reasoning step.

For scientific claims, this matters because a claim supported by a strict logical derivation from established facts should not be treated the same as a claim supported by a single defeasible observation. ASPIC+ captures this distinction formally.

From Claims to Arguments

The Translation Pipeline (T1-T7)

The bridge package (propstore.aspic_bridge) translates propstore's claim graph into formal ASPIC+ types via seven translation steps. Each step corresponds to a definition in Modgil & Prakken (2018).

T1: Claims become literals (Def 1, p.8)

Each active claim becomes a Literal(atom=claim_id, negated=False). The atom is the claim ID, not the concept ID, because multiple claims can bind to the same concept with different values. The logical language L is closed under contrariness: for every literal, its complement is also in L.

propstore/aspic_bridge/translate.py — claims_to_literals()

T2: Justifications become inference rules (Def 2, p.8)

Each canonical justification becomes a Rule mapping premise literals to a conclusion literal. reported_claim justifications are skipped (they produce premises via T4 instead). The rule kind depends on rule_strength:

  • "strict" produces a strict rule (no name, cannot be undercut)
  • "defeasible" produces a defeasible rule (named by justification ID, can be undercut per Def 8c)

Rules where premise or conclusion literals are missing (because the corresponding claim is inactive) are silently dropped.

propstore/aspic_bridge/translate.py — justifications_to_rules()

T3: Stances become contrariness relations (Def 2, p.8)

Stances between claims define the contrariness function:

  • rebuts/contradicts become contradictory pairs (symmetric — both directions added)
  • supersedes/undermines become contrary pairs (asymmetric — the source is contrary to the target, but not vice versa)
  • undercuts target the rule-name literal of matching defeasible rules, following Pollock (1987) Def 2.5

This distinction matters for defeat: contradictory attacks are filtered through preferences (either side can win), while contrary attacks always defeat (the attacker wins regardless of preference).

propstore/aspic_bridge/translate.py — stances_to_contrariness()

T4: Claims partitioned into knowledge base (Def 4, p.9)

Claims with reported_claim justifications become premises in the knowledge base K = K_n U K_p:

  • premise_kind="necessary" places the claim in K_n (axioms — firm, cannot be attacked)
  • All other premise kinds place the claim in K_p (ordinary premises — can be undermined)

propstore/aspic_bridge/translate.py — claims_to_kb()

T5: Preference configuration (Defs 19-22, p.21-22)

Each claim carries a metadata_strength_vector. Component-wise Pareto domination between vectors defines the current heuristic premise ordering: claim A is preferred over claim B iff A dominates B on every component. Transitive closure is applied to the resulting relation.

Rule ordering is populated from authored rule-file superiority data. Rule-file pairs are authored as (superior_rule_id, inferior_rule_id), validated and closed as a strict partial order, then projected into ASPIC+ PreferenceConfig.rule_order as (weaker_rule, stronger_rule) pairs over grounded defeasible rules.

propstore/aspic_bridge/translate.py — build_preference_config()

T6: Full CSAF assembly (Def 12, p.13)

The orchestrator calls T1-T5 in sequence, then:

  1. Builds the language L from all literals and their contraries
  2. Applies transposition closure to strict rules (Def 12)
  3. Rebuilds L to include any new literals generated by transposition
  4. Calls build_arguments(), compute_attacks(), compute_defeats()
  5. Constructs the corresponding Dung AF with deterministic string IDs (arg_0, arg_1, ...)

The result is a CSAF (Complete Structured Argumentation Framework) that bundles the argumentation system, knowledge base, preferences, arguments, attacks, defeats, and the induced Dung AF.

propstore/aspic_bridge/build.py — build_bridge_csaf()

T7: Projection back to StructuredArgument instances (Def 5)

ASPIC+ arguments are mapped back to StructuredArgument dataclasses for downstream consumption. Transposition artifacts (negated literals or atoms not matching any claim ID) are excluded from projection. Argument strength is computed as the mean of the claim strength vector. The framework's defeats and attacks are filtered to projected arguments only.

propstore/aspic_bridge/projection.py — csaf_to_projection()

Architecture

structured_projection.py              aspic_bridge/                 argumentation.aspic
  build_structured_projection() ---> build_aspic_projection()
                                       _extract_stance_rows()
                                       _extract_justifications()
                                       build_bridge_csaf()  ---------> T1: claims_to_literals()
                                         |                            T2: justifications_to_rules()
                                         |                            T3: stances_to_contrariness()
                                         |                            T4: claims_to_kb()
                                         |                            T5: build_preference_config()
                                         |                            transposition_closure()
                                         |                            build_arguments()
                                         |                            compute_attacks()
                                         |                            compute_defeats()
                                       csaf_to_projection() --------> StructuredProjection
  compute_structured_justified_arguments()
    -> grounded_extension() / preferred_extensions() / etc. (argumentation.dung)

Data flows one way: claims/stances/justifications and grounded rule priorities enter as propstore domain objects, are translated into formal ASPIC+ types, pass through argument construction and attack/defeat computation, produce a Dung AF, and exit as extensions. CKR-style contextual exceptions are integrated after ASPIC+ argument construction by adding exception-derived Dung defeats with propstore.defeasibility.apply_exception_defeats_to_csaf(...).

argumentation/src/argumentation/aspic.py is a leaf module with zero propstore imports. It implements ASPIC+ in pure logic. propstore.aspic_bridge handles all translation between propstore's claim graph and the formal engine. propstore/structured_projection.py provides the public dataclasses and thin delegation wrappers.

Argument Construction

Arguments are built recursively following Def 5 (pp.9-10) of Modgil & Prakken (2018):

  • PremiseArg (Def 5 clause 1): An argument whose conclusion is a single premise from the knowledge base. is_axiom=True for K_n members, False for K_p members. These are the leaves of the argument tree.
  • StrictArg (Def 5 clause 2): An argument built by applying a strict inference rule to the conclusions of its sub-arguments. The conclusion follows necessarily.
  • DefeasibleArg (Def 5 clause 3): An argument built by applying a defeasible inference rule. The conclusion follows tentatively and can be challenged.

The construction algorithm (argumentation/src/argumentation/aspic.py:514, build_arguments()) operates as a fixpoint:

  1. Seed with a PremiseArg for each literal in K_n and K_p
  2. Index arguments by their conclusion literal
  3. Iterate: for each rule, enumerate the Cartesian product of arguments matching each antecedent
  4. Acyclicity check (Def 7, p.11): the rule's consequent must not appear among sub-argument conclusions
  5. C-consistency filter (Def 6, p.10): only keep arguments whose premises are c-consistent (their strict closure contains no conflicting pair)

Computed properties follow Def 5 directly:

  • conc(a) — the conclusion of argument a
  • prem(a) — the set of all premises (leaves) of a
  • sub(a) — the set of all sub-arguments of a (including a itself)
  • top_rule(a) — the last inference rule applied (None for premise arguments)
  • def_rules(a) — all defeasible rules used anywhere in a
  • last_def_rules(a) — defeasible rules at the last inference step only

All property functions are cached via @functools.cache for performance.

Attack Determination

Three attack types are defined per Def 8 (p.11) of Modgil & Prakken (2018):

Undermining (Def 8a): Argument A attacks argument B on sub-argument B' if A's conclusion is contrary or contradictory to an ordinary premise of B'. This challenges the evidence that B relies on. Firm premises (from K_n) are never targeted (Def 18, p.16).

Rebutting (Def 8b): Argument A attacks argument B on sub-argument B' if A's conclusion is contrary or contradictory to the conclusion of B', and B' uses a defeasible top rule. This is a head-on clash of competing defeasible conclusions. Corresponds to Pollock (1987) Def 2.4 (p.485).

Undercutting (Def 8c): Argument A attacks argument B on sub-argument B' if A's conclusion is contrary or contradictory to the rule-name literal of a defeasible rule used in B'. This does not challenge B's conclusion directly — it challenges the applicability of B's reasoning step. Corresponds to Pollock (1987) Def 2.5 (p.485).

The implementation (argumentation/src/argumentation/aspic.py:622, compute_attacks()) pre-computes a sub-argument cache and conclusion index to avoid O(n^3) scanning.

Preference-Based Defeat

Not every attack succeeds as a defeat. Def 9 (p.12) defines when attacks become defeats:

  • Undercutting always defeats: an undercutting attack succeeds regardless of preference (Pollock 1987 Def 2.5).
  • Contrary attacks always defeat: when the contrariness is asymmetric (directional), the attacker wins regardless of preference.
  • Contradictory attacks are filtered: for symmetric conflicts (rebutting or undermining with contradictory contrariness), the attack becomes a defeat only if the attacker is NOT strictly weaker than the targeted sub-argument under the preference ordering.
  • Self-attacks always succeed: by irreflexivity of the ordering (Def 22).

Set Comparison (Def 19, p.21)

Two modes for comparing sets of rules or premises:

  • Elitist: set A is strictly less than set B iff every element of A is less than some element of B. This is the stricter standard — the entire attacking set must be outclassed.
  • Democratic: set A is strictly less than set B iff some element of A is less than some element of B. This is the more permissive standard — one weak link is enough.

argumentation/src/argumentation/aspic.py:724 — _set_strictly_less()

Last-Link Principle (Def 20, p.21)

Compare the LastDefRules sets of the attacker and target. The last defeasible rules are the ones applied at the final inference step. If both sets are empty (firm+strict arguments), fall back to comparing ordinary premises.

argumentation/src/argumentation/aspic.py:808 — _strictly_weaker() (last-link branch)

Weakest-Link Principle (Def 21, p.21)

Compare both Prem_p (ordinary premises) and DefRules (all defeasible rules) of the attacker and target. Three cases based on whether each argument is firm, strict, or neither. The weakest link in the chain determines the comparison.

argumentation/src/argumentation/aspic.py:825 — _strictly_weaker() (weakest-link branch)

Transposition Closure

Transposition closure (Def 12, p.13; Prakken 2010 Def 5.1) ensures that strict rules interact correctly with contrariness. For each strict rule A1, ..., An -> C and each antecedent index i, a transposed rule is generated: A1, ..., ~C, ..., An -> ~Ai. This process repeats until a fixpoint is reached.

Degenerate rule filtering: transposed rules with contradictory antecedent pairs are discarded (they reference Thm 14, direct consistency). After the fixpoint, an axiom consistency check verifies that no literal's strict closure contains its own contrary.

Transposition closure is required for the rationality postulates (Thms 12-15) to hold. Without it, the framework can produce inconsistent extensions — arguments that are jointly accepted but whose conclusions contradict each other under strict rules.

argumentation/src/argumentation/aspic.py:247 — transposition_closure()

Rationality Postulates

The implementation satisfies eight rationality postulates, verified by Hypothesis property-based tests over randomly generated c-SAFs:

# Postulate Paper Reference Verification
1 Sub-argument closure Thm 12 (p.18) Every extension that contains an argument also contains all its sub-arguments
2 Closure under strict rules Thm 13 (p.18) Extensions are closed under strict rule application
3 Direct consistency Thm 14 (p.18) No extension contains two arguments with conflicting conclusions
4 Indirect consistency Thm 15 (p.19) The strict closure of an extension's conclusions is also consistent
5 Firm+strict in every complete extension Def 18 (p.16) Arguments built from axioms and strict rules alone are never defeated
6 Undercutting always defeats Def 9 (p.12) Undercutting attacks succeed regardless of preference ordering
7 Attack-based conflict-free Def 14 (p.14) No argument in an extension attacks another argument in the same extension
8 Transposition closure Def 12 (p.13) Strict rules are closed under transposition (Prakken 2010 Thm 6.10)

These postulates are achieved by construction — the algorithms enforce them structurally — and verified at test time by property-based fuzzing, not runtime assertion.

tests/test_aspic.py:~2130 — TestRationalityPostulates

CLI Usage

The structured argumentation backend is available via the pks world CLI:

# Compute extensions using the ASPIC+ backend
pks world extensions --backend aspic --semantics grounded

# Preferred extensions with democratic set comparison
pks world extensions --backend aspic --semantics preferred --set-comparison democratic

pks worldline run my-worldline

Extension semantics (grounded, preferred, stable) work identically to the claim-graph backend. The difference is in how the Dung AF is constructed: the aspic backend builds it from recursive ASPIC+ arguments with formal preference defeat, rather than from flat claim-row heuristics.

Goal-Directed Query (Backward Chaining)

The exhaustive build_arguments() constructs every possible argument from the knowledge base and rules. For large claim graphs where only one claim's status matters, this is wasteful. build_arguments_for() provides goal-directed backward chaining: given a specific conclusion literal, it constructs only the arguments relevant to that conclusion.

Algorithm

The backward chaining algorithm in build_arguments_for() (argumentation/src/argumentation/aspic.py) works top-down from the goal:

  1. Base case: If the goal literal is in K_n (axioms) or K_p (premises), create a PremiseArg.
  2. Recursive case: Find all rules whose consequent matches the goal. For each rule, recursively build arguments for every antecedent. Combine sub-arguments via Cartesian product into StrictArg or DefeasibleArg.
  3. Attacker discovery (when include_attackers=True): Build arguments for contraries of the goal and of all intermediate conclusions in the goal's argument tree — including rule-name literals for undercutting. A second pass finds counter-attackers for reinstatement.
  4. Cycle detection: An in_progress set tracks literals currently being resolved. If a literal is encountered again during its own resolution, the recursion returns empty — ASPIC+ arguments are finite trees (Def 5), so cycles are not valid arguments.
  5. Depth limiting: max_depth (default 10) prevents infinite chains through long rule sequences.
  6. Memoization: Results are cached per literal within a single call, avoiding exponential blowup on diamond-shaped rule graphs.
  7. c-consistency: The same is_c_consistent() filter as forward construction is applied to every candidate argument.

The result uses the same PremiseArg/StrictArg/DefeasibleArg types as build_arguments(). The existing compute_attacks() and compute_defeats() work unchanged on the result.

References: Toni (2014) for ABA backward chaining from claims to assumptions. Besnard & Hunter (2001, Def 6.1, p.215) for argument trees rooted at a specific conclusion. Odekerken (2023) for queryable-driven stability analysis as a complementary technique.

Correctness Invariant

The fundamental correctness property: goal-directed arguments are a subset of exhaustive arguments.

build_arguments_for(system, kb, goal, include_attackers=False) ⊆ build_arguments(system, kb)

Additionally, backward chaining is complete for the goal literal: every exhaustive argument whose conclusion is the goal also appears in the goal-directed result. Together these mean the backward result contains exactly the exhaustive arguments concluding the goal, plus their sub-arguments.

These properties are verified by Hypothesis property-based tests over randomly generated ASPIC+ systems in the external argumentation package.

Bridge-Level Integration: query_claim()

query_claim() in propstore.aspic_bridge provides the claim-graph-level integration. It runs the same T1-T5 translation pipeline as build_bridge_csaf(), then replaces the exhaustive build_arguments() with build_arguments_for() for the queried claim.

from propstore.aspic_bridge import query_claim

result = query_claim(
    claim_id="claim_42",
    active_claims=active_claims,
    justifications=justifications,
    stances=stances,
)

# Result fields:
result.claim_id          # "claim_42"
result.goal              # Literal(atom="claim_42", negated=False)
result.arguments_for     # frozenset of arguments concluding the goal
result.arguments_against # frozenset of arguments concluding contraries
result.attacks           # frozenset of Attack objects among relevant arguments
result.defeats           # frozenset of (attacker, target) pairs after preferences

ClaimQueryResult partitions the relevant arguments into arguments_for (conclusion matches the goal) and arguments_against (all other relevant arguments, including attackers). Attacks and defeats are computed on this focused subset using the same compute_attacks() / compute_defeats() functions as the full CSAF path.

Relationship to ATMS

Backward chaining and the ATMS backend answer different questions:

  • Backward chaining answers "what arguments support or attack this specific claim?" — it constructs the local argument structure.
  • ATMS stability/relevance answers "will this claim's status change under future observations?" — it tracks assumption dependencies.

They are complementary. Use query_claim() to understand the argumentation structure around a claim. Use pks world atms stability and pks world atms relevance to understand how robust that status is under uncertainty.

Architecture

query_claim()  ──────────────────────> T1-T5 translation (same as build_bridge_csaf)
  │                                    │
  └── build_arguments_for(goal) ◄──────┘  (replaces build_arguments)
        │
        ├── _build_backward(goal, 0)        backward chaining from goal
        ├── _contraries_of(goal, ...)       find contrary literals
        ├── _build_backward(contraries, 0)  attacker discovery
        └── _build_backward(counter, 0)     counter-attacker discovery
        │
        ▼
      compute_attacks() / compute_defeats()  (unchanged)
        │
        ▼
      ClaimQueryResult { arguments_for, arguments_against, attacks, defeats }

Known Limitations

  • Premise ordering is metadata-derived: authored rule priorities now populate rule_order, but ordinary-premise ordering still comes from metadata_strength_vector() rather than an authored premise-priority surface.
  • K_a partition missing: Odekerken (2023) defines assumption premises as a third knowledge base partition K_a. This is not yet implemented.

References

  • Modgil, S. & Prakken, H. (2018). A general account of argumentation with preferences. Artificial Intelligence, 248, 51-104.
  • Prakken, H. (2010). An abstract framework for argumentation with structured arguments. Argument & Computation, 1(2), 93-124.
  • Pollock, J. L. (1987). Defeasible reasoning. Cognitive Science, 11(4), 481-518.
  • Dung, P. M. (1995). On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence, 77(2), 321-357.
  • Odekerken, D. (2023). ASPIC+ with incomplete information. Argument & Computation.