This report describes how ArgForge works.

ArgForge was developed in Python 3. Its semantics and extensions are computed with Answer Set Programming (ASP).

Every evaluation goes through the same six steps, and each step uses only the result of the one before it:

1. the theory is read and checked;
2. every argument is built;
3. every attack between arguments is found;
4. preferences decide which attacks succeed, that is, which are defeats;
5. the extensions of the chosen semantics are computed;
6. the status of every claim is determined.

An argumentation theory can consist of the following elements: axioms, which are certain facts; premises; strict rules (a, b → c); defeasible rules (a, b ⇒ c); a conflict relation; and preferences over defeasible rules and over premises.

An argument is a finite derivation tree. It is either a premise or an axiom on its own, or a rule applied to one argument for each of the rule's antecedents. Each different combination of sub-arguments gives a separate argument: if one antecedent of a rule can be derived in three different ways and another in two, the rule yields six arguments for the same claim.

For every argument A, ArgForge records its conclusion, its sub-arguments, the ordinary premises it uses, its defeasible rules and its last defeasible rules. An argument that uses no defeasible rule is called strict, and an argument that uses no ordinary premise is called firm.

An argument A attacks an argument B through one of B's sub-arguments, B′. There are three ways to do this:

• Undermining: B′ is an ordinary premise and A's conclusion conflicts with that premise.
• Rebutting: B′ ends with a defeasible rule and A's conclusion conflicts with B′'s conclusion.
• Undercutting: B′ ends with a defeasible rule r, and A concludes that r does not apply in this case (-r).

The conclusions of strict steps cannot be contested, and axioms cannot be attacked. Two kinds of conflict can be declared. A contradictory pair behaves like x and -x: each attacks the other. A contrary is one-way: x attacks y, but y does not attack x. Undercuts and attacks through a contrary always succeed, whatever the preferences; the outcome of every other attack depends on the preferences.

A preference-dependent attack by A on B′ succeeds unless A is strictly weaker than B′; in that case A defeats B. Arguments are compared through sets of rules or sets of premises. For two sets X and Y:

• Elitist comparison: X is weaker if some element of X is weaker than every element of Y.
• Democratic comparison: X is weaker if every element of X is weaker than at least one element of Y.
• An empty set is never weaker; every non-empty set is weaker than the empty set.

Last link compares the last defeasible rules of the two arguments; if neither has such a rule, it looks at their ordinary premises. Weakest link compares premises if both arguments are strict, and defeasible rules if both are firm; otherwise it requires both the premises and the rules to be weaker. Declared preferences are extended transitively and may not form a cycle; two rules cannot be declared equally strong.

Once the defeats are known, a set S none of whose members defeats another is called conflict-free. S defends A if every argument that defeats A is defeated by a member of S. The semantics select sets as follows:

• Admissible: conflict-free and defends all its members.
• Complete: admissible and contains every argument it defends.
• Grounded: the smallest complete extension.
• Preferred: the complete extensions that are largest with respect to set inclusion.
• Stable: conflict-free and defeats every argument outside it.

The status of a claim is determined by looking at all the extensions together. If every extension contains an argument for the claim, the claim is justified. If some extensions contain one and some do not, it is defensible. If, in every extension, every argument for the claim is defeated, it is overruled; if none of these holds, it is undecided. The acceptance share shows the proportion of extensions that contain an argument for the claim.

Caminada and Amgoud (2007) expect two things of the accepted conclusions: they should be consistent with each other, and they should include everything the strict rules require. ASPIC+ guarantees this for well-defined theories. In a well-defined theory the axioms are consistent, no contrary targets an axiom or a strict conclusion, and the strict rules are closed under transposition. This means that for every strict rule a₁, …, aₙ → c and every i, the rule a₁, …, −c, …, aₙ → −aᵢ is also present, where −x stands for any contradictory of x.

The option “Add contrapositives of strict rules” in ArgForge adds the missing contrapositives. It does not repair the other conditions: if the axioms contradict each other, for example, the results remain inconsistent. With the option off, a theory containing p, -q and p → q, and preferring -q to p, accepts both q and -q. With the option on, the added rule -q → -p lets -q defeat p, and only -q and -p remain standing.

When rules form a cycle that can be reached from the facts, for example a premise p together with the rules p ⇒ q and q ⇒ p, every argument is still finite, but there are infinitely many of them. ArgForge therefore groups arguments into classes and keeps one representative of each class.

Every argument has a signature: the set made up of its own description (its conclusion, its top rule, its last defeasible rules, its defeasible rules and its ordinary premises) and the descriptions of all its sub-arguments. Three facts make this grouping exact:

1. Whether A attacks or defeats B depends only on A's description and the descriptions of B's sub-arguments. Arguments with the same signature therefore attack and defeat the same arguments, and are themselves attacked and defeated by the same arguments.
2. Such interchangeable arguments are always accepted together or rejected together. Under the grounded, complete, preferred and stable semantics, every extension of the full, infinite framework therefore corresponds to exactly one extension of the framework of representatives, and the claim statuses do not change.
3. An argument's signature depends only on the signatures of its sub-arguments, and there are finitely many signatures. Combining representatives step by step reaches every class and eventually stops.

Every explanation reports facts computed from the result. For a selected argument, ArgForge shows how it is built step by step from its direct sub-arguments, the premises and rules it relies on, its label in the selected extension and the reason for that label:

• accepted: a member of the extension answers every argument that defeats it; each defeater is shown together with the argument that answers it;
• defeated: the members of the extension that defeat it are shown;
• undecided: the arguments that defeat it and are themselves undecided are shown.

Attacks on the argument that fail because of preferences are listed as well. Every explanation states which extension it concerns; if the semantics has no extension, it says that grounded labels are shown instead. The claim explanation below it states the claim's status exactly: for a justified claim, that every extension contains an argument for it; for a defensible claim, the extensions that accept it; and for an overruled claim, which accepted arguments defeat each of its arguments.

The grounded round shows at which step of the grounded computation an argument's status was settled; round 0 means that nothing defeats it.

Strength is the h-categorizer score of Besnard and Hunter (2001): s(a) = 1 / (1 + Σ s(b)). The sum is taken over the arguments b that defeat a, and the formula is repeated until the values stop changing. An argument that nothing defeats has strength 1; a single undefeated defeater lowers this to 0.5; two arguments that defeat each other both receive 0.618. Strength is a graded measure on the defeat graph and is not the same as being accepted.

Random theories are created with a seeded generator; the same seed always gives the same theory. In the workspace, each new theory also chooses its own size and its own mix of components. Each of these components may or may not appear in a theory: negation, strict and defeasible rules, axioms, mutually conflicting premises, rules with more than one condition, undercuts, rule and premise preferences, contraries, contradictories and cycles.

Every generated theory is valid, its axioms are consistent and its contraries are correctly defined. Every rule is applicable, because its conditions are made of facts or of the conclusions of other rules. With the option “Add contrapositives of strict rules” on, the theory is also well defined.