diff --git a/CHANGELOG b/CHANGELOG
new file mode 100644
--- /dev/null
+++ b/CHANGELOG
@@ -0,0 +1,17 @@
+0.9 => 1.0
+=============
+This package version is now compatible with the translation package CarneadesIntoDung. 
+See http://hackage.haskell.org/package/CarneadesIntoDung/
+
+This package has furthermore been significantly extended and now includes:
+
+* Preferred, stable and semi-stable semantics along with all definitions from
+   Caminada's paper "An Algorithm for Computing Semi-Stable Semantics".
+
+* An Input module, allowing files in standard CEGARTIX/PrefSat format to be parsed.
+
+* An Output module, allowing AFs in this package to be outputted in standard
+  CEGARTIX/PrefSat format.
+
+* A main executable, allowing input files to be read, argumentation frameworks
+  to be outputted and evaluated.
diff --git a/Dung.cabal b/Dung.cabal
--- a/Dung.cabal
+++ b/Dung.cabal
@@ -1,31 +1,47 @@
 name:          Dung
 category:      Argumentation, Embedded, AI
-version:       0.9
+version:       1.0
 license:       BSD3
-cabal-version: >= 1.2
+cabal-version: >= 1.6
 license-file:  LICENSE
 author:        Bas van Gijzel
 maintainer:    Bas van Gijzel <bmv@cs.nott.ac.uk>
 stability:     experimental
 homepage:      http://www.cs.nott.ac.uk/~bmv/Dung/
-copyright:     Copyright (C) 2013 Bas van Gijzel
+copyright:     Copyright (C) 2014 Bas van Gijzel
 synopsis:      An implementation of the Dung argumentation frameworks.
 description:   An implementation of Dung's argumentation frameworks, an abstract argumentation model used to either directly represent conflicting information, or used as
                a translation target for more complex (structured) argumentation models. For an introduction to Dung's frameworks see 
                <http://en.wikipedia.org/wiki/Argumentation_framework> and Dung's paper from 1995: \"On the acceptability of arguments and its fundamental role
                in nonmonotonic reasoning, logic programming, and n-person games\", Artificial Intelligence 77: 321-357.
-               For the paper accompanying this library see \"Towards a framework for the implementation and verification of translations between argumentation
-               models\" available at <http://www.cs.nott.ac.uk/~bmv/Dung/>.
+               For the papers accompanying this library see \"Towards a framework for the implementation and verification of translations between argumentation
+               models\" and \"A principled approach to the implementation of argumentation models\", available at <http://www.cs.nott.ac.uk/~bmv/Dung/>.
 
 build-type:    Simple
 
+Extra-Source-Files:
+                           CHANGELOG
+
 Library
   build-depends:
     base                   >= 4        && < 5,
-    containers             >= 0.3      && < 0.6
+    containers             >= 0.3      && < 0.6,
+    cmdargs                >= 0.10.2,
+    parsec                 >= 3
 
+  hs-source-dirs:
+    src
+
   exposed-modules:
     Language.Dung.AF
     Language.Dung.Examples
-    
+    Language.Dung.Output
+    Language.Dung.Input
 
+Executable dungell
+  main-Is:                 Main.hs
+  hs-source-dirs:          src
+
+source-repository head
+  Type:     git
+  Location: https://github.com/nebasuke/Dung
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c)2013, Bas van Gijzel
+Copyright (c)2014, Bas van Gijzel
 
 All rights reserved.
 
@@ -13,7 +13,7 @@
       disclaimer in the documentation and/or other materials provided
       with the distribution.
 
-    * Neither the name of Bas van Gijzel, Henrik Nilsson, nor the names of other
+    * 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.
 
