Safe Haskell | None |
---|

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)

- generatedArgs =
*emptyset*. - sortedArgs = Topological sort of arguments on its dependency graph.
- 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*

- type ConcreteArg = Either PropLiteral Argument
- type LConcreteArg = (Bool, ConcreteArg)
- type ConcreteAF = DungAF ConcreteArg
- type LConcreteAF = DungAF LConcreteArg
- translate :: CAES -> ConcreteAF
- translate' :: CAES -> LConcreteAF
- corApp :: CAES -> Bool
- corAcc :: CAES -> Bool

# 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.