CarneadesIntoDung-1.0: A translation from the Carneades argumentation model into Dung's AFs.

Safe HaskellNone




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 ArgumentSource

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

type LConcreteArg = (Bool, ConcreteArg)Source

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

type ConcreteAF = DungAF ConcreteArgSource

An argumentation framework (AF) instantiated with ConcreteArg.

type LConcreteAF = DungAF LConcreteArgSource

An argumentation framework (AF) instantiated with LConcreteArg.

Translation functions

translate :: CAES -> ConcreteAFSource

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

translate' :: CAES -> LConcreteAFSource

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 -> BoolSource

Correspondence of the applicability of arguments.

corAcc :: CAES -> BoolSource

Correspondence of the acceptability of propositional literals, including assumptions.