Metadata-Version: 2.4
Name: formal-argumentation
Version: 0.3.0
Summary: Finite formal argumentation frameworks and semantics: Dung, ASPIC+, bipolar, partial, and revision
Project-URL: Homepage, https://github.com/ctoth/argumentation
Project-URL: Repository, https://github.com/ctoth/argumentation
Project-URL: Issues, https://github.com/ctoth/argumentation/issues
Author: ctoth
Keywords: abstract-argumentation,argument-labelling,argumentation,aspic,aspic-plus,belief-revision,bipolar-argumentation,df-quad,dung,formal-argumentation,gradual-semantics,iccma,incomplete-argumentation,knowledge-representation,monte-carlo,nonmonotonic-reasoning,partial-argumentation,probabilistic-argumentation,qbaf,ranking-semantics,sat,tree-decomposition,z3
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Typing :: Typed
Requires-Python: >=3.11
Provides-Extra: asp
Requires-Dist: clingo>=5.7; extra == 'asp'
Provides-Extra: grounding
Requires-Dist: gunray; extra == 'grounding'
Provides-Extra: sat
Requires-Dist: python-sat>=1.8.dev13; extra == 'sat'
Provides-Extra: z3
Requires-Dist: z3-solver>=4.12; extra == 'z3'
Description-Content-Type: text/markdown

# argumentation

A finite, citation-anchored Python library for formal argumentation.

`argumentation` is a small, pure-Python kernel that implements the standard
objects and algorithms of computational argumentation theory: Dung abstract
argumentation, ASPIC+ structured argumentation, ABA / ABA+, abstract
dialectical frameworks, bipolar and value-based AFs, partial AFs with
completion-based reasoning, AF revision, probabilistic and gradual semantics,
ranking and weighted services, and ASP encodings of the standard extension
semantics plus a Z3-backed AF SAT kernel. Every algorithm cites the paper, definition, and (where
useful) page that fixes its behaviour. The pure-Python implementations are the
reference for package algorithms; solver adapters are typed boundaries around
external tools.

The package is organized into layered subpackages — `core`,
`structured.aspic`, `structured.aba`, `frameworks`, `gradual`, `ranking`,
`probabilistic`, `dynamics`, `interop`, `solving`, `solver_adapters` — with an
`import-linter`-enforced import DAG. See `docs/architecture.md` for the layer
contract and [`CHANGELOG.md`](CHANGELOG.md) for the 0.3.0 breaking-change
details (all import paths changed in 0.3.0).

## Contents