diff --git a/Language/Dung/AF.hs b/Language/Dung/AF.hs
deleted file mode 100644
--- a/Language/Dung/AF.hs
+++ /dev/null
@@ -1,121 +0,0 @@
--- | This module implements Dung's argumentation frameworks. 
-module Language.Dung.AF 
- (
-    -- * Basic definitions  
-   DungAF(..), 
-   setAttacks, conflictFree, acceptable, f, admissible, unattacked, attacked, 
-   -- * Grounded semantics through fixpoints and labelling
-   groundedF, Status(..), grounded, groundedExt)
- where
-import Data.List (intersect, (\\))
-
-
--- |An abstract argumentation framework is a set of arguments 
--- (represented as a list) and an attack relation on these arguments. 
-data DungAF arg = AF [arg] [(arg, arg)]
-  deriving (Eq, Show)
-
-
--- |Given an argumentation framework, determines whether args 
--- (subset of the arguments in the AF), attacks an argument arg (in the AF).
-setAttacks :: Eq arg => DungAF arg -> [arg] -> arg -> Bool
-setAttacks (AF _ def) args arg 
-  = or [b == arg | (a, b) <- def, a `elem` args] 
-
--- |Given an argumentation framework, determines whether args 
--- (subset of the arguments in the AF) is conflict-free.
-conflictFree :: Eq arg => DungAF arg -> [arg] -> Bool
-conflictFree (AF _ def) args 
-  = null [(a,b) | (a, b) <- def, a `elem` args, b `elem` args] 
-
-  
--- |Given an argumentation framework, determines whether an  
--- argument is acceptable with respect to a list of 'args' (subset of the arguments in the AF). 
-acceptable :: Eq arg => DungAF arg -> arg -> [arg] -> Bool
-acceptable af@(AF _ def) a args 
-  = and [setAttacks af args b | (b, a') <- def, a == a']
-
--- |Given an argumentation framework, determines whether an  
--- argument is acceptable with respect to 'args' (subset of the arguments in the AF). 
-f :: Eq arg => DungAF arg -> [arg] -> [arg]
-f af@(AF args' _) args = [a | a <- args', acceptable af a args]  
-
--- Returns 'True' if 'xs' is a subset of 'ys'
-subset :: Eq a => [a] -> [a] -> Bool
-xs `subset` ys = null (xs \\ ys)
-
--- |Given an argumentation framework, determines whether 
--- the set of arguments 'args' (subset of the arguments in the AF) is admissible,
--- i.e. if 'args' is 'conflictFree' and args is a subset of @f af args@
-admissible :: Eq arg =>  DungAF arg -> [arg] -> Bool
-admissible af args = conflictFree af args && args `subset` f af args 
-
--- alternatively: 
--- if 'args' is 'conflictFree' and and each argument in args is acceptable with respect to args.
--- admissible af args = conflictFree af args && and [acceptable af arg args | arg <- args]
-
--- |Given a characteristic function f, computes the grounded extension
--- by iterating on the empty set (list) until it reaches a fixpoint.
-groundedF :: Eq arg => ([arg] -> [arg]) -> [arg]
-groundedF f = groundedF' f []
-  where  groundedF' f args 
-           | f args == args  = args
-           | otherwise       = groundedF' f (f args)
-
-
--- |Given a list of arguments that are 'Out' in an argumentation framework af, 
--- an argument 'arg' is unattacked if the list of its attackers, ignoring the outs, is empty. 
-unattacked :: Eq arg => [arg] -> 
-              DungAF arg -> arg -> Bool
-unattacked outs (AF _ def) arg = 
-  let attackers = [a | (a, b) <- def, arg == b]
-  in null (attackers \\ outs)
-
--- |Given a list of arguments that are 'In' in an argumentation framework af, 
--- an argument 'arg' is attacked if there exists an attacker that is 'In'.
-attacked :: Eq arg => [arg] -> 
-            DungAF arg -> arg -> Bool
-attacked ins (AF _ def) arg = 
-  let attackers = [a | (a, b) <- def, arg == b]
-  in not (null (attackers `intersect` ins))
-
-  
--- |Labelling of arguments.
-data Status = In | Out | Undecided
-  deriving (Eq, Show)
-
--- |Computes the grounded labelling for a Dung argumentation framework,
--- returning a list of arguments with statuses.
--- 
--- Based on section 4.1 of Proof Theories and Algorithms for Abstract Argumentation Frameworks
--- by Modgil and Caminada
-grounded :: Eq arg => DungAF arg -> [(arg, Status)]
-grounded af@(AF args _) = grounded' [] [] args af
- where 
- grounded' :: Eq a => [a] -> [a] -> 
-              [a] -> DungAF a -> [(a, Status)]
- grounded' ins outs [] _   
-  =    map (\ x -> (x, In)) ins 
-    ++ map (\ x -> (x, Out)) outs
- grounded' ins outs args af  = 
-   let newIns   = filter (unattacked outs af)  args
-       newOuts  = filter (attacked ins af)     args
-   in if null (newIns ++ newOuts) 
-      then  map (\ x -> (x, In)) ins
-        ++  map (\ x -> (x, Out)) outs 
-        ++  map (\ x -> (x, Undecided)) args
-      else grounded' (ins ++ newIns) 
-                     (outs ++ newOuts) 
-                     (args \\ (newIns ++ newOuts)) 
-                     af
-
--- |The grounded extension of an argumentation framework is just the grounded labelling, 
--- keeping only those arguments that were labelled 'In'.
-groundedExt :: Eq arg => DungAF arg -> [arg]
-groundedExt af = [arg | (arg, In) <- grounded af] 
-
-
-
-
-
-
diff --git a/Language/Dung/Examples.hs b/Language/Dung/Examples.hs
deleted file mode 100644
--- a/Language/Dung/Examples.hs
+++ /dev/null
@@ -1,126 +0,0 @@
--- | This is the examples module accompanying the implementation of Dung's 
--- argumentation frameworks. 
---
--- This module contains a collection of examples, showing how to define 
--- arguments, argumentation frameworks and how to use the standard definitions.
---
--- To run these examples, or your own: start GHCi and do the following:
---
--- @\:l Language.Dung.Examples@
--- 
-module Language.Dung.Examples 
-  (
-   -- * Example uses of the basic definitions 
-   AbsArg, exampleAF, exampleAF2,
-   -- * Example uses of the fixpoint definitions
-   faf)
- where
-import Language.Dung.AF
-
--- | The simplest abstract argument is an argument identifiable by its name
-type AbsArg = String 
-
--- @a = \"A\"@, @b = \"B\"@, @c = \"C\"@
--- * Tests using the above argumentation frameworks:
-a, b, c :: AbsArg 
-a = "A"
-b = "B"
-c = "C"
-
-
--- |Example AF: A -> B -> C 
-exampleAF :: DungAF AbsArg
-exampleAF = AF [a, b, c] [(a, b), (b, c)]
-
--- |Example AF: A \<-> B
---
--- Now follow a few example outputs using the above argumentation frameworks.
---
--- [setAttacks:]
--- 
---  @[a,b]@ 'setAttacks' @c@ in the argumentation framework 'exampleAF':
--- 
--- >>> setAttacks exampleAF [a,b] c
--- True
---
--- >>> setAttacks exampleAF [b,c] a
--- False
--- 
--- >>> setAttacks exampleAF2 [] b
--- False
---
--- [conflictFree:]
---
--- @\[a,c\]@ is 'conflictFree' in the argumentation framework 'exampleAF':
--- 
--- >>> conflictFree exampleAF [a,c]
--- True
---
--- >>> conflictFree exampleAF [a,b,c]
--- False
---
--- >>> conflictFree exampleAF2 [a,b]
--- False
--- 
--- [acceptable:]
---
--- @c@ is acceptable w.r.t. @\[a,b\]@ in the argumentation framework 'exampleAF':
---
--- >>> acceptable exampleAF c [a,b]
--- True
--- 
--- >>> acceptable exampleAF c [] 
--- False
---
--- >>> acceptable exampleAF b [a,b,c] 
--- False
--- 
--- [admissible:]
--- 
--- @\[a,b,c\]@ is admissible in the argumentation framework 'exampleAF':
---
--- >>> admissible exampleAF [a,b,c]
--- False
--- 
--- >>> admissible exampleAF [a,c]
--- True
--- 
--- >>> admissible exampleAF [a]
--- True
---
--- [grounded:]
--- 
--- The grounded labelling of the argumentation framework 'exampleAF':
---
--- >>> grounded exampleAF
--- [("A",In),("C",In),("B",Out)]
--- 
--- >>> grounded exampleAF2
--- [("A",Undecided),("B",Undecided)]
---
--- [groundedExt:]
--- 
--- The grounded extension of the argumentation framework 'exampleAF':
---
--- >>> groundedExt exampleAF
--- ["A", "C"]
--- >>> groundedExt exampleAF2
--- []
-exampleAF2 :: DungAF AbsArg 
-exampleAF2 = AF [a, b] [(a, b), (b, a)]
-
--- |fixed point function for a specific argumentation framework,
--- @faf = f exampleAF@.
--- 
--- [groundedF:]
---
--- The grounded extension of the argumentation framework 'exampleAF' using the fixpoint definition:
---
--- >>> groundedF faf
--- ["A","C"]
---
--- >>> groundedF (f exampleAF2)
--- []
-faf :: [AbsArg] -> [AbsArg]
-faf = f exampleAF
-
diff --git a/src/Language/Dung/AF.hs b/src/Language/Dung/AF.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Dung/AF.hs
@@ -0,0 +1,424 @@
+-- | This module implements Dung's argumentation frameworks. 
+module Language.Dung.AF 
+ (
+    -- * Basic definitions  
+   DungAF(..), 
+   setAttacks, aplus, amin, argplus, argmin, 
+   conflictFree, acceptable, f, admissible, 
+   -- * Grounded, preferred, semi-stable and stable semantics through fixpoints
+   groundedF,
+   -- * Basic labelling definitions
+   -- |The following functions are implementations of the 
+   -- definitions in \"An algorithm for Computing Semi-Stable 
+   -- Semantics\" in \"Symbolic and Quantitative Approaches to Reasoning with
+   -- Uncertainty\", pages 222--234, Springer, 2007.
+   Status(..), Labelling(..), 
+   inLab, outLab, undecLab, 
+   allIn, allOut, allUndec,
+   unattacked, attacked, 
+   labAttackers, illegallyIn, illegallyOut, illegallyUndec,
+   legallyIn, legallyOut, legallyUndec,
+   isAdmissible, isComplete, isPreferred, isStable, isSemiStable,
+   transitionStep, terminatedTransition, superIllegallyIn,
+   -- * Grounded, preferred, semi-stable and stable labellings
+   -- |The following functions are implementations of the 
+   -- definitions in \"An algorithm for Computing Semi-Stable 
+   -- Semantics\" in \"Symbolic and Quantitative Approaches to Reasoning with 
+   -- Uncertainty\", pages 222--234, Springer, 2007 and Section 4.1 of Proof 
+   -- Theories and Algorithms for Abstract Argumentation Frameworks by Modgil 
+   -- and Caminada.
+   grounded, groundedExt, complete, preferred, stable, semiStable, 
+   completeExt, preferredExt, stableExt, semiStableExt
+ )
+ where
+import Data.List (intersect, (\\), partition, delete, nub, sort)
+
+
+-- |An abstract argumentation framework is a set of arguments 
+-- (represented as a list) and an attack relation on these arguments. 
+data DungAF arg = AF [arg] [(arg, arg)]
+  deriving (Eq, Show)
+
+-- |Given an argumentation framework, determines whether args 
+-- (subset of the arguments in the AF), attacks an argument arg (in the AF).
+setAttacks :: Eq arg => DungAF arg -> [arg] -> arg -> Bool
+setAttacks (AF _ def) args arg 
+  = or [b == arg | (a, b) <- def, a `elem` args] 
+
+-- |Given an argumentation framework, determines the set of arguments
+-- that are attacked by an argument (in the AF).
+aplus :: Eq arg => DungAF arg -> arg -> [arg]
+aplus (AF args atk) a = [b | (a', b) <- atk, a == a']
+
+-- |Given an argumentation framework, determines the set of arguments
+-- attacking an argument (in the AF).
+amin :: Eq arg => DungAF arg -> arg -> [arg]
+amin (AF args atk) a = [b | (b, a') <- atk, a == a']
+
+-- |Given an argumentation framework, determines the set of arguments
+-- that are attacked by the given subset of arguments (in the AF).
+argplus :: Eq arg => DungAF arg -> [arg] -> [arg]
+argplus af = nub . concatMap (aplus af)
+
+-- |Given an argumentation framework, determines the set of arguments
+-- that attack a given subset of arguments (in the AF).
+argmin :: Eq arg => DungAF arg -> [arg] -> [arg]
+argmin af = nub . concatMap (amin af)
+
+-- |Given an argumentation framework, determines whether args 
+-- (subset of the arguments in the AF) is conflict-free.
+conflictFree :: Eq arg => DungAF arg -> [arg] -> Bool
+conflictFree (AF _ def) args 
+  = null [(a,b) | (a, b) <- def, a `elem` args, b `elem` args] 
+
+-- |Given an argumentation framework, determines whether an  
+-- argument is acceptable with respect to a list of 'args' (subset of the arguments in the AF). 
+acceptable :: Eq arg => DungAF arg -> arg -> [arg] -> Bool
+acceptable af@(AF _ def) a args 
+  = and [setAttacks af args b | (b, a') <- def, a == a']
+
+-- |Given an argumentation framework, returns the set of arguments  
+-- that are acceptable with respect to 'args' (subset of the arguments in the AF). 
+f :: Eq arg => DungAF arg -> [arg] -> [arg]
+f af@(AF args' _) args = [a | a <- args', acceptable af a args]  
+
+-- Returns 'True' if 'xs' is a subset of 'ys'
+subset :: Eq a => [a] -> [a] -> Bool
+xs `subset` ys = null (xs \\ ys)
+
+-- |Given an argumentation framework, determines whether 
+-- the set of arguments 'args' (subset of the arguments in the AF) is admissible,
+-- i.e. if 'args' is 'conflictFree' and args is a subset of @f af args@
+admissible :: Eq arg =>  DungAF arg -> [arg] -> Bool
+admissible af args = conflictFree af args && args `subset` f af args 
+
+-- alternatively: 
+-- if 'args' is 'conflictFree' and each argument in args is acceptable with
+-- respect to args. 
+-- admissible af args = conflictFree af args && 
+--                      and [acceptable af arg args | arg <- args]
+
+-------------------------------------------------------------------------------
+--- Implementations of semantics through fixpoints or generation of complete--- 
+---                              extensions                                 ---
+-------------------------------------------------------------------------------
+
+-- |Given a characteristic function f, computes the grounded extension
+-- by iterating on the empty set (list) until it reaches a fixpoint.
+groundedF :: Eq arg => ([arg] -> [arg]) -> [arg]
+groundedF f = groundedF' f []
+  where  groundedF' f args 
+           | f args == args  = args
+           | otherwise       = groundedF' f (f args)
+
+
+
+-------------------------------------------------------------------------------
+-- The following functions are implementations of the 
+-- definitions in \"An algorithm for Computing Semi-Stable 
+-- Semantics\" in \"Symbolic and Quantitative Approaches to 
+-- Reasoning with Uncertainty\", pages 222--234, Springer, 2007.
+-------------------------------------------------------------------------------
+
+-- |Labelling status of arguments.
+data Status = In | Out | Undecided
+  deriving (Eq, Show, Ord)
+
+-- Definition 4
+-- |Labelling of arguments. 
+type Labelling arg = [(arg,Status)]
+
+
+-- Just below Definition 4, functions on a labelling:
+-- in(Lab)
+-- |Given a labelling of arguments, give back the arguments labelled 'In'.
+inLab :: Labelling arg -> [arg]
+inLab labs = [a | (a, In) <- labs]
+
+-- out(Lab)
+-- |Given a labelling of arguments, give back the arguments labelled 'Out'.
+outLab :: Labelling arg -> [arg]
+outLab labs = [a | (a, Out) <- labs]
+
+-- undec(lab)
+-- |Given a labelling of arguments, give back the arguments labelled 
+-- 'Undecided'.
+undecLab :: Labelling arg -> [arg]
+undecLab labs = [a | (a, Undecided) <- labs]
+
+
+-- Just below Definition 4, Caminada distinguishes three special kinds of labelling.
+
+-- |The allIn labelling is a 'Labelling' that labels every argument 'In'.
+allIn :: [arg] -> Labelling arg
+allIn = map (\ a -> (a, In))
+
+-- |The allOut labelling is a 'Labelling' that labels every argument 'Out'.
+allOut :: [arg] -> Labelling arg
+allOut = map (\ a -> (a, Out))
+
+-- |The allUndec labelling is a 'Labelling' that labels every argument 'Undecided'.
+allUndec :: [arg] -> Labelling arg
+allUndec = map (\ a -> (a, Undecided))
+
+-- |Given a list of arguments that are 'Out' in an argumentation framework af, 
+-- an argument 'arg' is unattacked if the list of its attackers, ignoring the outs, is empty. 
+unattacked :: Eq arg => [arg] -> 
+              DungAF arg -> arg -> Bool
+unattacked outs (AF _ def) arg = 
+  let attackers = [a | (a, b) <- def, arg == b]
+  in null (attackers \\ outs)
+
+-- |Given a list of arguments that are 'In' in an argumentation framework af, 
+-- an argument 'arg' is attacked if there exists an attacker that is 'In'.
+attacked :: Eq arg => [arg] -> 
+            DungAF arg -> arg -> Bool
+attacked ins (AF _ def) arg = 
+  let attackers = [a | (a, b) <- def, arg == b]
+  in not (null (attackers `intersect` ins))
+
+
+-- |Computes the grounded labelling for a Dung argumentation framework,
+-- returning a (unique) list of arguments with statuses.
+-- 
+-- Based on section 4.1 of Proof Theories and Algorithms for Abstract Argumentation Frameworks
+-- by Modgil and Caminada.
+grounded :: Eq arg => DungAF arg -> Labelling arg
+grounded af@(AF args _) = grounded' [] [] args af
+ where 
+ grounded' :: Eq a => [a] -> [a] -> 
+              [a] -> DungAF a -> [(a, Status)]
+ grounded' ins outs [] _   
+  =    allIn ins 
+    ++ allOut outs
+ grounded' ins outs args af  = 
+   let newIns  = filter (unattacked outs af) args
+       newOuts = filter (attacked ins af) args
+   in if null (newIns ++ newOuts) 
+      then allIn ins
+        ++ allOut outs 
+        ++ allUndec args
+      else grounded' (ins ++ newIns) 
+                     (outs ++ newOuts) 
+                     (args \\ (newIns ++ newOuts)) 
+                     af
+
+-- |The grounded extension of an argumentation framework is just the grounded labelling, 
+-- keeping only those arguments that were labelled 'In'.
+groundedExt :: Eq arg => DungAF arg -> [arg]
+groundedExt af = [arg | (arg, In) <- grounded af] 
+
+-- |Given an argumentation framework, determines the list of attackers of an argument, 
+-- from a given labelling, returning the labelled attackers. 
+labAttackers :: Eq arg => DungAF arg -> arg -> Labelling arg -> Labelling arg
+labAttackers (AF args atk) a labs = [lab | lab@(b, _) <- labs, (b, a) `elem` atk]
+
+-- Definition 5.1 of Caminada
+-- |Given an AF and 'Labelling',
+-- an argument a (in the AF) is illegally 'In' iff a is labelled 'In',
+-- but not all its attackers are labelled 'Out'.
+illegallyIn :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool
+illegallyIn af labs (a, In) = not . null $ [lab | lab@(_, l) <- labAttackers af a labs, l /= Out]
+illegallyIn _  _     _      = False
+
+-- Definition 5.2 of Caminada
+-- |Given an AF and 'Labelling',
+-- an argument a (in the AF) is illegally 'Out' iff a is labelled 'Out'
+-- but does not have an attacker labelled 'In'.
+illegallyOut :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool
+illegallyOut af labs (a, Out) = null [lab | lab@(_, In) <- labAttackers af a labs]
+illegallyOut _  _    _        = False
+
+-- Definition 5.3 of Caminada
+-- |Given an AF and 'Labelling',
+-- an argument a (in the AF) is illegally 'Undecided' iff a is labelled 'Undecided' 
+-- but either all its attackers are labelled 'Out' 
+-- or it has an attacker that is labelled 'In'.
+illegallyUndec :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool
+illegallyUndec af labs (a, Undecided) = and [l == Out | (_, l) <- labAttackers af a labs]
+                                        || (not . null) [lab | lab@(_, In) <- labAttackers af a labs] 
+illegallyUndec _  _    _              = False
+
+
+-- Just below Definition 5.3 of Caminada
+-- The implementation of a 'Labelling' that has no illegal
+-- arguments is given as 'isComplete', further below.
+
+-- Just below Definition 5.3 of Caminada
+-- |Given an AF and 'Labelling',
+-- an argument a (in the AF) is legally 'In' iff a is labelled 'In' 
+-- and it's not 'illegallyIn'.
+legallyIn :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool
+legallyIn af labs arg@(_, In) = not $ illegallyIn af labs arg
+legallyIn _  _    _           = False
+
+-- Just below Definition 5.3 of Caminada
+-- |Given an AF and 'Labelling',
+-- an argument a (in the AF) is legally 'Out' iff a is labelled 'Out' 
+-- and it's not 'illegallyOut'.
+legallyOut :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool
+legallyOut af labs arg@(_, Out) = not $ illegallyOut af labs arg
+legallyOut _  _    _            = False
+
+-- Just below Definition 5.3 of Caminada
+-- |Given an AF and 'Labelling',
+-- an argument a (in the AF) is legally 'Undecided' iff a is labelled 'Undecided' 
+-- and it's not 'illegallyUndec'.
+legallyUndec :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool
+legallyUndec af labs arg@(_, Undecided) = not $ illegallyUndec af labs arg
+legallyUndec _  _    _                  = False
+
+-- Definition 6 of Caminada
+-- |Given an AF, an admissible labelling is a 'Labelling' without arguments
+-- that are 'illegallyIn' and without arguments that are 'illegallyOut'.
+isAdmissible :: Eq arg => DungAF arg -> Labelling arg -> Bool
+isAdmissible af labs = null $ 
+                      [lab | lab@(a, In) <- labs, illegallyIn af labs lab] 
+                   ++ [lab | lab@(a, Out) <- labs, illegallyOut af labs lab] 
+
+-- Definition 7 of Caminada
+-- |Given an AF, a complete labelling is a labelling without arguments
+-- that are 'illegallyIn', without arguments that are 'illegallyOut' and 
+-- without arguments that are 'illegallyUndec'.
+isComplete ::  Eq arg => DungAF arg -> Labelling arg -> Bool
+isComplete af labs = null $ 
+                   [lab | lab@(a, In) <- labs, illegallyIn af labs lab] 
+                ++ [lab | lab@(a, Out) <- labs, illegallyOut af labs lab] 
+                ++ [lab | lab@(a, Undecided) <- labs, illegallyUndec af labs lab]
+
+
+-- Definition 8 of Caminada, grounded labelling
+-- |Let 'labs' be a complete labelling, i.e. @isComplete af labs@, we say that 
+-- labs is a grounded labelling iff @inLab labs@ is minimal 
+-- (w.r.t. set inclusion).
+isGrounded :: Eq arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool
+isGrounded af labss labs = isComplete af labs && 
+                           all (inLab labs `subset`) (map inLab labss)
+
+-- Definition 8 of Caminada, preferred labelling
+-- |Let 'labs' be a complete labelling, i.e. @isComplete af labs@, we say that 
+-- labs is a preferred labelling iff @inLab labs@ is maximal 
+-- (w.r.t. set inclusion).
+isPreferred :: Eq arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool
+isPreferred af labss labs = isComplete af labs && 
+                            all (not . (inLab labs `subset` )) (map inLab (delete labs labss))
+
+-- Definition 8 of Caminada, stable labelling
+-- |Let 'labs' be a complete labelling, i.e. 'isComplete af labs', we say that 
+-- labs is a preferred labelling iff @undecLab(labs) == []@
+isStable :: Eq arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool
+isStable af labss labs = isComplete af labs && 
+                         null (undecLab labs)
+                            
+-- Definition 8 of Caminada, semi-stable labelling
+-- |Let 'labs' be a complete labelling, i.e. @isComplete af labs@, we say that 
+-- labs is a semi-stable labelling iff @undecLab labs@ is minimal 
+-- (w.r.t. set inclusion).
+isSemiStable :: Eq arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool
+isSemiStable af labss labs = isComplete af labs && 
+                             all (undecLab labs `subset`) 
+                                 (map undecLab labss)
+
+-- Definition 9 of Caminada
+-- |Given an AF, a labelling labs and an illegally in argument a in the af, 
+-- (i.e. @illegallyIn af a labs@ => True),
+-- a transition step on a in labs consists of the following: 
+-- 1. the label of a is changed from 'In' to 'Out'
+-- 2. for every b in {a} \cup a+, if b is illegally out,
+-- then change the label from b from 'Out' to 'Undecided'
+transitionStep :: Eq arg => DungAF arg -> Labelling arg -> arg -> Labelling arg
+transitionStep af labs a = 
+ let labs' = (a, Out) : delete (a, In) labs -- Step 1
+     bs    = a : aplus af a -- bs = every b in {a} \cup a+
+     (newUndecs, rem) = partition (\ lab@(b, l) -> 
+                                       b `elem` bs
+                                    && illegallyOut af labs' lab)
+                                  labs'
+ in map (\ (a, _) -> (a, Undecided)) newUndecs
+ ++ rem
+
+
+-- Based on Definition 10 of Caminada
+-- Instead of checking termination of a transition sequence
+-- This function implements a check of termination for a specific transition
+-- last . 
+-- |Given an AF, a labelling, labs, is terminated iff labs does not contain any argument that is 
+-- illegally in, i.e. @not (illegallyIn af lab arg)@ for all arg in labs.
+terminatedTransition :: Eq arg => DungAF arg -> Labelling arg -> Bool
+terminatedTransition af labs = not . or $ map (illegallyIn af labs) labs
+
+-- Definition 11 of Caminada
+-- |Given an AF and 'Labelling',
+-- an argument a (in the AF) is superillegally 'In' iff a is labelled 'In',
+-- and it is attacked by an argument that is legally 'In' or legally 'Undecided'.
+superIllegallyIn :: Eq arg => DungAF arg -> Labelling arg -> (arg, Status) -> Bool
+superIllegallyIn af labs (a, In) = 
+  not . null $ 
+    [lab | lab <- labAttackers af a labs, 
+           legallyIn af labs lab || legallyUndec af labs lab]
+superIllegallyIn _  _    _      = False
+
+-- Based on the Algorithm of Caminada
+-- Instead of using a search tree and keeping a list of potential semi-stable
+-- labellings, we remove the checks. 
+-- Note that this actually gives us an algorithm for computing the complete 
+-- labellings, allowing us to then filter out the grounded, preferred,
+-- stable or semi-stable labellings dependent on what should be maximal or 
+-- minimal
+-- |Computes all complete labellings for a Dung argumentation framework. This
+-- is based on Caminada's algorithm for computing semi-stable labellings, 
+-- with all checks removed.
+complete :: Ord arg => DungAF arg -> [Labelling arg]
+complete af@(AF args atk) = 
+ let allInArgs = allIn args
+     complete' :: Eq arg => DungAF arg -> Labelling arg -> [Labelling arg]
+     complete' af labs =
+      case filter (superIllegallyIn af labs) labs of
+            []          -> case filter (illegallyIn af labs) labs of
+                             [] -> [labs]
+                             ills -> concatMap (complete' af) $
+                                       map (transitionStep af labs . fst) 
+                                           ills
+            ((a,_) : _) -> complete' af (transitionStep af labs a)
+ in nub . map sort $ complete' af allInArgs
+
+-- |Computes all preferred labellings for a Dung argumentation framework, by
+-- taking the maximally in complete labellings.
+preferred :: Ord arg => DungAF arg -> [Labelling arg]
+preferred af@(AF args atk) = 
+ let completes = complete af 
+ in filter (isPreferred af completes) completes
+
+-- |Computes all stable labellings for a Dung argumentation framework, by
+-- keeping only those labellings with no 'Undecided' labels.
+stable :: Ord arg => DungAF arg -> [Labelling arg]
+stable af@(AF args atk) = 
+ let completes = complete af 
+ in filter (isStable af completes) completes
+
+-- |Computes all semi-stable labellings for a Dung argumentation framework, by
+-- taking the minimally undecided complete labellings.
+semiStable :: Ord arg => DungAF arg -> [Labelling arg]
+semiStable af@(AF args atk) = 
+ let completes = complete af 
+ in filter (isSemiStable af completes) completes
+
+-- |The complete extension of an argumentation framework is just the complete labelling, 
+-- keeping only those arguments that were labelled 'In'.
+completeExt :: Ord arg => DungAF arg -> [[arg]]
+completeExt af = [[arg | (arg, In) <- c] | c <- complete af]
+
+-- |The preferred extension of an argumentation framework is just the preferred labelling, 
+-- keeping only those arguments that were labelled 'In'.
+preferredExt :: Ord arg => DungAF arg -> [[arg]]
+preferredExt af = [[arg | (arg, In) <- c] | c <- preferred af]
+
+-- |The stable extension of an argumentation framework is just the stable labelling, 
+-- keeping only those arguments that were labelled 'In'.
+stableExt :: Ord arg => DungAF arg -> [[arg]]
+stableExt af = [[arg | (arg, In) <- c] | c <- stable af]
+
+-- |The semi-stable extension of an argumentation framework is just the semi-stable labelling, 
+-- keeping only those arguments that were labelled 'In'.
+semiStableExt :: Ord arg => DungAF arg -> [[arg]]
+semiStableExt af = [[arg | (arg, In) <- c] | c <- semiStable af]
diff --git a/src/Language/Dung/Examples.hs b/src/Language/Dung/Examples.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Dung/Examples.hs
@@ -0,0 +1,321 @@
+-- | This is the examples module accompanying the implementation of Dung's 
+-- argumentation frameworks. 
+--
+-- This module contains a collection of examples, showing how to define 
+-- arguments, argumentation frameworks and how to use the standard definitions.
+--
+-- To run these examples, or your own: start GHCi and do the following:
+--
+-- @\:l Language.Dung.Examples@
+-- 
+module Language.Dung.Examples 
+  (
+   -- * Example uses of the basic definitions 
+   -- |Given @a = \"A\"@, @b = \"B\"@, @c = \"C\"@
+   AbsArg, a, b, c, exampleAF, exampleAF2, 
+   -- * Example uses of the fixpoint definitions
+   faf,
+   -- * Example uses of the basic labelling definitions
+   -- |Given @d = \"D\"@, @e = \"E\"@
+   d, e, exampleAF3, exampleAF4,
+   -- * Example uses of the input functionality
+   exampleAF5,
+   -- * Example uses of the output functionality
+   output, output2, output3, output4, output5
+  )
+ where
+import Language.Dung.AF
+import Language.Dung.Input
+import Language.Dung.Output
+-- | The simplest abstract argument is an argument identifiable by its name
+type AbsArg = String 
+
+
+a, b, c :: AbsArg 
+a = "A"
+b = "B"
+c = "C"
+
+-- |Example AF: A -> B -> C 
+exampleAF :: DungAF AbsArg
+exampleAF = AF [a, b, c] [(a, b), (b, c)]
+
+-- |Example AF: A \<-> B
+--
+-- Now follow a few example outputs using the above argumentation frameworks.
+--
+-- [setAttacks:]
+-- 
+-- @[a,b]@ 'setAttacks' @c@ in the argumentation framework 'exampleAF':
+-- 
+-- >>> setAttacks exampleAF [a,b] c
+-- True
+--
+-- >>> setAttacks exampleAF [b,c] a
+-- False
+-- 
+-- >>> setAttacks exampleAF2 [] b
+-- False
+--
+-- [conflictFree:]
+--
+-- @\[a,c\]@ is 'conflictFree' in the argumentation framework 'exampleAF':
+-- 
+-- >>> conflictFree exampleAF [a,c]
+-- True
+--
+-- >>> conflictFree exampleAF [a,b,c]
+-- False
+--
+-- >>> conflictFree exampleAF2 [a,b]
+-- False
+-- 
+-- [acceptable:]
+--
+-- @c@ is acceptable w.r.t. @\[a,b\]@ in the argumentation framework 'exampleAF':
+--
+-- >>> acceptable exampleAF c [a,b]
+-- True
+-- 
+-- >>> acceptable exampleAF c [] 
+-- False
+--
+-- >>> acceptable exampleAF b [a,b,c] 
+-- False
+-- 
+-- [admissible:]
+-- 
+-- @\[a,b,c\]@ is admissible in the argumentation framework 'exampleAF':
+--
+-- >>> admissible exampleAF [a,b,c]
+-- False
+-- 
+-- >>> admissible exampleAF [a,c]
+-- True
+-- 
+-- >>> admissible exampleAF [a]
+-- True
+--
+-- [grounded:]
+-- 
+-- The grounded labelling of the argumentation frameworks 'exampleAF'
+-- and 'exampleAF2':
+-- 
+-- >>> grounded exampleAF
+-- [("A",In),("C",In),("B",Out)]
+-- 
+-- >>> grounded exampleAF2
+-- [("A",Undecided),("B",Undecided)]
+--
+-- [groundedExt:]
+-- 
+-- The grounded extension of the argumentation frameworks 'exampleAF'
+-- and 'exampleAF2':
+--
+-- >>> groundedExt exampleAF
+-- ["A", "C"]
+-- >>> groundedExt exampleAF2
+-- []
+exampleAF2 :: DungAF AbsArg 
+exampleAF2 = AF [a, b] [(a, b), (b, a)]
+
+-- |fixed point function for a specific argumentation framework,
+-- @faf = f exampleAF@.
+-- 
+-- [groundedF:]
+--
+-- The grounded extension of the argumentation framework 'exampleAF' using the
+-- fixpoint definition:
+--
+-- >>> groundedF faf
+-- ["A","C"]
+--
+-- >>> groundedF (f exampleAF2)
+-- []
+faf :: [AbsArg] -> [AbsArg]
+faf = f exampleAF
+
+d, e :: AbsArg 
+d = "D"
+e = "E"
+
+-- |Left hand side of Fig1. in Caminada.
+-- Arguments are: {a,b,c,d}. 
+-- Attacks: {(a, a), (a, c), (b, c), (c, d)}
+exampleAF3 :: DungAF AbsArg
+exampleAF3 = AF [a, b, c, d] [(a, a), (a, c), (b, c), (c, d)]
+
+-- |Right hand side of Fig1. in Caminada.
+-- Arguments are: {a,b,c,d,e}. 
+-- Attacks: {(a, b), (b, a), (b, c), (c, d), (d, e), (e, c)}
+--
+-- [complete:]
+-- 
+-- The complete labellings of the argumentation framework 'exampleAF3'
+-- and 'exampleAF4':
+-- 
+-- >>> complete exampleAF3
+-- [
+--   [("A",Undecided),("B",In),("C",Out),("D",In)]
+-- ]
+-- 
+-- >>> complete exampleAF4
+-- [
+--   [("A",Out),("B",In),("C",Out),("D",In),("E",Out)],
+--   [("A",In),("B",Out),("C",Undecided),("D",Undecided),("E",Undecided)],
+--   [("A",Out),("B",In),("C",Out),("D",Undecided),("E",Undecided)]
+-- ]
+--
+-- [completeExt:]
+-- 
+-- The complete extensions of the argumentation frameworks 'exampleAF3'
+-- and 'exampleAF4':
+--
+-- >>> completeExt exampleAF3
+-- [
+--   ["B","D"]
+-- ]
+-- >>> completeExt exampleAF4
+-- [
+--   ["B","D"],
+--   ["A"],
+--   ["B"]
+-- ]
+--
+-- [semiStable:]
+-- 
+-- The semi-stable labellings of the argumentation framework 'exampleAF3'
+-- and 'exampleAF4':
+-- 
+-- >>> semiStable exampleAF3
+-- [
+--   [("A",Undecided),("B",In),("C",Out),("D",In)]
+-- ]
+-- 
+-- >>> semiStable exampleAF4
+-- [
+--   [("A",Out),("B",In),("C",Out),("D",In),("E",Out)],
+-- ]
+--
+-- [semiStableExt:]
+-- 
+-- The complete extensions of the argumentation frameworks 'exampleAF3'
+-- and 'exampleAF4':
+--
+-- >>> semiStableExt exampleAF3
+-- [
+--   ["B","D"]
+-- ]
+-- >>> semiStableExt exampleAF4
+-- [
+--   ["B","D"],
+-- ]
+--
+exampleAF4 :: DungAF AbsArg
+exampleAF4 = AF [a, b, c, d, e] [(a, b), (b, a), (b, c), (c, d), (d, e), (e, c)]
+
+-- |Parsed example as given on the CEGARTIX webpage:
+-- <http://www.dbai.tuwien.ac.at/proj/argumentation/cegartix/>.
+-- 
+-- @
+-- arg(a).
+-- arg(b).
+-- arg(c).
+-- arg(d).
+-- arg(e).
+-- arg(f).
+-- arg(g).
+-- att(a,b).
+-- att(c,b).
+-- att(c,d).
+-- att(d,c).
+-- att(d,e).
+-- att(e,g).
+-- att(f,e).
+-- att(g,f).
+-- @
+-- 
+-- This is given as a literal string to 'parseAF'. 
+exampleAF5 :: DungAF AbsArg
+exampleAF5 = case 
+  parseAF 
+    "arg(a).\
+    \arg(b).\
+    \arg(c).\
+    \arg(d).\
+    \arg(e).\
+    \arg(f).\
+    \arg(g).\
+    \att(a,b).\
+    \att(c,b).\
+    \att(c,d).\
+    \att(d,c).\
+    \att(d,e).\
+    \att(e,g).\
+    \att(f,e).\
+    \att(g,f)."
+      of 
+  Left err -> error (show err)
+  Right af -> af
+
+-- |Output 'String' corresponding to 'exampleAF', 
+-- i.e. @toCegartix exampleAF@.
+--
+-- >>> putStr output
+-- arg("A").
+-- arg("B").
+-- arg("C").
+-- att("A","B").
+-- att("B","C").
+output :: String
+output = toCegartix exampleAF
+
+-- |Output 'String' corresponding to 'exampleAF2', 
+-- i.e. @toCegartix exampleAF2@.
+--
+-- >>> putStr output2
+-- arg("A").
+-- arg("B").
+-- att("A","B").
+-- att("B","A").
+output2 :: String
+output2 = toCegartix exampleAF2
+
+-- |Output 'String' corresponding to 'exampleAF3', 
+-- i.e. @toCegartix exampleAF3@.
+--
+-- >>> putStr output3
+-- arg("A").
+-- arg("B").
+-- arg("C").
+-- arg("D").
+-- att("A","A").
+-- att("A","C").
+-- att("B","C").
+-- att("C","D").
+output3 :: String
+output3 = toCegartix exampleAF3
+
+-- |Output 'String' corresponding to 'exampleAF4', 
+-- i.e. @toCegartix exampleAF4@.
+--
+-- >>> putStr output4
+-- arg("A").
+-- arg("B").
+-- arg("C").
+-- arg("D").
+-- arg("E").
+-- att("A","B").
+-- att("B","A").
+-- att("B","C").
+-- att("C","D").
+-- att("D","E").
+-- att("E","C").
+output4 :: String
+output4 = toCegartix exampleAF4
+
+-- |Output 'String' corresponding to 'exampleAF5', 
+-- i.e. @toCegartix exampleAF5@.
+output5 :: String
+output5 = toCegartix exampleAF5
+
diff --git a/src/Language/Dung/Input.hs b/src/Language/Dung/Input.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Dung/Input.hs
@@ -0,0 +1,90 @@
+-- | This is the input module accompanying the implementation of Dung's 
+-- argumentation frameworks. It defines a simple parser for an argumentation framework
+-- that assumes the input file is in CEGARTIX/PrefSat-like format.
+--
+-- Files are assumed to have one argument or attack on each line, ending
+-- in a dot. (Our parser is slightly more relaxed than this and doesn't care about whitespace.)
+--
+-- @att(a1,a2).@ or @arg(a1).@
+--
+-- Argument names are assumed to consist only of letters and numbers.
+-- Arguments used in attacks should be declared separately as well. 
+
+module Language.Dung.Input
+  (
+   -- * Parsing functions
+   parseAF, pAF
+   )
+ where
+import Language.Dung.AF
+import Text.Parsec
+import Text.Parsec.String (Parser)
+import Text.Parsec.Char (char, string)
+import qualified Text.Parsec.Token as P
+import Text.Parsec.Language(haskellStyle)
+import Text.Parsec.Error(errorMessages, messageString)
+import Data.Either (partitionEithers)
+
+lexer :: P.TokenParser ()
+lexer = P.makeTokenParser haskellStyle
+
+whiteSpace :: Parser ()
+whiteSpace = P.whiteSpace lexer
+
+identifier :: Parser String
+identifier = P.identifier lexer
+
+stringLiteral :: Parser String
+stringLiteral = P.stringLiteral lexer
+
+-- |An argument name consists of one or more letters and digits
+-- or a string literal.
+argName :: Parser String
+argName =  try identifier <|> stringLiteral
+
+-- |A complete argument consists of @arg(argName).@
+pArgument :: Parser String
+pArgument = do 
+               string "arg("
+               arg <- argName
+               string ")."
+               whiteSpace
+               return arg
+
+-- |A complete attack consists of @atk(argName,argName).@
+-- or @att(argName,argName).@.
+pAttack :: Parser (String, String)
+pAttack = do 
+             string "at"
+             string "t(" <|> string "k("
+             arg1 <- argName
+             char ','
+             whiteSpace
+             arg2 <- argName
+             string ")."
+             return (arg1, arg2)
+
+-- |Parses one attack or argument and returns the result
+-- in the 'Either' data type.
+pArgOrAttack :: Parser (Either String (String, String))
+pArgOrAttack = try (do arg <- pArgument 
+                       whiteSpace
+                       return $ Left arg)
+               <|> 
+               do atk <- pAttack
+                  whiteSpace
+                  return $ Right atk
+
+-- |An AF is parsed by parsing at least one argument or attack,
+-- followed by an end of file token.
+pAF :: Parser (DungAF String)
+pAF = do  
+          ps <- many1 pArgOrAttack
+          eof
+          let (args, atks) = partitionEithers ps
+          return $ AF args atks
+
+-- |Parses a 'String' containing multiple arguments/attacks. 
+-- If parsing fails, it propagates the parse error.
+parseAF :: String -> Either ParseError (DungAF String)
+parseAF = parse pAF ""
diff --git a/src/Language/Dung/Output.hs b/src/Language/Dung/Output.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Dung/Output.hs
@@ -0,0 +1,60 @@
+-- | This is the output module accompanying the implementation of Dung's 
+-- argumentation frameworks. It allows an implemented argumentation framework
+-- to be outputted to files in a standard format.
+--
+-- This module currently contains two output format. The strict version is readable 
+-- by both CEGARTIX and PrefSat. The lax version keeps more of the original formatting.
+module Language.Dung.Output 
+  (
+   -- * CEGARTIX/PrefSat output
+   argToCegartix, atkToCegartix, toCegartix,
+   argToStrictCegartix, atkToStrictCegartix, toStrictCegartix
+   )
+ where
+import Language.Dung.AF
+
+
+-- |Converts an argument to a CEGARTIX 'String'. All argument names are made
+-- into string literals removing extra quotes. Additionally all parentheses are removed.
+argToStrictCegartix :: Show arg => arg -> String
+argToStrictCegartix arg = "arg(" ++ (show . remParens . remQuote . show) arg ++ ").\n" 
+
+-- |Converts an attack to a CEGARTIX 'String'. All argument names are made
+-- into string literals removing extra quotes. Additionally all parentheses are removed.
+atkToStrictCegartix :: Show arg => (arg, arg) -> String
+atkToStrictCegartix (a,b) = "att(" ++ (show . remParens . remQuote . show) a ++ "," ++ (show . remQuote. show) b ++ ").\n"
+
+-- |Converts an argument to a CEGARTIX 'String'. All argument names are made
+-- into string literals removing extra quotes.
+argToCegartix :: Show arg => arg -> String
+argToCegartix arg = "arg(" ++ (show . remQuote . show) arg ++ ").\n" 
+
+-- |Converts an attack to a CEGARTIX 'String'. All argument names are made
+-- into string literals removing extra quotes.
+atkToCegartix :: Show arg => (arg, arg) -> String
+atkToCegartix (a,b) = "att(" ++ (show . remQuote . show) a ++ "," ++ (show . remQuote. show) b ++ ").\n"
+
+-- |Outputs an argumentation frameworks in CEGARTIX/PrefSat format.
+toCegartix :: Show arg => DungAF arg -> String
+toCegartix (AF args att) = 
+    concatMap argToCegartix args
+ ++ concatMap atkToCegartix att
+
+-- |Outputs an argumentation frameworks in strict CEGARTIX/PrefSat format.
+toStrictCegartix :: Show arg => DungAF arg -> String
+toStrictCegartix (AF args att) = 
+    concatMap argToStrictCegartix args
+ ++ concatMap atkToStrictCegartix att
+
+-- toCegartix :: Show arg => DungAF arg -> IO ()
+-- toCegartix (AF args att) = do 
+  -- mapM_ (putStr . argToCegartix) args
+  -- mapM_ (putStr . atkToCegartix) att
+
+-- |Remove all quotes from a 'String'.
+remQuote :: String -> String
+remQuote = filter (/= '"')
+
+-- |Remove all parentheses from a 'String'.
+remParens :: String -> String
+remParens = filter (\ x -> x /= '(' && x /= ')')
diff --git a/src/Main.hs b/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Main.hs
@@ -0,0 +1,97 @@
+-- |This module implements a command-line interface to the implementation of 
+-- Dung's argumentation frameworks. Dung + Haskell = Dungell
+--
+-- Code in this module partly taken from/inspired by Shinobu
+-- See: http://zuttobenkyou.wordpress.com/2011/04/19/haskell-using-cmdargs-single-and-multi-mode/
+-- and http://listx.github.com/
+{-# LANGUAGE DeriveDataTypeable, RecordWildCards #-}
+module Main
+  (
+    main
+  )
+ where
+import Language.Dung.AF(groundedExt, preferredExt, stableExt, semiStableExt,
+                        DungAF(..))
+import Language.Dung.Input
+import Language.Dung.Output
+
+import System.Console.CmdArgs
+import System.Environment (getArgs, withArgs)
+import System.Exit
+import Control.Monad (when, unless)
+
+data MyOptions = MyOptions {
+  cegartix    :: Bool,
+  laxCegartix :: Bool,
+  fileName    :: String,
+  outputFile  :: String,
+  grounded    :: Bool,
+  preferred   :: Bool,
+  stable      :: Bool,
+  semiStable  :: Bool,
+  all         :: Bool
+ } deriving (Show, Data, Typeable)
+
+myProgOpts :: MyOptions
+myProgOpts = MyOptions
+    { cegartix    = True  &= help "Output in strict CEGARTIX/PrefSat format (standard)" 
+    , laxCegartix = False &= help "Output in lax CEGARTIX/PrefSat format (+parentheses)" 
+    , fileName    = def   &= typFile &= help "Name of the file to be read"
+    , outputFile  = def   &= typFile &= help "Name of the file to be written"
+    , grounded    = False &= help "Output grounded extension for the AF"
+    , preferred   = False &= help "Output preferred extensions for the AF"
+    , stable      = False &= help "Output stable extensions for the AF"
+    , semiStable  = False &= help "Output semi-stable extensions for the AF"
+    , all         = False &= help "Output extensions of all implemented semantics for AF"
+    }
+ 
+getOpts :: IO MyOptions
+getOpts = cmdArgs $ myProgOpts
+    -- &= verbosityArgs [explicit, name "Verbose", name "V"] []
+    &= versionArg [explicit, name "version", name "v", summary _PROGRAM_INFO]
+    &= summary (_PROGRAM_INFO ++ ", " ++ _COPYRIGHT)
+    &= help _PROGRAM_ABOUT
+    &= helpArg [explicit, name "help", name "h"]
+    &= program _PROGRAM_NAME
+ 
+_PROGRAM_NAME = "Dungell"
+_PROGRAM_VERSION = "1.0"
+_PROGRAM_INFO = _PROGRAM_NAME ++ " version " ++ _PROGRAM_VERSION
+_PROGRAM_ABOUT = "An implementation of Dung's AFs"
+_COPYRIGHT = "(C) Bas van Gijzel 2014"
+
+
+main :: IO ()
+main = do 
+        args <- getArgs
+        opts <- (if null args then withArgs ["--help"] else id) getOpts
+        optionHandler opts
+
+-- |Check any malformed arguments/missing arguments. 
+optionHandler :: MyOptions -> IO ()
+optionHandler opts@MyOptions{..}  = do 
+    when (null fileName) $ putStrLn "--fileName is blank!" >> exitWith (ExitFailure 1)
+    input <- readFile fileName
+    let opts = opts {cegartix = not laxCegartix}
+    af <- case parseAF input of 
+           Left err -> putStrLn "Parsing error: " >> print err >> exitWith (ExitFailure 1)
+           Right af -> return af
+    let opts' = if all 
+         then 
+           opts {grounded = True, preferred = True, stable = True, semiStable = True} 
+         else 
+           opts
+    exec opts' af
+
+-- |Execute supplied options
+exec :: (Show arg, Eq arg, Ord arg) => MyOptions -> DungAF arg -> IO ()
+exec opts@MyOptions{..} af = do
+    print af
+    when grounded   $ putStr "grounded: "    >> print (groundedExt af)
+    when preferred  $ putStr "preferred: "   >> print (preferredExt af)
+    when stable     $ putStr "stable: "      >> print (stableExt af)
+    when semiStable $ putStr "semi-stable: " >> print (semiStableExt af)
+    unless (null outputFile)
+      $ if cegartix 
+          then writeFile outputFile (toStrictCegartix af) >> putStrLn "File outputted."
+          else writeFile outputFile (toCegartix af) >> putStrLn "File outputted."
