CarneadesIntoDung (empty) → 0.9
raw patch · 5 files changed
+406/−0 lines, 5 filesdep +CarneadesDSLdep +Dungdep +basesetup-changed
Dependencies added: CarneadesDSL, Dung, base, containers, fgl
Files
- CarneadesIntoDung.cabal +37/−0
- LICENSE +30/−0
- Language/CarneadesIntoDung/Examples.hs +107/−0
- Language/CarneadesIntoDung/Translation.hs +230/−0
- Setup.hs +2/−0
+ CarneadesIntoDung.cabal view
@@ -0,0 +1,37 @@+name: CarneadesIntoDung+category: Argumentation, Embedded, AI+version: 0.9+license: BSD3+cabal-version: >= 1.6+license-file: LICENSE+author: Bas van Gijzel, Henrik Nilsson+maintainer: Bas van Gijzel <bmv@cs.nott.ac.uk>+stability: experimental+homepage: http://www.cs.nott.ac.uk/~bmv/CarneadesIntoDung/+copyright: Copyright (C) 2013 Bas van Gijzel+synopsis: A translation from the Carneades argumentation model into Dung's AFs.+description: A translation from the Carneades argumentation model + (http://hackage.haskell.org/package/CarneadesDSL) into Dung's + argumentation frameworks (http://hackage.haskell.org/package/Dung). + This package provides a translation function and correspondence+ properties. See "Towards a framework for the implementation and+ verification of translations between argumentation models" by + Bas van Gijzel and Henrik Nilsson or the package's homepage. +build-type: Simple++Library+ build-depends:+ base >= 4 && < 5,+ containers >= 0.3 && < 0.6,+ fgl >= 5.4.2.4 && < 5.5,+ CarneadesDSL >= 1.2,+ Dung >= 0.9+ ++ exposed-modules:+ Language.CarneadesIntoDung.Translation + Language.CarneadesIntoDung.Examples ++source-repository head+ Type: git+ Location: https://github.com/nebasuke/CarneadesIntoDung
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c)2013, Bas van Gijzel++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Bas van Gijzel, nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Language/CarneadesIntoDung/Examples.hs view
@@ -0,0 +1,107 @@+-- | This is the examples module accompanying the implementation of the +-- translation from the Carneades argumentation model into Dung's +-- argumentation frameworks. +-- +-- This module contains a collection of examples, showing how to translate +-- an existing Carneades Argument Evaluation Structure (CAES) into an argumentation +-- framework. +-- +-- To run these examples, or your own: start GHCi and do the following: +-- +-- @\:l Language.CarneadesIntoDung.Examples@ +-- + +module Language.CarneadesIntoDung.Examples + ( + -- *Example translation + -- |We use the example CAES as defined in "Language.Carneades.ExampleCAES". + caes, + exTrans, exTrans', + -- *Correspondence properties + corProp, + ) + where +import Language.CarneadesIntoDung.Translation +import Language.Dung.AF +import Language.Carneades.CarneadesDSL +import Language.Carneades.ExampleCAES + +-- |Translation of the example CAES 'caes'. +-- The following is the prettified output of the translation, where +-- the five propositions in the middle are the assumptions and 'defeater'. +-- +-- >>> translate caes +-- AF [ +-- Left (True,"murder"), +-- Left (False,"murder"), +-- Right ["kill","intent"] ~[]=>"murder", +-- Left (False,"intent"), +-- Left (True,"intent"), +-- Right ["witness2"] ~["unreliable2"]=>"-intent", +-- Right ["witness"] ~["unreliable"]=>"intent", +-- Left (True,"unreliable"), +-- Left (False,"unreliable") +-- , +-- Left (True,"defeater"), +-- Left (True,"kill"), +-- Left (True,"witness"), +-- Left (True,"witness2"), +-- Left (True,"unreliable2")] +-- [ +-- (Left (True,"defeater"), Left (True,"murder")), +-- (Left (True,"defeater"), Left (False,"murder")), +-- (Left (True,"defeater"), Right ["kill","intent"] ~[]=>"murder"), +-- (Left (True,"defeater"), Left (False,"intent")), +-- (Left (True,"defeater"),Left (True,"intent")), +-- (Left (True,"unreliable2"),Right ["witness2"] ~["unreliable2"]=>"-intent"), +-- (Left (True,"defeater"),Left (True,"unreliable")), +-- (Left (True,"defeater"),Left (False,"unreliable")) +-- ] +exTrans :: ConcreteAF +exTrans = translate caes + + + +-- |Translation of the example CAES 'caes', keeping labels. +-- The following is the prettified output of the translation, where +-- the five propositions in the middle are the assumptions and 'defeater'. +-- +-- >>> translate' caes +-- AF [ +-- (False,Left (True,"murder")), +-- (False,Left (False,"murder")), +-- (False,Right ["kill","intent"] ~[]=>"murder"), +-- (False,Left (False,"intent")), +-- (False,Left (True,"intent")), +-- (False,Right ["witness2"] ~["unreliable2"]=>"-intent"), +-- (True,Right ["witness"] ~["unreliable"]=>"intent"), +-- (False,Left (True,"unreliable")), +-- (False,Left (False,"unreliable")) +-- , +-- (True,Left (True,"defeater")), +-- (True,Left (True,"kill")), +-- (True,Left (True,"witness")), +-- (True,Left (True,"witness2")), +-- (True,Left (True,"unreliable2"))] +-- [ +-- ((True,Left (True,"defeater")),(False,Left (True,"murder"))), +-- ((True,Left (True,"defeater")),(False,Left (False,"murder"))), +-- ((True,Left (True,"defeater")), (False,Right ["kill","intent"] ~[]=>"murder")), +-- ((True,Left (True,"defeater")),(False,Left (False,"intent"))), +-- ((True,Left (True,"defeater")),(False,Left (True,"intent"))), +-- ((True,Left (True,"unreliable2")),(False,Right ["witness2"] ~["unreliable2"]=>"-intent")), +-- ((True,Left (True,"defeater")),(False,Left (True,"unreliable"))), +-- ((True,Left (True,"defeater")),(False,Left (False,"unreliable"))) +exTrans' :: LConcreteAF +exTrans' = translate' caes + + + +-- |Combining the correspondence properties. +-- +-- And as expected: +-- +-- >>> corApp caes && corAcc caes +-- True +corProp :: CAES -> Bool +corProp caes = corApp caes && corAcc caes
+ Language/CarneadesIntoDung/Translation.hs view
@@ -0,0 +1,230 @@+-- |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/ +module Language.CarneadesIntoDung.Translation + ( + -- * Basic types + ConcreteArg, LConcreteArg, + ConcreteAF, LConcreteAF, + -- * Translation functions + translate, translate', + -- * 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, corAcc) + where +import Language.Dung.AF hiding (acceptable) +import Language.Carneades.CarneadesDSL +import Language.Carneades.Cyclic +import Data.Graph.Inductive +import Data.List(find, delete, intersect) +import Data.Maybe(fromMaybe) +import Data.Either(lefts, rights) +import Data.Set(fromList) +import Prelude hiding (negate) + +-- |A concrete argument (in an argumentation framework) is either a Carneades +-- propositional literal, or a Carneades argument. +type ConcreteArg = Either PropLiteral Argument + +-- |A labelled version of the concrete argument allowing a more efficient +-- translation by keeping track of the translation status. +type LConcreteArg = (Bool, ConcreteArg) + +-- |An argumentation framework (AF) instantiated with 'ConcreteArg'. +type ConcreteAF = DungAF ConcreteArg + +-- |An argumentation framework (AF) instantiated with 'LConcreteArg'. +type LConcreteAF = DungAF LConcreteArg + +-- |Assumed true argument in the translated AF. It is used to attack arguments +-- that do not uphold their proof standard or have unacceptable premises. +defeater :: LConcreteArg +defeater = (True, Left $ mkProp "defeater") + + +-- | Topological sort of the dependency graph +-- The result is a list, pairing a proposition with all its pro arguments +topSort :: ArgSet -> [(PropLiteral, [Argument])] +topSort g | cyclic g = error "Argumentation graph is cyclic!" + | otherwise = reverse $ topsort' g + +-- |Transforms a Carneades proposition into a Dung argument and labels it 'True'. +propToLArg :: PropLiteral -> LConcreteArg +propToLArg p = (True, Left p) + +-- |Strips the label of both the 'LConcreteArg's in the attack. +stripAttack :: (LConcreteArg, LConcreteArg) -> (ConcreteArg, ConcreteArg) +stripAttack (a, b) = (snd a, snd b) + +-- |Translation function. It translate an arbitrary /cycle-free/ Carneades argument +-- Evaluation Structure (CAES) into a Dung argumentation framework (instantiated +-- with a ConcreteArg) +translate :: CAES -> ConcreteAF +translate caes@(CAES (argSet, (assumptions, _), _)) + = AF (map snd args) (map stripAttack attacks) + where AF args attacks = argsToAF (topSort argSet) + caes + (AF (defeater : map propToLArg assumptions) []) + + +-- |Mainly, for testing purposes. This function behaves exactly like 'translate', +-- but retains the labels. +translate' :: CAES -> LConcreteAF +translate' caes@(CAES (argSet, (assumptions, _), _)) + = AF args attacks + where AF args attacks = argsToAF (topSort argSet) + caes + (AF (defeater : map propToLArg assumptions) []) + + +-- |Retrieves the arguments con the given proposition 'p'. +conArgs :: PropLiteral -> [(PropLiteral, [Argument])] -> (PropLiteral, [Argument]) +conArgs p argList = fromMaybe (negate p, []) (find ((== negate p) . fst) argList) + +-- |Corresponds to the whole of 3. of the above algorithm (or Algorithm 4.1 in +-- the paper) +-- +-- If there are no more arguments to process, the translated AF is returned. + +-- If there is a propositional literal left, but it is an assumption, it has +-- already been translated and does not need to be considered. +-- +-- Otherwise, collect all pro and con arguments for p (con arguments are obtained +-- by calling 'conArgs') and remove them from @argList@. The translation is then +-- done in four steps. 'transApps' is called to translate the applicability part of +-- the pro and con arguments. 'transAcc' is called to translate the acceptability of +-- p and the opposite of p (note that the order of applicable arguments is switched +-- for translating the acceptability of the opposite of p). The results of these +-- four calls are collected and used in the recursive step of 'argsToAF'. +argsToAF :: [(PropLiteral, [Argument])] -> CAES -> LConcreteAF -> LConcreteAF +argsToAF [] _ transAF = transAF +argsToAF (pro@(p, proArgs) : argList) caes@(CAES (_, (assumptions, _), _)) (AF args defs) + | p `elem` assumptions = argsToAF argList caes (AF args defs) + | otherwise = + let con = conArgs p argList + (proAppArgs, proDefs) = transApps args pro + (conAppArgs, conDefs) = transApps args con + (newArgPro, proDefs') = transAcc p proAppArgs conAppArgs caes + (newArgCon, conDefs') = transAcc (negate p) conAppArgs proAppArgs caes + argList' = delete con argList + in argsToAF argList' caes + (AF (newArgPro : newArgCon : proAppArgs ++ conAppArgs ++ args) + (proDefs' ++ conDefs' ++ proDefs ++ conDefs ++ defs)) + +-- |Filters out propositional literals that have been labelled 'True'. +accProps :: [LConcreteArg] -> [PropLiteral] +accProps [] = [] +accProps ((True, Left p) : ls) = p : accProps ls +accProps ((True, Right _) : ls) = accProps ls +accProps ((False, _) : ls) = accProps ls + +-- |This function takes two arguments, a list of already translated arguments +-- (including the translated premises and exceptions) and a proposition +-- paired with its to be translated arguments. It collects the results +-- of the transApp function, which does the main work. +transApps :: [LConcreteArg] -> (PropLiteral, [Argument]) -> ([LConcreteArg], [(LConcreteArg, LConcreteArg)]) +transApps tArgs (p, args) = + let tr = map (transApp tArgs p) args + in (map fst tr, concatMap snd tr) + +-- |Given a list of already translated arguments and a propositional literal, +-- an argument (pro the propositional literal) is translated into a Dung argument +-- and a possibly empty list of attackers. +transApp :: [LConcreteArg] -> PropLiteral -> Argument -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) +transApp tArgs p a@(Arg (prems, excs, c)) + | accProps tArgs `intersect` prems /= prems = ((False, Right a), [(defeater, (False, Right a))]) + | otherwise = + let acceptableExceptions = filter (\ (b, arg) -> b && either (`elem` excs) (const False) arg) tArgs + applicableArg = (null acceptableExceptions, Right a) + defeats = map (\ argExc -> (argExc, applicableArg)) acceptableExceptions + in (applicableArg, defeats) + +-- |Determines the maximum weight of a list of applicable arguments (assumed +-- to have the same conclusion). +maxWeight :: [LConcreteArg] -> CAES -> Double +maxWeight as caes@(CAES (_, (_, argWeight), _)) + = foldl max 0 [argWeight a | (True, Right a) <- as] + + +-- |This function expects the following arguments: a propositional literal at +-- question, a list of pro arguments (labelled 'True', and thus acceptable in +-- the current AF), a list of con arguments (acceptable in the current AF) and +-- a CAES. The result will be an argument corresponding to the proposition and +-- a list of attacks. +transAcc :: PropLiteral -> [LConcreteArg] -> [LConcreteArg] -> CAES -> (LConcreteArg, [(LConcreteArg, LConcreteArg)]) +transAcc c [] conArgs caes = ((False, Left c), [(defeater, (False, Left c))]) -- no applicable argument for p +transAcc c ((_, Left _): proArgs) conArgs caes = error "Proposition in the list of applicable arguments" +transAcc c ((False, _) : proArgs) conArgs caes = transAcc c proArgs conArgs caes +transAcc c proArgs@((True, _) : proArgs') conArgs caes@(CAES (_, _, standard)) + | standard c == Scintilla = ((True, Left c), []) -- there is an applicable argument for p, thus acceptable under Scintilla + | standard c == Preponderance && + maxWeight proArgs caes > maxWeight conArgs caes = ((True, Left c), []) + | standard c == ClearAndConvincing && + maxWeight proArgs caes > alpha && + maxWeight proArgs caes > maxWeight conArgs caes + beta = ((True, Left c), []) + | standard c == BeyondReasonableDoubt && + maxWeight proArgs caes > alpha && + maxWeight proArgs caes > maxWeight conArgs caes + beta && + maxWeight conArgs caes < gamma = ((True, Left c), []) + | standard c == DialecticalValidity && null conArgs = ((True, Left c), []) + | otherwise = ((False, Left c), [(defeater, (False, Left c))]) + +-- |Correspondence of the applicability of arguments. +corApp :: CAES -> Bool +corApp caes@(CAES (argSet, _, _)) = + let translatedCAES = translate caes + applicableArgs = filter (`applicable` caes) + (getAllArgs argSet) + transArgs = rights $ groundedExt translatedCAES + in fromList applicableArgs == fromList transArgs + +-- |Correspondence of the acceptability of propositional literals, including +-- assumptions. +corAcc :: CAES -> Bool +corAcc caes@(CAES (argSet, (assumptions, _), _)) = + let translatedCAES = translate caes + acceptableProps = filter (\ p -> p `acceptable` caes || + p `elem` assumptions) + (getProps argSet) + transProps = lefts $ delete (Left $ mkProp "defeater") + (groundedExt translatedCAES ) + in fromList acceptableProps == fromList transProps
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple +main = defaultMain