- [Install](#install)
- [Quick start](#quick-start)
- [Surface tour](#surface-tour)
- [Documentation map](#documentation-map)
- [Core: Dung, labellings, preferences, dispatch](#core)
- [Structured: ASPIC+, ABA, accrual](#structured)
- [Quantitative and bipolar: ranking, weighted, gradual, DF-QuAD](#quantitative-and-bipolar)
- [Probabilistic and epistemic](#probabilistic-and-epistemic)
- [Specialized frameworks: ADF, SETAF, CAF, VAF, practical reasoning](#specialized-frameworks)
- [Dynamics, revision, enforcement](#dynamics-revision-enforcement)
- [Encoding and interop: ICCMA, SAT, datalog grounding](#encoding-and-interop)
- [Solver surfaces](#solver-surfaces)
- [`iccma-cli`](#iccma-cli)
- [Design](#design)
- [Non-goals](#non-goals)
- [Development](#development)

## Install

```powershell
uv add formal-argumentation
```

The PyPI distribution name is `formal-argumentation`; the import name is
`argumentation`. Requires Python 3.11+. The core kernel has no runtime
dependencies.

Optional extras unlock specific surfaces:

| Extra | What it unlocks | Pulls |
|---|---|---|
| `[z3]` | `argumentation.probabilistic.epistemic` linear atomic constraint satisfiability / entailment and the `argumentation.solving.af_sat` SAT backend | `z3-solver>=4.12` |
| `[asp]` | Clingo-backed ABA solving (`argumentation.structured.aba.aba_asp`) and ASP backends in `argumentation.structured.aspic.aspic_encoding` | `clingo>=5.7` |
| `[grounding]` | Datalog-style grounding of defeasible theories into ASPIC+ (`argumentation.structured.aspic.datalog_grounding`) | [`gunray`](https://github.com/ctoth/gunray) (sourced from git, not PyPI) |

```powershell
uv add "formal-argumentation[z3]"
uv add "formal-argumentation[asp]"
```

The `[grounding]` extra requires resolving `gunray` from its git URL; see
`pyproject.toml` for the source declaration.

## Quick start

A Dung framework, three semantics, in eight lines:

```python
from argumentation.core.dung import (
    ArgumentationFramework,
    grounded_extension,
    preferred_extensions,
    stable_extensions,
)

af = ArgumentationFramework(
    arguments=frozenset({"a", "b", "c", "d"}),
    defeats=frozenset({("a", "b"), ("b", "c"), ("c", "d"), ("d", "a")}),
)

grounded_extension(af)     # frozenset()
preferred_extensions(af)   # [frozenset({"a", "c"}), frozenset({"b", "d"})]
stable_extensions(af)      # [frozenset({"a", "c"}), frozenset({"b", "d"})]
```

Frameworks are immutable, equality is structural, and there is no global
state. The same dataclass flows into the labelling bridge, generic semantics
dispatch, the SAT encoder, the probabilistic kernel, and the ICCMA writer.

## Surface tour

| Family | Subpackage | One-line summary |
|---|---|---|
| [Core](#core) | `core.dung`, `core.labelling`, `core.preference`, `semantics` | Dung 1995 + Caminada/Gaggl-Woltran/DMT extensions, three-valued labellings, preference primitives, generic dispatch |
| [Structured](#structured) | `structured.aspic.*`, `structured.aba.*`, `core.accrual` | ASPIC+ argument construction, ASP-style encoding, incomplete-premise reasoning, flat ABA / ABA+ with native, ASP, and SAT backends |
| [Quantitative and bipolar](#quantitative-and-bipolar) | `core.bipolar`, `gradual.*`, `ranking.*` | Cayrol bipolar, Potyka quadratic energy + Shapley impacts, Categoriser/Burden rankings, Dunne-style weighted, DF-QuAD, Gabbay equational, zero-sum game strengths |
| [Probabilistic and epistemic](#probabilistic-and-epistemic) | `probabilistic.probabilistic`, `probabilistic.epistemic` | PrAFs over seven strategies (Monte Carlo, exact enum, tree-decomp DP, paper-faithful Popescu-Wallner, DF-QuAD), epistemic graphs with Z3-backed constraints |
| [Specialized frameworks](#specialized-frameworks) | `frameworks.*` | Brewka-Woltran ADFs with typed acceptance ASTs, collective-attack SETAFs, claim-augmented AFs, Bench-Capon value-based, Atkinson AATS practical arguments |
| [Dynamics and revision](#dynamics-revision-enforcement) | `frameworks.partial_af`, `dynamics.*` | Partial AFs and completions, Baumann/Diller revision, dynamic update streams, minimal-change enforcement, k-stable approximation |
| [Encoding and interop](#encoding-and-interop) | `interop.iccma`, `solving.sat_encoding`, `solving.af_sat`, `structured.aspic.datalog_grounding`, `gradual.llm_surface` | ICCMA AF/ADF/ABA exchange, in-package SAT-extension routing, incremental AF SAT kernel, Gunray-grounded ASPIC+, QBAF adapter for argumentative LLM pipelines |
| [Solver orchestration](#solver-surfaces) | `solving.*`, `solver_adapters/` | Typed solver tasks, capability detection, `backend="auto"` routing, ICCMA / clingo subprocess adapters |

`docs/architecture.md` covers the layered kernel-and-adapters design in depth.
`docs/backends.md` documents the backend selection rule.

## Documentation map

The package docs are organized around the questions users and contributors
actually need answered:

| Question | Doc |
|---|---|
| What is the package, and how do I use the main surfaces? | this README |
| Are there small current examples for copy-paste use? | [`docs/examples.md`](docs/examples.md) |
| Where does a module live, and what may it import? | [`docs/architecture.md`](docs/architecture.md) |
| Which backend string means what? | [`docs/backends.md`](docs/backends.md) |
| What is intentionally incomplete or out of scope? | [`docs/gaps.md`](docs/gaps.md) |
| How do I prepare ICCMA data and run local benchmark slices? | [`docs/iccma-data.md`](docs/iccma-data.md), [`docs/iccma-2025-data.md`](docs/iccma-2025-data.md) |
| How should solver-performance research be recorded? | [`docs/performance-research.md`](docs/performance-research.md) |

[`docs/index.md`](docs/index.md) is the short landing page for the whole docs
folder.

## Core

`argumentation.core.dung` provides the four canonical Dung semantics —
`grounded_extension`, `complete_extensions`, `preferred_extensions`,
`stable_extensions` — together with `naive_extensions`,
`semi_stable_extensions` (Caminada 2011), `stage_extensions`,
`cf2_extensions` (Gaggl & Woltran 2013), `stage2_extensions`,
`eager_extension`, `ideal_extension` (Dung, Mancarella & Toni 2007), and
prudent-semantics helpers. The `ArgumentationFramework` dataclass tracks both
a pre-preference `attacks` relation (used by conflict-freeness) and the
post-preference `defeats` relation (used by defence), following Modgil &
Prakken (2018) Def 14.

`argumentation.core.labelling` exposes the three-valued IN / OUT / UNDEC
labelling and a bridge from extensions to labellings:

```python
from argumentation.core.labelling import Labelling

labelling = Labelling.from_extension(af, frozenset({"a", "c"}))
labelling.in_arguments         # frozenset({"a", "c"})
labelling.out_arguments        # frozenset({"b", "d"})
labelling.undecided_arguments  # frozenset()
labelling.range                # in ∪ out
```

`argumentation.core.preference` provides preference primitives used across
ASPIC+ and revision: `strict_partial_order_closure` (transitive closure with
cycle and reflexivity rejection), `strictly_weaker` (elitist and democratic
comparisons over numeric strength vectors, Modgil & Prakken Def 19), and
`defeat_holds` (generic attack-to-defeat resolution).

`argumentation.semantics` is a small set-returning dispatcher for callers that
work across framework families:

```python
from argumentation.semantics import accepted_arguments, extensions

extensions(af, semantics="grounded")
accepted_arguments(af, semantics="preferred", mode="credulous")
```

> 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.
> Caminada, M. (2011). Semi-stable semantics. *Argument & Computation*, 2(1).
> Gaggl, S. A. & Woltran, S. (2013). The cf2 argumentation semantics
> revisited. *Journal of Logic and Computation*, 23(5), 925–949.
> Dung, P. M., Mancarella, P. & Toni, F. (2007). Computing ideal sceptical
> argumentation. *Artificial Intelligence*, 171(10–15), 642–674.

## Structured

`argumentation.structured.aspic.aspic` builds arguments from a knowledge base
and a set of strict and defeasible rules over a logical language with a
contrariness function, then derives attacks and defeats. The full ASPIC+
surface includes `build_arguments`, `compute_attacks`, `compute_defeats`,
argument accessors (`conc`, `prem`, `sub`, `top_rule`, `def_rules`,
`last_def_rules`, `prem_p`, `is_firm`, `is_strict`), `transposition_closure`,
`strict_closure`, `is_c_consistent`, and a `CSAF` type packaging the
constructed structured AF.

```python
from argumentation.structured.aspic.aspic import (
    ArgumentationSystem, ContrarinessFn, GroundAtom, KnowledgeBase, Literal,
    PreferenceConfig, Rule, build_arguments, compute_attacks, compute_defeats,
)

p, q = Literal(GroundAtom("p")), Literal(GroundAtom("q"))
system = ArgumentationSystem(
    language=frozenset({p, p.contrary, q, q.contrary}),
    contrariness=ContrarinessFn(
        contradictories=frozenset({(p, p.contrary), (q, q.contrary)}),
    ),
    strict_rules=frozenset(),
    defeasible_rules=frozenset({
        Rule(antecedents=(p,), consequent=q, kind="defeasible", name="r1"),
    }),
)
kb = KnowledgeBase(axioms=frozenset({p}), premises=frozenset())
pref = PreferenceConfig(
    rule_order=frozenset(), premise_order=frozenset(),
    comparison="elitist", link="last",
)
arguments = build_arguments(system, kb)
defeats = compute_defeats(compute_attacks(arguments, system), arguments, system, kb, pref)
```

`argumentation.structured.aspic.aspic_encoding` encodes ASPIC+ theories into a
deterministic ASP-style fact vocabulary (Lehtonen, Niskanen & Järvisalo 2024)
and provides a typed grounded-query surface backed by either the materialised
reference projection or an optional registered backend (e.g. clingo via the
`[asp]` extra).

`argumentation.structured.aspic.aspic_incomplete` reasons over ASPIC+ theories
with optional ordinary premises. `evaluate_incomplete_grounded` enumerates all
completions of the unknown premises and classifies a query literal as
`stable`, `relevant`, `unknown`, or `unsupported`.

`argumentation.structured.aspic.subjective_aspic` implements Wallner-style
value filtering before ASPIC+ argument construction.
`argumentation.core.accrual` exposes Prakken-style weak/strong applicability
checks and accrual envelopes for same-conclusion arguments.

`argumentation.structured.aba.aba` implements flat ABA and ABA+ over ASPIC
literals, including complete, preferred, stable, naive, grounded,
well-founded, and ideal assumption-extension functions plus a Dung
projection. `argumentation.structured.aba.aba_sat` provides task-directed
support-mask SAT enumeration for stable, complete, and preferred extensions.
`argumentation.structured.aba.aba_asp` provides clingo-backed extension
queries when the `[asp]` extra is installed.

> Modgil, S. & Prakken, H. (2018). A general account of argumentation with
> preferences. *Artificial Intelligence*, 248, 51–104.
> Lehtonen, T., Niskanen, A., & Järvisalo, M. (2024). Reasoning over ASPIC+
> in answer set programming. *KR 2024*.
> Odekerken, D., Borg, A. & Bex, F. (2023). Justification, stability and
> relevance for case-based reasoning with incomplete focus cases.

## Quantitative and bipolar

`argumentation.core.bipolar` adds an explicit support relation alongside
defeats. Support chains induce *derived* defeats (supported and indirect),
computed to a fixpoint, and yield d-, s-, and c-admissibility variants.

```python
from argumentation.core.bipolar import (
    BipolarArgumentationFramework, cayrol_derived_defeats,
    d_preferred_extensions,
)

baf = BipolarArgumentationFramework(
    arguments=frozenset({"a", "b", "c"}),
    defeats=frozenset({("b", "c")}),
    supports=frozenset({("a", "b")}),
)
cayrol_derived_defeats(baf.defeats, baf.supports)   # {("a", "c")}
```

`argumentation.ranking.ranking` provides non-binary acceptability rankings —
Categoriser scores, iterative Burden numbers, and others. Results expose
`scores`, `ranking` (a tuple of frozensets, one per tier, best first),
`converged`, `iterations`, and `semantics`:

```python
from argumentation.ranking.ranking import categoriser_ranking

result = categoriser_ranking(af)
result.scores       # {"a": 0.618..., "b": 0.618..., ...}
result.ranking      # tuple of frozensets, best tier first
result.converged    # True / False
```

`argumentation.ranking.weighted` implements Dunne-style weighted argument
systems by enumerating attack sets whose deleted weight fits an inconsistency
budget.

`argumentation.gradual.gradual` computes Potyka-style quadratic-energy
strengths for weighted bipolar graphs, exposes revised direct-impact
attribution, and computes exact Shapley-style per-attack impact scores
(Al Anaissy et al. 2024 Def 13).

`argumentation.gradual.dfquad` exposes DF-QuAD aggregation/combination and
strength propagation. `argumentation.gradual.equational` provides iterative
equational fixpoint scoring schemes. `argumentation.ranking.matt_toni`
computes finite zero-sum game strengths and raises when the game matrix is too
large for the in-package solver.

`argumentation.gradual.gradual_principles` and
`argumentation.ranking.ranking_axioms` contain executable checks for balance,
directionality, monotonicity, ranking preorder, void-precedence, and
cardinality-precedence obligations.

`argumentation.frameworks.vaf` implements Bench-Capon value-based
argumentation frameworks. `argumentation.gradual.llm_surface` is a
dependency-free QBAF adapter for argumentative LLM pipelines (Freedman et
al. 2025).

> Cayrol, C. & Lagasquie-Schiex, M.-C. (2005). On the acceptability of
> arguments in bipolar argumentation frameworks. In *ECSQARU 2005*.
> Al Anaissy, C., Toni, F., & Rago, A. (2024). Shapley value for argumentation.
> Freedman, G., Rago, A., Albini, E., Toni, F., & Cocarascu, O. (2025).
> Argumentative Large Language Models for explainable and contestable claim
> verification.

## Probabilistic and epistemic

`argumentation.probabilistic.probabilistic` implements probabilistic
argumentation frameworks (PrAFs). Each argument has an existence probability
and each defeat has a presence probability; acceptance is the probability over
sampled worlds.

```python
from argumentation.probabilistic.probabilistic import (
    ProbabilisticAF, compute_probabilistic_acceptance,
)

praf = ProbabilisticAF(
    framework=af,
    p_args={"a": 0.9, "b": 0.7, "c": 1.0, "d": 0.6},
    p_defeats={("a", "b"): 0.8, ("b", "c"): 1.0, ("c", "d"): 0.9, ("d", "a"): 0.5},
)
result = compute_probabilistic_acceptance(praf, semantics="grounded")
result.acceptance_probs    # {"a": ..., "b": ..., ...}
result.strategy_used       # auto-routed
```

`compute_probabilistic_acceptance` dispatches across seven strategies:

- `deterministic` — fast path when every probability is 0 or 1; collapses to
  standard Dung evaluation.
- `exact_enum` — brute-force enumeration over induced Dung AFs; default for
  small frameworks (up to ~13 arguments).
- `mc` — Monte Carlo sampling with Agresti–Coull stopping (Li, Oren & Norman
  2012 Algorithm 1), decomposed across connected components per Hunter &
  Thimm 2017 Proposition 18.
- `exact_dp` — adapted grounded edge-tracking tree-decomposition backend for
  credulous grounded acceptance on defeat-only worlds. Effective in practice
  for primal-graph treewidth ≤ ~15; not asymptotically faster than brute
  force, and not the full Popescu & Wallner I/O/U witness-table DP.
- `paper_td` — paper-faithful Popescu & Wallner (2024) Algorithm 1 for exact
  extension-probability queries. Opt-in only.
- `dfquad_quad` and `dfquad_baf` — DF-QuAD gradual semantics for
  quantitative bipolar frameworks (Freedman et al. 2025).

Two query kinds are supported. Per-argument acceptance is the default;
exact-set extension probability is opt-in via `query_kind="extension_probability"`
with `queried_set=...`. `summarize_defeat_relations` exposes exact defeat
marginals as a diagnostic.

`argumentation.probabilistic.epistemic` represents epistemic graphs with
positive and negative influences over belief levels, finite model
enumeration, evidence updates, and projection to constellation PrAFs. Install
`[z3]` to use its linear atomic constraint satisfiability and entailment
helpers.

> Li, H., Oren, N., & Norman, T. J. (2012). Probabilistic argumentation
> frameworks. In *TAFA 2011*.
> Hunter, A. & Thimm, M. (2017). Probabilistic reasoning with abstract
> argumentation frameworks. *JAIR*, 59, 565–611.
> Popescu, A. & Wallner, J. P. (2024). Tree-decomposition-based dynamic
> programming for probabilistic abstract argumentation.

## Specialized frameworks

`argumentation.frameworks.adf` implements abstract dialectical frameworks with
typed acceptance-condition ASTs, three-valued interpretations,
grounded/admissible/complete/model/preferred/stable model enumeration,
structural link classification, JSON/formula I/O helpers, and Dung bridges.

`argumentation.frameworks.setaf` implements argumentation frameworks with
collective attacks (conflict-free, admissible, complete, preferred, grounded,
stable, semi-stable, stage). `argumentation.frameworks.setaf_io` provides
ASPARTIX fact I/O plus compact deterministic SETAF parser/writer helpers. See
`docs/setaf.md` for semantics details.

`argumentation.frameworks.caf` implements claim-augmented AFs with inherited
and claim-level extension views plus a concurrence checker. See
`docs/caf-semantics.md`.

`argumentation.frameworks.vaf` implements Bench-Capon value-based
argumentation frameworks: audience-specific defeat removes attacks whose
target value is preferred to the attacker value, and objective/subjective
acceptance quantify over audience orders.
`argumentation.frameworks.vaf_completion` adds finite argument-chain and
audience helpers for fact-uncertainty completions.

`argumentation.frameworks.practical_reasoning` implements the Atkinson and
Bench-Capon AATS grounding for AS1-style practical arguments and the CQ5, CQ6,
and CQ11 choice-stage objections.

## Dynamics, revision, enforcement

`argumentation.frameworks.partial_af` represents AFs that leave some attack
pairs *uncertain*. Pairs over A × A are partitioned into `attacks`,
`ignorance`, and `non_attacks`; reasoning is by enumerating *completions*. The
module also provides three merge aggregations (`sum_merge_frameworks`,
`max_merge_frameworks`, `leximax_merge_frameworks`) and `consensual_expand`.

`argumentation.dynamics.af_revision` adds arguments and attacks to an existing
framework, or revises an extension state by a formula or by a target
framework, while preserving rationality postulates:

```python
from argumentation.dynamics.af_revision import (
    baumann_2015_kernel_union_expand,
    cayrol_2014_classify_grounded_argument_addition,
    AFChangeKind,
)

merged = baumann_2015_kernel_union_expand(base_af, incoming_af)
kind = cayrol_2014_classify_grounded_argument_addition(
    framework=base_af, argument="x",
    attacks=frozenset({("x", "a")}),
)
# AFChangeKind.DECISIVE | RESTRICTIVE | QUESTIONING |
# DESTRUCTIVE | EXPANSIVE | CONSERVATIVE | ALTERING
```

`argumentation.dynamics.dynamic` provides a recompute-from-scratch dynamic AF
wrapper with argument/attack update streams and credulous/skeptical queries
after each state transition.

`argumentation.dynamics.enforcement` provides a brute-force minimal-change
oracle for argument and extension enforcement, returning typed witness edits,
the edited framework, and the resulting extensions.

`argumentation.dynamics.approximate` exposes k-stable semantics, bounded
grounded iteration, and budgeted semi-stable approximation with exactness
metadata.

> Baumann, R. (2015). Context-free and context-sensitive kernels: update and
> deletion equivalence in abstract argumentation. In *ECAI 2014*.
> Diller, M., Haret, A., Linsbichler, T., Rümmele, S., & Woltran, S. (2015).
> An extension-based approach to belief revision in abstract argumentation.
> Cayrol, C., de Saint-Cyr, F. D., & Lagasquie-Schiex, M.-C. (2010).
> Change in abstract argumentation frameworks: adding an argument.
> *JAIR*, 38, 49–84.

## Encoding and interop

`argumentation.interop.iccma` reads and writes ICCMA-style AF, ADF, and ABA
exchange formats:

```python
from argumentation.interop.iccma import parse_af, write_af

af = parse_af("p af 3\n1 2\n2 3\n")
text = write_af(af)
```

`argumentation.solving.sat_encoding` exposes `sat_extensions`, the `"sat"`
backend's in-package routing helper over the native Dung/SCC enumerators (no
external SAT solver and no standalone CNF apparatus). The Z3-backed
incremental SAT kernel for Dung AFs with telemetry (`SATCheck`,
`SATTraceSink`, `AfSatKernel`) lives in `argumentation.solving.af_sat`.
`argumentation.structured.aba.aba_sat` provides task-directed SAT enumeration
for ABA.

`argumentation.structured.aspic.datalog_grounding` (requires the
`[grounding]` extra) grounds a Gunray `DefeasibleTheory` into propositional
ASPIC+ via `ground_defeasible_theory(theory) -> GroundedDatalogTheory`. It
consumes [Gunray](https://github.com/ctoth/gunray) — a sister project that
owns the defeasible-theory schema — rather than redefining one.

`argumentation.gradual.llm_surface` is a dependency-free adapter for
argumentative LLM pipelines: callers supply propositions and attack/support
edges, the package computes QBAF strengths, Shapley-style attack
explanations, and contestation witnesses.

The package ships with prebuilt clingo `.lp` encodings under
`argumentation.encodings/` (admissible/complete/stable for AF, ASPIC+, and
ABA), used by the ASP-backed paths.

## Solver surfaces

`argumentation.solving.solver` separates solver tasks by result type:

- `ExtensionEnumerationSuccess` — all extensions for enumeration tasks.
- `SingleExtensionSuccess` — one witness extension or `None`.
- `AcceptanceSuccess` — credulous/skeptical yes/no plus a witness or
  counterexample when the backend supplies one.

Entry points include `solve_dung_extensions`, `solve_dung_single_extension`,
`solve_dung_acceptance`, `solve_aba_extensions`, `solve_aba_single_extension`,
`solve_aba_acceptance`, `solve_adf_models`, and `solve_setaf_extensions`.

ICCMA `SE` tasks produce one witness, not full enumeration. Use
`solve_dung_single_extension(..., backend="iccma", iccma=ICCMAConfig(...))` or
the ABA equivalent for that contract; `solve_dung_extensions(..., backend="iccma")`
returns typed unavailable instead of pretending one witness enumerates every
extension.

Capability detection and backend auto-selection live inside
`argumentation.solving.solver`: `backend="auto"` resolves per semantics/task
through the `_auto_*` routing helpers (`_has_clingo()` gates the ASP-backed
ABA paths). See `docs/backends.md` for the backend-string set and the routing
table. `argumentation.core.solver_results` defines the typed
`SolverUnavailable`, `SolverProcessError`, and `SolverProtocolError` returns.
`argumentation.solving.solver_differential` provides
`solver_capability_matrix` and task-aware comparison helpers across native,
ICCMA, SAT, clingo, ADF, SETAF, and unsupported backend combinations.

unsupported task/semantics/backend combinations return typed unavailable
results before subprocess invocation. Optional solver environment variables
used by smoke tests: `ICCMA_AF_SOLVER`, `ICCMA_ABA_SOLVER`, `ASPFORABA_SOLVER`.

External callers supply already-projected frameworks, theories, or benchmark
manifests and consume package result objects; the package does not own caller
identity, storage, merge policy, provenance, or rendering policy.

## `iccma-cli`

The package ships an ICCMA-format command-line solver, registered as the
`iccma-cli` console script:

```powershell
iccma-cli --problem SE-ST --file framework.af
iccma-cli --problem DC-PR --file framework.af --argument 3
iccma-cli --problem SE-CO --file theory.aba --backend sat
```

Supported problem codes: `SE` (single extension), `DC` (credulous decision),
`DS` (skeptical decision). Supported semantics: `CO`, `GR`, `PR`, `ST`, `SST`,
`STG`, `ID`, `CF2`. Backends: `auto`, `native`, `sat`. The CLI dispatches into
`argumentation.solving.solver` and reads ICCMA `p af` and `p aba` input files.
Its module entry point is `argumentation.solving.iccma_cli`.

## Design

- Pure-Python algorithms are the reference implementation for package-owned
  algorithms. Solver adapters are typed boundaries around external tools or
  optional dependencies.
- The package is organized into layered subpackages with an
  `import-linter`-enforced import DAG; an upward import fails CI. See
  `docs/architecture.md` for the layer contract.
- Frameworks, rules, arguments, and extensions are immutable frozen
  dataclasses over frozensets. Equality is structural.
- Conflict-freeness is checked against the pre-preference attack relation;
  defence is checked against defeats. Both are tracked separately on
  `ArgumentationFramework`.
- Algorithms cite their formal source in module and function docstrings.

`docs/architecture.md` is the long form. `docs/backends.md` documents the
default backend selection rule. `docs/gaps.md` enumerates known limitations
and open workstreams. [`CHANGELOG.md`](CHANGELOG.md) records release history,
including the 0.3.0 layered-subpackage reorganization and the complete
old→new import-path table.

## Non-goals

`argumentation` does not own application provenance, source calibration,
subjective-logic opinion calculi, persistent storage, repository workflow, or
application-side argument rendering. Callers translate those concerns into
finite formal objects before invoking this package. The `iccma-cli` script
is a thin solver wrapper for ICCMA-format files; it is not an
application-side CLI.

## Development

```powershell
uv sync
uv run pyright src
uv run lint-imports
uv run pytest -vv
```

Tests are tagged `unit`, `property`, and `differential`. Property tests use
Hypothesis. Differential tests cross-check independently implemented package
paths where the repository has more than one executable route.
`uv run lint-imports` enforces the layered import DAG.

See `CONTRIBUTING.md` for contribution guidelines.
