<h1 align="center">
  <br>
  <img src="assets/pickaxe.svg" alt="pickaxe" width="96">
  <br>
  pickaxe-rs
  <br>
</h1>

<p align="center">
  <strong>An ASPIC+ argumentation engine</strong>
</p>

<p align="center">
  High-performance, pure-Rust implementation of the
  <a href="https://doi.org/10.1016/j.artint.2012.10.008">ASPIC+</a> framework
  (Modgil &amp; Prakken, 2013; 2014), with the
  Prakken (2019) accrual extension.
</p>

<p align="center">
  <a href="#quick-start-library">Library</a>&ensp;&middot;&ensp;<a href="#quick-start-cli">CLI</a>&ensp;&middot;&ensp;<a href="#pipeline-architecture">Architecture</a>&ensp;&middot;&ensp;<a href="#algorithms-and-literature">Algorithms</a>&ensp;&middot;&ensp;<a href="#feature-flags">Features</a>&ensp;&middot;&ensp;<a href="#references">References</a>
</p>

---

ASPIC+ is a formal framework for constructing arguments from a knowledge
base of premises and inference rules, identifying attacks between those
arguments, computing defeats via preference orderings, and evaluating
which arguments are ultimately acceptable under Dung-style semantics.
For a gentle introduction, see the
[tutorial paper](https://doi.org/10.1080/19462166.2013.869766) by Modgil
& Prakken (2014).

## Quick start (library)

Add pickaxe-rs to your `Cargo.toml`:

```toml
[dependencies]
pickaxe-rs = "0.1"
```

The classic Tweety Triangle — birds defeasibly fly, penguins strictly
don't, Tweety is both:

```rust
use pickaxe_rs::prelude::*;

let (system, _warnings) = AspicSystemBuilder::new()
    .ordinary_premise(formula!(bird(tweety)))
    .ordinary_premise(formula!(penguin(tweety)))
    .defeasible_rule("d1", vec![formula!(bird(tweety))], formula!(flies(tweety)))
    .strict_rule("s1", vec![formula!(penguin(tweety))], formula!(bird(tweety)))
    .strict_rule("s2", vec![formula!(penguin(tweety))], formula!(!flies(tweety)))
    .with_classical_negation()
    .build();

let rule_ord = TieredOrdering::new(vec![
    vec![RuleId("s2".into())],
    vec![RuleId("d1".into())],
]);

let ordering: Box<dyn ArgumentOrdering> = Box::new(LastLinkOrdering {
    rule_ordering: Box::new(rule_ord),
    premise_ordering: Box::new(NoPreference),
    lifting: LiftingStrategy::Elitist,
});

let pipeline = AspicPipeline::classical(system, ordering);
let result = pipeline.evaluate(Semantics::Grounded).unwrap();

for &arg_id in &result.extensions[0] {
    if let Some(arg) = result.store.get(arg_id) {
        println!("{}", arg.conclusion());
    }
}
```

For full control over each pipeline stage, construct `AspicPipeline`
directly:

```rust
let pipeline = AspicPipeline {
    system,
    grounder: Box::new(NaiveGrounder),
    arg_constructor: Box::new(ForwardChainingConstructor),
    attack_computer: Box::new(PairwiseAttackComputer),
    evaluator: Box::new(ClassicalEvaluator {
        semantics_solver: Box::new(NaiveEnumerationSolver),
    }),
    preference: PreferenceConfig::ArgumentOrdering(ordering),
};

let result = pipeline.evaluate(Semantics::Preferred).unwrap();
```

## Quick start (CLI)

The `pickaxe` binary reads a theory JSON file, runs the full ASPIC+
pipeline, and outputs structured JSON with extensions and per-stage
timing.

```bash
cargo install pickaxe-rs --features cli
```

Minimal invocation:

```bash
pickaxe -i theory.json -s grounded
```

With preferences and a faster solver backend:

```bash
pickaxe -i theory.json -s preferred \
    --preferences last-link-elitist \
    --solver scc-sat
```

Using a named preset (wires up grounder, attack computer, and solver
together):

```bash
pickaxe -i theory.json -s stable --preset optimised
```

<details>
<summary><strong>All CLI flags</strong></summary>

<br>

| Flag | Values | Default |
| :--- | :--- | :--- |
| `-s` / `--semantics` | `grounded`, `preferred`, `stable`, `complete`, `semi-stable`, `ideal`, `eager`, `admissible` | *(required)* |
| `--preferences` | `none`, `flat`, `last-link-elitist`, `last-link-democratic`, `weakest-link-elitist`, `weakest-link-democratic` | `none` |
| `--solver` | `naive-enumeration`, `sat`, `scc-sat`, `sat-cadical`, `scc-sat-cadical`, `aspartix`, `mutoksia` | `naive-enumeration` |
| `--preset` | `classical`, `optimised`, `accrual` | *(none)* |
| `--task` | `enumerate-all`, `find-one`, `count` | `enumerate-all` |
| `--format` | `simple`, `native` | `simple` |
| `--grounder` | `naive`, `semi-naive` | `naive` |
| `--attack-computer` | `pairwise`, `indexed` | `pairwise` |

Run `pickaxe --help` for the full list.

</details>

## JSON input format

The **simple** format is designed for hand-authored theories and
external tool interop. Formulae are plain strings (`"p"`, `"-q"` for
negation):

```json
{
    "premises": [
        { "formula": "bird", "kind": "ordinary" },
        { "formula": "penguin", "kind": "ordinary" }
    ],
    "strict_rules": [
        { "id": "s1", "antecedents": ["penguin"], "consequent": "bird" },
        { "id": "s2", "antecedents": ["penguin"], "consequent": "-flies" }
    ],
    "defeasible_rules": [
        { "id": "d1", "antecedents": ["bird"], "consequent": "flies" }
    ],
    "contrariness": [
        { "target": "flies", "attacker": "-flies", "relation": "contradictory" }
    ],
    "rule_preferences": [
        { "superior": "s2", "inferior": "d1" }
    ],
    "classical_negation": false
}
```

When `classical_negation` is `true`, every literal `p` automatically
gets a contradictory counterpart `-p` (and vice versa), so you can omit
explicit contrariness entries for classically-negated pairs.

A **native** format (`--format native`) uses the full `Formula` type for
lossless round-trips with programmatic consumers.

## Examples

Three runnable examples ship in `examples/`:

| Example | Description | Command |
| :--- | :--- | :--- |
| `tweety.rs` | Tweety Triangle with last-link elitist ordering and TGF export | `cargo run --example tweety` |
| `custom_pipeline.rs` | Manual pipeline assembly with weakest-link democratic ordering, evaluating under three semantics | `cargo run --example custom_pipeline` |
| `json_input.rs` | Loading a theory from JSON, building orderings from `rule_preferences`, and native-format round-tripping | `cargo run --example json_input --features json` |

---

## Pipeline architecture

The evaluation pipeline has four stages, each defined by a swappable
trait. Every stage can be replaced with an alternative implementation.

```mermaid
flowchart LR
    AS[AspicSystem] --> G[Grounder]
    G --> GS[GroundedSystem]
    GS --> AC[ArgumentConstructor]
    AC --> Store[ArgumentStore]
    Store --> ATC[AttackComputer]
    ATC --> Attacks["Vec of Attack"]
    Attacks --> E[Evaluator]
    E --> Result[PipelineResult]
```

### Stage implementations

**Grounding** &ensp;(`Grounder` trait) — eliminates first-order variables
via Herbrand substitution.

- `NaiveGrounder` — exhaustive substitution with a configurable
  explosion limit.
- `SemiNaiveGrounder` — incremental grounding that avoids
  re-deriving already-seen instances.

**Argument construction** &ensp;(`ArgumentConstructor` trait) — builds the
set of all derivable ASPIC+ arguments.

- `ForwardChainingConstructor` — fixpoint saturation with a
  non-circularity guard (see
  [Algorithms and literature](#algorithms-and-literature) below).

**Attack computation** &ensp;(`AttackComputer` trait) — identifies rebut,
undermine, and undercut attacks between arguments.

- `PairwiseAttackComputer` — brute-force pairwise comparison.
- `IndexedAttackComputer` — hash-index lookups for faster attack
  identification (requires `sat` feature).

**Evaluation** &ensp;(`Evaluator` trait) — computes defeats (applying
preference orderings), builds an abstract argumentation framework,
and solves for extensions.

- `ClassicalEvaluator` — delegates to an interchangeable
  `SemanticsSolver`.
- `AccrualEvaluator` — implements Prakken (2019) accrual semantics
  with set-level preferences.

### Semantics solvers

The `ClassicalEvaluator` wraps an interchangeable `SemanticsSolver`:

| Solver | Feature gate | Notes |
| :--- | :--- | :--- |
| `NaiveEnumerationSolver` | *(always available)* | Reference enumeration solver for all semantics |
| `SatSolver<S>` | `sat` | Propositional SAT encoding; default backend is BatSat (pure Rust). CaDiCaL available via `cadical` feature |
| `SccDecomposingSolver` | `sat` | Decomposes the framework by SCCs and solves each independently, wrapping an inner `SemanticsSolver` |
| `AspartixSolver` | `aspartix` | Shells out to [clingo](https://potassco.org/clingo/) via ASPARTIX encodings |
| `IccmaSolver` | `iccma` | Wraps an ICCMA-compatible external solver binary |

### Pipeline presets

Three convenience constructors wire up common configurations:

| Preset | Configuration |
| :--- | :--- |
| `AspicPipeline::classical()` | `NaiveGrounder` + `ForwardChainingConstructor` + `PairwiseAttackComputer` + `ClassicalEvaluator(NaiveEnumerationSolver)` |
| `AspicPipeline::optimised()` *(feature `sat`)* | `NaiveGrounder` + `ForwardChainingConstructor` + `IndexedAttackComputer` + `ClassicalEvaluator(SccDecomposingSolver(SatSolver))` |
| `AspicPipeline::accrual()` | `NaiveGrounder` + `ForwardChainingConstructor` + `PairwiseAttackComputer` + `AccrualEvaluator` with `SetPreference` |

---

## Algorithms and literature

### Forward-chaining argument construction

Arguments are built by forward-chaining saturation over the grounded
rule set:

1. **Seed** — create one premise argument per knowledge base entry.
2. **Saturate** — repeatedly fire every rule against the current
   argument store. For each rule whose antecedents are matched by
   existing argument conclusions, every combination of supporting
   sub-arguments is considered. A candidate is accepted only when its
   conclusion does not already appear among the transitive
   sub-conclusions of the chosen sub-arguments (the *non-circularity
   guard* from Li et al. 2017 / Grooters & Prakken), and no
   structurally identical argument (same rule + same sub-argument
   list) exists.
3. **Terminate** — the loop halts when a full pass produces no new
   arguments.

See `doc/forward-chaining-construction.tex` for a detailed writeup.

### Preference orderings and defeat

Attacks are filtered into defeats by applying a configurable preference
ordering over arguments (Modgil & Prakken, 2013; 2014):

- **Last-link** — compares arguments by the preference over the
  last rule applied in each argument.
- **Weakest-link** — compares arguments by the preference over the
  weakest (least preferred) rule or premise used anywhere in the
  argument.
- **Flat** — a simple rule-level ordering without lifting.

Both last-link and weakest-link support **lifting strategies** for
comparing sets of rules/premises:

- **Elitist** — A is preferred if its best element beats B's best.
- **Democratic** — A is preferred if every element of A beats every
  element of B.

### SAT-based evaluation

The `SatSolver` encodes Dung-style semantics as propositional SAT
problems, following Besnard & Doutre (2004) and Cerutti et al. (2014).
Each argument maps to a propositional variable. Constraints are layered:

- **Conflict-free**: for each defeat `(a, b)`, `¬x_a ∨ ¬x_b`.
- **Defence (admissibility)**: if `b` is accepted then some
  counter-attacker of each attacker of `b` must be accepted.
- **Stable range**: each argument is either accepted or attacked by an
  accepted argument.
- **Complete closure**: auxiliary variables encode the characteristic
  function fixpoint.

Preferred and semi-stable extensions use iterative maximisation with
blocking clauses on top of admissibility/completeness encodings.

The default backend is **BatSat** (pure Rust, no FFI). **CaDiCaL** is
available via the `cadical` feature.

### SCC decomposition

The `SccDecomposingSolver` partitions the abstract framework into
strongly connected components (via Tarjan's algorithm) and solves each
independently, composing partial extensions bottom-up in topological
order. This is exact for grounded, complete, preferred, stable, and
admissible semantics (Baroni, Giacomin & Guida, 2005). For ideal
semantics, preferred extensions are computed via SCC recursion and the
ideal extension is derived as the maximal admissible subset of their
intersection. Semi-stable and eager fall back to full-framework solving.

### Graph utilities

Three domain-agnostic graph algorithms are used internally
(`src/algorithms/`):

- **Tarjan's SCC** (Tarjan, 1972) — finds strongly connected
  components; used by `AbstractFramework::sccs()` and
  `SccDecomposingSolver`.
- **Kahn's topological layers** (Kahn, 1962) — peels sources
  iteratively to produce layered tiers; used to build tiered rule
  orderings from preference-pair DAGs.
- **Maximal-by-inclusion** — filters a set of sets to retain only
  ⊆-maximal elements; used by the SAT, naive, and accrual solvers
  when computing preferred extensions.

---

## The Bernays-Schoenfinkel (BS) fragment

The language **L** is restricted to the
[Bernays-Schoenfinkel fragment](https://en.wikipedia.org/wiki/Bernays%E2%80%93Sch%C3%B6nfinkel_class)
of first-order logic:

- **Terms** are either variables or constants — no function symbols.
  The `Term` type has exactly two variants: `Var(String)` and
  `Const(String)`.
- Variables are implicitly universally quantified over a **finite
  Herbrand universe** consisting of all constants that appear in
  premises and rules.
- Because the universe is finite, **grounding always terminates**. A
  configurable explosion guard (default: 100,000 ground instances)
  raises `AspicError::GroundingExplosion` if the limit is exceeded.
- The `formula!` macro uses a naming convention: **uppercase**
  identifiers become variables, **lowercase** become constants (e.g.
  `formula!(bird(X))` — `X` is a variable, `bird` is a predicate
  over the constant `X` will be bound to).

Compound formula constructors (`And`, `Or`, `Implies`, `Not`) exist in
the type system for user-space extensions but are not consumed by the
core pipeline.

## Supported semantics

| Semantics | Reference |
| :--- | :--- |
| Grounded | Dung (1995) |
| Complete | Dung (1995) |
| Preferred | Dung (1995) |
| Stable | Dung (1995) |
| Semi-stable | Caminada, Carnielli & Dunne (2012) |
| Ideal | Dung, Mancarella & Toni (2007) |
| Eager | Caminada (2007) |
| Admissible | Dung (1995) |

## Feature flags

| Feature | Default | What it enables |
| :--- | :---: | :--- |
| `sat` | Yes | `SatSolver`, `SccDecomposingSolver`, `IndexedAttackComputer`, `optimised()` preset |
| `cadical` | No | CaDiCaL as an alternative SAT backend (implies `sat`) |
| `json` | Yes | JSON serialization via `serde_json` |
| `toml-ser` | Yes | TOML serialization via `toml` |
| `aspartix` | No | `AspartixSolver` (requires `clingo` on `PATH`) |
| `iccma` | No | `IccmaSolver` (requires an ICCMA-compatible solver on `PATH`) |
| `cli` | No | Builds the `pickaxe` command-line binary (implies `json`) |

## Export formats

The `AbstractFramework` supports export to:

| Format | Extension | Use case |
| :--- | :---: | :--- |
| TGF | `.tgf` | Trivial Graph Format |
| ASPARTIX | — | ASP-based argumentation solver interop |
| DOT | `.dot` | Graphviz visualisation |
| ICCMA | — | Competition format |

## Deviations from the formal papers

The implementation closely follows Modgil & Prakken (2013, 2014) and
Prakken (2019), with deliberate engineering choices where the formal
definitions are silent or where practical concerns arise. Notable
deviations include: restriction of the language to the BS fragment, an
explicit Herbrand grounding stage not present in the formal framework,
bundling of the argumentation system, knowledge base, and contrariness
function into a single `AspicSystem` struct, and argument deduplication
by rule ID and sub-argument vector.

## Testing

```bash
cargo test
```

The test suite covers argument construction, attack classification,
defeat with various orderings, all eight semantics, grounding,
rationality postulates, accrual evaluation, and pipeline integration.
Several test cases are adapted from the
[PyArg](https://github.com/DaphneOdekerken/PyArg) library for
cross-validation. Property-based tests via
[proptest](https://crates.io/crates/proptest) exercise edge cases in
formula parsing, grounding, and ordering logic.

---

## References

<details>
<summary>Expand full bibliography</summary>

<br>

- Modgil, S. & Prakken, H. (2014). The ASPIC+ framework for structured
  argumentation: a tutorial. *Argument & Computation*, 5(1), 31--62.
  [doi:10.1080/19462166.2013.869766](https://doi.org/10.1080/19462166.2013.869766)
- Modgil, S. & Prakken, H. (2013). A general account of argumentation with
  preferences. *Artificial Intelligence*, 195, 361--397.
  [doi:10.1016/j.artint.2012.10.008](https://doi.org/10.1016/j.artint.2012.10.008)
- Young, A.P., Modgil, S. & Prakken, H. (2018). Erratum to "A general account
  of argumentation with preferences." [doi:10.1016/j.artint.2018.05.001](https://doi.org/10.1016/j.artint.2018.05.001)
- Prakken, H. (2019). Modelling accrual of arguments in ASPIC+. *Proc. ICAIL
  '19*, pp. 103--112. ACM.
  [doi:10.1145/3322640.3326703](https://doi.org/10.1145/3322640.3326703)
- 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.
  [doi:10.1016/0004-3702(94)00041-X](https://doi.org/10.1016/0004-3702(94)00041-X)
- Baroni, P., Giacomin, M. & Guida, G. (2005). SCC-recursiveness: a general
  schema for argumentation semantics. *Artificial Intelligence*, 168(1--2),
  162--210.
  [doi:10.1016/j.artint.2005.05.006](https://doi.org/10.1016/j.artint.2005.05.006)
- Besnard, P. & Doutre, S. (2004). Checking the acceptability of a set of
  arguments. *Proc. NMR 2004*, pp. 59--64.
- Cerutti, F., Dunne, P.E., Giacomin, M. & Vallati, M. (2014). Computing
  preferred extensions in abstract argumentation: a SAT-based approach. *Proc.
  COMMA 2014*, pp. 176--184.
  [doi:10.3233/978-1-61499-436-7-176](https://doi.org/10.3233/978-1-61499-436-7-176)
- Caminada, M. & Amgoud, L. (2007). On the evaluation of argumentation
  formalisms. *Artificial Intelligence*, 171(5--6), 286--310.
  [doi:10.1016/j.artint.2007.02.003](https://doi.org/10.1016/j.artint.2007.02.003)
- Caminada, M., Carnielli, W. & Dunne, P. (2012). Semi-stable semantics.
  *Journal of Logic and Computation*, 22(5), 1207--1254.
  [doi:10.1093/logcom/exr033](https://doi.org/10.1093/logcom/exr033)
- Dung, P.M., Mancarella, P. & Toni, F. (2007). Computing ideal sceptical
  argumentation. *Artificial Intelligence*, 171(10--15), 642--674.
  [doi:10.1016/j.artint.2007.05.003](https://doi.org/10.1016/j.artint.2007.05.003)
- Egly, U., Gaggl, S.A. & Woltran, S. (2010). Answer-set programming encodings
  for argumentation frameworks. *Argument and Computation*, 1(2), 147--177.
  [doi:10.1080/19462166.2010.486479](https://doi.org/10.1080/19462166.2010.486479)
- Gaggl, S.A., Manthey, N., Ronca, A., Wallner, J.P. & Woltran, S. (2015).
  Improved answer-set programming encodings for abstract argumentation. *Theory
  and Practice of Logic Programming*, 15(4--5), 434--448.
  [doi:10.1017/S1471068415000149](https://doi.org/10.1017/S1471068415000149)
- Dvorak, W., Rapberger, A., Wallner, J.P. & Woltran, S. (2020). ASPARTIX-V19.
  *FoIKS 2020*, pp. 79--89.
  [doi:10.1007/978-3-030-39951-1_5](https://doi.org/10.1007/978-3-030-39951-1_5)
- Li, H., Oren, N. & Norman, T.J. (2017). Probabilistic argumentation
  frameworks. *Proc. TAFA 2015*, pp. 1--16. Springer.
- Tarjan, R.E. (1972). Depth-first search and linear graph algorithms. *SIAM
  Journal on Computing*, 1(2), 146--160.
- Kahn, A.B. (1962). Topological sorting of large networks. *Communications of
  the ACM*, 5(11), 558--562.

</details>

## Acknowledgements

**PyArg** — Several test cases are adapted from the
[PyArg](https://github.com/DaphneOdekerken/PyArg) library by Daphne
Odekerken (MIT License). These tests validate that the Rust
implementation produces equivalent results to PyArg on shared scenarios.

**ASPARTIX** — The ASP encodings in `encodings/aspartix/` originate
from the [ASPARTIX](https://www.dbai.tuwien.ac.at/research/argumentation/aspartix/dung.html)
project at TU Wien, developed by Uwe Egly, Sarah Alice Gaggl, Wolfgang
Dvorak, Johannes Peter Wallner, Stefan Woltran, and others. They are
redistributed for interoperability with the `AspartixSolver` and serve
primarily as a reference oracle for validating the built-in solvers.

## License

MIT
