Language.CarneadesIntoDung.Translation

This module implements a translation from the Carneades argumentation model into Dung's argumentation frameworks. Any cycle-free Carneades Argument Evaluation Structure (CAES) is handled. We also give a Haskell implementation of correspondence properties.

Translation is done according to the following algorithm (see also "Towards a framework for the implementation and verification of translations between argumentation models" by Bas van Gijzel and Henrik Nilsson)

1. generatedArgs = emptyset.
2. sortedArgs = Topological sort of arguments on its dependency graph.
3. while sortedArgs != emptyset:

• Pick the first argument in sortedArgs. Remove all arguments from sortedArgs that have the same conclusion, c, and put them in argSet.
• Translate applicability part of arguments argSet, building on previously generatedArgs and put the generated arguments in tempArgs.
• argSet = emptyset
• Repeat the above three steps for the arguments for the opposite conclusion.
• Translate the acceptability part of c and the opposite conclusion based on arguments in tempArgs. Add the results and tempArgs to generatedArgs.
• tempArgs = emptyset

Basic types

type ConcreteArg = Either PropLiteral Argument

A concrete argument (in an argumentation framework) is either a Carneades propositional literal, or a Carneades argument.

type LConcreteArg = (Bool, ConcreteArg)

A labelled version of the concrete argument allowing a more efficient translation by keeping track of the translation status.

type ConcreteAF = DungAF ConcreteArg

An argumentation framework (AF) instantiated with ConcreteArg.

type LConcreteAF = DungAF LConcreteArg

An argumentation framework (AF) instantiated with LConcreteArg.

Translation functions

translate :: CAES -> ConcreteAF

Translation function. It translate an arbitrary cycle-free Carneades argument Evaluation Structure (CAES) into a Dung argumentation framework (instantiated with a ConcreteArg)

translate' :: CAES -> LConcreteAF

Mainly, for testing purposes. This function behaves exactly like translate, but retains the labels.

Correspondence properties

Informally, the correspondence properties below state that every argument and proposition in a CAES, after translation, will have a corresponding argument and keep the same acceptability status.

If the translation function is a correct implementation, the Haskell implementation of the correspondence properties should always return True. However to constitute an actual (mechanised) proof we would need to convert the translation and the implementation of the correspondence properties in Haskell to a theorem prover like Agda.

See Section 4.4 of the paper for the formally stated properties.

corApp :: CAES -> Bool

Correspondence of the applicability of arguments.

corAcc :: CAES -> Bool

Correspondence of the acceptability of propositional literals, including assumptions.