| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.CarneadesIntoDung.Translation
Description
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 Argument Source
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 ConcreteArg Source
An argumentation framework (AF) instantiated with ConcreteArg.
type LConcreteAF = DungAF LConcreteArg Source
An argumentation framework (AF) instantiated with LConcreteArg.
Translation functions
translate :: CAES -> ConcreteAF Source
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 Source
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.