diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..9e05c58
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,40 @@
+name: CI
+
+on:
+  push:
+    branches: [master]
+  pull_request:
+    branches: [master]
+
+jobs:
+  build:
+    name: GHC ${{ matrix.ghc }}
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        ghc: ['9.4', '9.6', '9.8', '9.10']
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: haskell-actions/setup@v2
+        with:
+          ghc-version: ${{ matrix.ghc }}
+
+      - name: Cache cabal store
+        uses: actions/cache@v4
+        with:
+          path: ~/.cabal/store
+          key: ${{ runner.os }}-ghc-${{ matrix.ghc }}-cabal-${{ hashFiles('Dung.cabal') }}
+          restore-keys: |
+            ${{ runner.os }}-ghc-${{ matrix.ghc }}-cabal-
+
+      - name: Update cabal package list
+        run: cabal update
+
+      - name: Build
+        run: cabal build all
+
+      - name: Run tests
+        run: cabal test all --test-show-details=direct
diff --git a/CHANGELOG b/CHANGELOG
deleted file mode 100644
index 732f591..0000000
--- a/CHANGELOG
+++ /dev/null
@@ -1,45 +0,0 @@
-1.0.0.1 => 1.1
-==============
-This package version is now compatible with the command-line application for 
-the ICCMA competition. See: https://github.com/nebasuke/DungICCMA and the
-competition website: http://argumentationcompetition.org/2015/index.html
-
-This package has again been significantly extended and now includes:
-
-* Strict version of the grounded fixpoint semantics.
-
-* Definitions of what it means to be a preferred and stable extension.
-
-* Naive implementations of complete, preferred and stable semantics using 
-  the characteristic function. The fixpoint definitions are actually FASTER
-  than the fancy algorithm implementation. 
-  
-* Included the fast implementations of intersect, nub and (\\) by Niklas 
-  Hambuechen. 
-  
-* Added some clarifying text for the "complete" labelling.
-
-
-1.0 => 1.0.0.1
-==============
-* Fixed the record declaration in Main.hs.
-
-* Added an example file.
-
-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.
\ No newline at end of file
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..015f2d6
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,64 @@
+# Changelog
+
+## 1.1 → 2.0.0.0
+
+### Breaking changes
+
+- **Fixed `groundedF` infinite-loop bug**: `groundedF` now correctly applies
+  the characteristic function at each step instead of recursing with unchanged
+  arguments. Code relying on `groundedF'` as a workaround can switch back to
+  `groundedF`.
+
+- **CLI rewritten**: The `dungell` executable now uses `optparse-applicative`
+  instead of `cmdargs`. Command-line flags have changed:
+  - Semantics are selected via `--grounded`, `--preferred`, `--stable`,
+    `--semi-stable`, or `--all`
+
+### Improvements
+
+- Upgraded to `cabal-version: 3.0` format
+- Relaxed `containers` upper bound to build on GHC 9.4+
+- Added `Language.Dung` convenience re-export module
+- Added test suite (tasty + QuickCheck + doctest)
+- Added GitHub Actions CI for GHC 9.4, 9.6, 9.8, 9.10
+- Fixed all `-Wall` warnings
+- Removed dependency on unmaintained `cmdargs` library
+- Converted documentation to Markdown
+
+## 1.0.0.1 → 1.1
+
+This package version is now compatible with the command-line application for
+the ICCMA competition. See: <https://github.com/nebasuke/DungICCMA> and the
+competition website: <http://argumentationcompetition.org/2015/index.html>
+
+This package has again been significantly extended and now includes:
+
+- Strict version of the grounded fixpoint semantics.
+- Definitions of what it means to be a preferred and stable extension.
+- Naive implementations of complete, preferred and stable semantics using
+  the characteristic function. The fixpoint definitions are actually FASTER
+  than the fancy algorithm implementation.
+- Included the fast implementations of `intersect`, `nub` and `(\\)` by
+  Niklas Hambuechen.
+- Added some clarifying text for the "complete" labelling.
+
+## 1.0 → 1.0.0.1
+
+- Fixed the record declaration in Main.hs.
+- Added an example file.
+
+## 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
index 404274c..a81e183 100644
--- a/Dung.cabal
+++ b/Dung.cabal
@@ -1,48 +1,102 @@
+cabal-version: 3.0
 name:          Dung
-category:      Argumentation, Embedded, AI
-version:       1.1
-license:       BSD3
-cabal-version: >= 1.6
+version:       2.0.0.0
+license:       BSD-3-Clause
 license-file:  LICENSE
 author:        Bas van Gijzel
-maintainer:    Bas van Gijzel <bmv@cs.nott.ac.uk>
+maintainer:    Bas van Gijzel <nenekotan+git@gmail.com>
+copyright:     Copyright (C) 2014-2026 Bas van Gijzel
 stability:     experimental
-homepage:      http://www.cs.nott.ac.uk/~bmv/Dung/
-copyright:     Copyright (C) 2014 Bas van Gijzel
+category:      Argumentation, Embedded, AI
+homepage:      https://github.com/nebasuke/Dung
 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 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/>.
+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 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 <https://scholar.google.com/citations?user=Xu4yjvwAAAAJ&hl>.
 
 build-type:    Simple
+tested-with:   GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1
 
-Extra-Source-Files:
-                           CHANGELOG
-                           exampleaf.txt
+extra-doc-files:
+  README.md
+  CHANGELOG.md
 
-Library
-  build-depends:
-    base                   >= 4        && < 5,
-    containers             >= 0.3      && < 0.6,
-    cmdargs                >= 0.10.2,
-    parsec                 >= 3
+extra-source-files:
+  LICENSE
+  exampleaf.txt
+  dungex.txt
 
-  hs-source-dirs:
-    src
+source-repository head
+  type:     git
+  location: https://github.com/nebasuke/Dung
 
+common warnings
+  ghc-options:
+    -Wall
+    -Wcompat
+    -Widentities
+    -Wincomplete-record-updates
+    -Wincomplete-uni-patterns
+    -Wredundant-constraints
+  default-language: Haskell2010
+
+library
+  import:           warnings
+  hs-source-dirs:   src
+  build-depends:
+    base       >= 4.16 && < 5,
+    containers >= 0.6  && < 0.8,
+    parsec     >= 3.1  && < 3.2
   exposed-modules:
+    Language.Dung
     Language.Dung.AF
     Language.Dung.Examples
-    Language.Dung.Output
     Language.Dung.Input
+    Language.Dung.Output
 
-Executable dungell
-  main-Is:                 Main.hs
-  hs-source-dirs:          src
+executable dungell
+  import:           warnings
+  main-is:          Main.hs
+  hs-source-dirs:   app
+  build-depends:
+    base                 >= 4.16 && < 5,
+    Dung,
+    optparse-applicative >= 0.17 && < 0.19
+  ghc-options:      -threaded
 
-source-repository head
-  Type:     git
-  Location: https://github.com/nebasuke/Dung
\ No newline at end of file
+test-suite dung-tests
+  import:           warnings
+  type:             exitcode-stdio-1.0
+  main-is:          Main.hs
+  hs-source-dirs:   test
+  build-depends:
+    base              >= 4.16 && < 5,
+    Dung,
+    containers        >= 0.6  && < 0.8,
+    tasty             >= 1.4  && < 1.6,
+    tasty-hunit       >= 0.10 && < 0.11,
+    tasty-quickcheck  >= 0.10 && < 0.11,
+    QuickCheck        >= 2.14 && < 2.16
+  other-modules:
+    Test.Language.Dung.AF
+    Test.Language.Dung.Input
+    Test.Language.Dung.Properties
+
+test-suite dung-doctest
+  import:           warnings
+  type:             exitcode-stdio-1.0
+  main-is:          Doctest.hs
+  hs-source-dirs:   test
+  build-depends:
+    base    >= 4.16 && < 5,
+    doctest >= 0.20 && < 0.23
diff --git a/LICENSE b/LICENSE
index c3f8f7b..98014c1 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c)2014, 2015, Bas van Gijzel
+Copyright (c) 2014-2026, Bas van Gijzel
 
 All rights reserved.
 
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..dfc2b8a
--- /dev/null
+++ b/README.md
@@ -0,0 +1,53 @@
+# Dung
+
+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 the
+[Wikipedia article on argumentation frameworks](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 papers accompanying this library see:
+
+- "Towards a framework for the implementation and verification of translations
+  between argumentation models"
+- "A principled approach to the implementation of argumentation models"
+
+Available at <https://scholar.google.com/citations?user=Xu4yjvwAAAAJ&hl>.
+
+## Usage
+
+```haskell
+import Language.Dung
+
+-- Define an argumentation framework: A -> B -> C
+let af = AF ["A", "B", "C"] [("A", "B"), ("B", "C")]
+
+-- Compute the grounded extension
+groundedExt af
+-- ["A", "C"]
+
+-- Compute preferred extensions
+preferredExt af
+-- [["A","C"]]
+```
+
+## Executable
+
+The `dungell` executable reads argumentation frameworks from files in
+CEGARTIX/PrefSat format:
+
+```
+dungell --filename exampleaf.txt --grounded
+dungell --filename exampleaf.txt --preferred
+dungell --filename exampleaf.txt --all
+```
+
+## License
+
+BSD-3-Clause. See [LICENSE](LICENSE) for details.
diff --git a/README.txt b/README.txt
deleted file mode 100644
index 783188f..0000000
--- a/README.txt
+++ /dev/null
@@ -1,8 +0,0 @@
-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/.
\ No newline at end of file
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
index bf68901..0000000
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
\ No newline at end of file
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
index 0000000..0dfe178
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,98 @@
+-- |This module implements a command-line interface to the implementation of
+-- Dung's argumentation frameworks. Dung + Haskell = Dungell
+{-# LANGUAGE RecordWildCards #-}
+module Main
+  ( main
+  ) where
+
+import Language.Dung.AF (groundedExt, preferredExt, stableExt, semiStableExt,
+                          DungAF(..))
+import Language.Dung.Input
+import Language.Dung.Output
+
+import Options.Applicative
+import System.Exit
+import Control.Monad (when)
+
+data Semantics
+  = Grounded
+  | Preferred
+  | Stable
+  | SemiStable
+  deriving (Eq, Show)
+
+data Options = Options
+  { optLaxCegartix :: Bool
+  , optFileName    :: FilePath
+  , optOutputFile  :: Maybe FilePath
+  , optSemantics   :: [Semantics]
+  } deriving (Show)
+
+semanticsFlags :: Parser [Semantics]
+semanticsFlags = combineFlags
+  <$> switch (long "grounded"    <> help "Output grounded extension for the AF")
+  <*> switch (long "preferred"   <> help "Output preferred extensions for the AF")
+  <*> switch (long "stable"      <> help "Output stable extensions for the AF")
+  <*> switch (long "semi-stable" <> help "Output semi-stable extensions for the AF")
+  <*> switch (long "all"         <> help "Output extensions of all implemented semantics for AF")
+  where
+    combineFlags gr pr st ss allSem
+      | allSem    = [Grounded, Preferred, Stable, SemiStable]
+      | otherwise = concat
+          [ [Grounded   | gr]
+          , [Preferred  | pr]
+          , [Stable     | st]
+          , [SemiStable | ss]
+          ]
+
+optionsParser :: Parser Options
+optionsParser = Options
+  <$> switch
+        (  long "lax-cegartix"
+        <> help "Output in lax CEGARTIX/PrefSat format (+parentheses)"
+        )
+  <*> strOption
+        (  long "filename"
+        <> metavar "FILE"
+        <> help "Name of the file to be read"
+        )
+  <*> optional (strOption
+        (  long "outputfile"
+        <> metavar "FILE"
+        <> help "Name of the file to be written"
+        ))
+  <*> semanticsFlags
+
+opts :: ParserInfo Options
+opts = info (optionsParser <**> helper)
+  (  fullDesc
+  <> progDesc "An implementation of Dung's AFs"
+  <> header "dungell - Dung + Haskell argumentation framework tool"
+  )
+
+main :: IO ()
+main = do
+  Options{..} <- execParser opts
+  input <- readFile optFileName
+  af <- case parseAF input of
+    Left err -> do
+      putStrLn "Parsing error: "
+      print err
+      exitWith (ExitFailure 1)
+    Right af -> return af
+  exec optLaxCegartix optOutputFile optSemantics af
+
+exec :: (Show arg, Ord arg)
+     => Bool -> Maybe FilePath -> [Semantics] -> DungAF arg -> IO ()
+exec laxCegartix outputFile semantics af = do
+  print af
+  when (Grounded   `elem` semantics) $ putStr "grounded: "    >> print (groundedExt af)
+  when (Preferred  `elem` semantics) $ putStr "preferred: "   >> print (preferredExt af)
+  when (Stable     `elem` semantics) $ putStr "stable: "      >> print (stableExt af)
+  when (SemiStable `elem` semantics) $ putStr "semi-stable: " >> print (semiStableExt af)
+  case outputFile of
+    Nothing -> return ()
+    Just fp ->
+      if not laxCegartix
+        then writeFile fp (toStrictCegartix af) >> putStrLn "File outputted."
+        else writeFile fp (toCegartix af) >> putStrLn "File outputted."
diff --git a/src/Language/Dung.hs b/src/Language/Dung.hs
new file mode 100644
index 0000000..4b695a7
--- /dev/null
+++ b/src/Language/Dung.hs
@@ -0,0 +1,12 @@
+-- | Convenience re-export module for Dung's argumentation frameworks.
+--
+-- This module re-exports "Language.Dung.AF" so users can simply write:
+--
+-- @
+-- import Language.Dung
+-- @
+module Language.Dung
+  ( module Language.Dung.AF
+  ) where
+
+import Language.Dung.AF
diff --git a/src/Language/Dung/AF.hs b/src/Language/Dung/AF.hs
index 5b14bf7..f82901f 100644
--- a/src/Language/Dung/AF.hs
+++ b/src/Language/Dung/AF.hs
@@ -1,5 +1,5 @@
--- | This module implements Dung's argumentation frameworks. 
-module Language.Dung.AF 
+-- | This module implements Dung's argumentation frameworks.
+module Language.Dung.AF
  (
     -- * Basic definitions  
    DungAF(..), 
@@ -14,14 +14,14 @@ module Language.Dung.AF
    -- 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(..), 
+   Status(..), Labelling,
    inLab, outLab, undecLab, 
    allIn, allOut, allUndec,
    powerLabel,
    unattacked, attacked, 
    labAttackers, illegallyIn, illegallyOut, illegallyUndec,
    legallyIn, legallyOut, legallyUndec,
-   isAdmissible, isComplete, isPreferred, isStable, isSemiStable,
+   isAdmissible, isComplete, isGrounded, isPreferred, isStable, isSemiStable,
    transitionStep, terminatedTransition, superIllegallyIn,
    -- * Grounded, preferred, semi-stable and stable labellings
    -- |The following functions are implementations of the 
@@ -82,12 +82,12 @@ setAttacks (AF _ def) args arg
 -- |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']
+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']
+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).
@@ -143,7 +143,7 @@ groundedF :: Eq arg => ([arg] -> [arg]) -> [arg]
 groundedF f = step f []
   where  step f args 
            | f args == args  = args
-           | otherwise       = step f args
+           | otherwise       = step f (f args)
 
 -- |Given a characteristic function f, computes the grounded extension
 -- by iterating on the empty set (list) until it reaches a fixpoint.
@@ -173,7 +173,7 @@ completeF af@(AF args _) =
 -- by applying a filter on the complete extensions. Note that this, 
 -- naive definition is faster than the current algorithm implementation.
 preferredF :: Ord arg => DungAF arg -> [[arg]]
-preferredF af@(AF args _) = 
+preferredF af =
   let cs = completeF af
   in filter (isPreferredExt af cs) cs
 
@@ -181,14 +181,14 @@ preferredF af@(AF args _) =
 -- by applying a filter on the complete extensions. Note that this, 
 -- naive definition is faster than the current algorithm implementation.
 stableF :: Ord arg => DungAF arg -> [[arg]]
-stableF af@(AF args _) = 
+stableF af =
   let ps = preferredF af
   in  filter (isStableExt af) ps
 
 -- |A complete extension is also a preferred extension if it is not a 
 -- subset of one of the other extensions. 
 isPreferredExt :: Ord arg => DungAF arg -> [[arg]] -> [arg] -> Bool
-isPreferredExt af exts ext = all (not . (ext `subset`)) 
+isPreferredExt _af exts ext = all (not . (ext `subset`))
                                  (delete ext exts)
 
 -- |S is a stable extension is an extension iff it is equal to the set 
@@ -301,14 +301,14 @@ 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]
+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 af labs (a, In) = not . null $ [()|  (_, l) <- labAttackers af a labs, l /= Out]
 illegallyIn _  _     _      = False
 
 -- Definition 5.2 of Caminada
@@ -316,7 +316,7 @@ illegallyIn _  _     _      = False
 -- 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 af labs (a, Out) = null [() | (_, In) <- labAttackers af a labs]
 illegallyOut _  _    _        = False
 
 -- Definition 5.3 of Caminada
@@ -326,7 +326,7 @@ illegallyOut _  _    _        = False
 -- 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] 
+                                        || (not . null) [() | (_, In) <- labAttackers af a labs]
 illegallyUndec _  _    _              = False
 
 
@@ -362,19 +362,19 @@ legallyUndec _  _    _                  = False
 -- |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] 
+isAdmissible af labs = null $
+                      [lab | lab@(_, In) <- labs, illegallyIn af labs lab]
+                   ++ [lab | lab@(_, 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]
+isComplete af labs = null $
+                   [lab | lab@(_, In) <- labs, illegallyIn af labs lab]
+                ++ [lab | lab@(_, Out) <- labs, illegallyOut af labs lab]
+                ++ [lab | lab@(_, Undecided) <- labs, illegallyUndec af labs lab]
 
 
 -- Definition 8 of Caminada, grounded labelling
@@ -398,8 +398,8 @@ isPreferred af labss labs = isComplete af labs &&
 -- |Let 'labs' be a complete labelling, i.e. 'isComplete af labs', we say that 
 -- labs is a stable labelling iff @undecLab(labs) == []@
 isStable :: Eq arg => DungAF arg -> [Labelling arg] -> Labelling arg -> Bool
-isStable af labss labs = isComplete af labs && 
-                         null (undecLab labs)
+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 
@@ -421,12 +421,12 @@ 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) -> 
+     (newUndecs, rest) = partition (\ lab@(b, _l) ->
                                        b `elem` bs
                                     && illegallyOut af labs' lab)
                                   labs'
- in map (\ (a, _) -> (a, Undecided)) newUndecs
- ++ rem
+ in map (\ (x, _) -> (x, Undecided)) newUndecs
+ ++ rest
 
 
 -- Based on Definition 10 of Caminada
@@ -460,7 +460,7 @@ superIllegallyIn _  _    _      = False
 -- 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) = 
+complete af@(AF args _atk) =
  let allInArgs = allIn args
      complete' :: Eq arg => DungAF arg -> Labelling arg -> [Labelling arg]
      complete' af labs =
@@ -476,21 +476,21 @@ complete af@(AF args atk) =
 -- |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) = 
+preferred af =
  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) = 
+stable af =
  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) = 
+semiStable af =
  let completes = complete af 
  in filter (isSemiStable af completes) completes
 
diff --git a/src/Language/Dung/Examples.hs b/src/Language/Dung/Examples.hs
index 56ad1c8..48e3bf3 100644
--- a/src/Language/Dung/Examples.hs
+++ b/src/Language/Dung/Examples.hs
@@ -27,6 +27,15 @@ module Language.Dung.Examples
 import Language.Dung.AF
 import Language.Dung.Input
 import Language.Dung.Output
+
+-- $setup
+-- >>> :{
+-- >>> let printList :: Show a => [a] -> IO ()
+-- >>>     printList [] = putStrLn "[]"
+-- >>>     printList [x] = do { putStrLn "[" ; putStrLn ("  " ++ show x) ; putStrLn "]" }
+-- >>>     printList xs = do { putStrLn "[" ; mapM_ (\x -> putStrLn ("  " ++ show x ++ ",")) (init xs) ; putStrLn ("  " ++ show (last xs)) ; putStrLn "]" }
+-- >>> :}
+
 -- | The simplest abstract argument is an argument identifiable by its name
 type AbsArg = String 
 
@@ -113,7 +122,7 @@ exampleAF = AF [a, b, c] [(a, b), (b, c)]
 -- and 'exampleAF2':
 --
 -- >>> groundedExt exampleAF
--- ["A", "C"]
+-- ["A","C"]
 -- >>> groundedExt exampleAF2
 -- []
 exampleAF2 :: DungAF AbsArg 
@@ -154,12 +163,12 @@ exampleAF3 = AF [a, b, c, d] [(a, a), (a, c), (b, c), (c, d)]
 -- The complete labellings of the argumentation framework 'exampleAF3'
 -- and 'exampleAF4':
 -- 
--- >>> complete exampleAF3
+-- >>> printList (complete exampleAF3)
 -- [
 --   [("A",Undecided),("B",In),("C",Out),("D",In)]
 -- ]
--- 
--- >>> complete exampleAF4
+--
+-- >>> printList (complete exampleAF4)
 -- [
 --   [("A",Out),("B",In),("C",Out),("D",In),("E",Out)],
 --   [("A",In),("B",Out),("C",Undecided),("D",Undecided),("E",Undecided)],
@@ -171,11 +180,11 @@ exampleAF3 = AF [a, b, c, d] [(a, a), (a, c), (b, c), (c, d)]
 -- The complete extensions of the argumentation frameworks 'exampleAF3'
 -- and 'exampleAF4':
 --
--- >>> completeExt exampleAF3
+-- >>> printList (completeExt exampleAF3)
 -- [
 --   ["B","D"]
 -- ]
--- >>> completeExt exampleAF4
+-- >>> printList (completeExt exampleAF4)
 -- [
 --   ["B","D"],
 --   ["A"],
@@ -187,14 +196,14 @@ exampleAF3 = AF [a, b, c, d] [(a, a), (a, c), (b, c), (c, d)]
 -- The semi-stable labellings of the argumentation framework 'exampleAF3'
 -- and 'exampleAF4':
 -- 
--- >>> semiStable exampleAF3
+-- >>> printList (semiStable exampleAF3)
 -- [
 --   [("A",Undecided),("B",In),("C",Out),("D",In)]
 -- ]
--- 
--- >>> semiStable exampleAF4
+--
+-- >>> printList (semiStable exampleAF4)
 -- [
---   [("A",Out),("B",In),("C",Out),("D",In),("E",Out)],
+--   [("A",Out),("B",In),("C",Out),("D",In),("E",Out)]
 -- ]
 --
 -- [semiStableExt:]
@@ -202,13 +211,13 @@ exampleAF3 = AF [a, b, c, d] [(a, a), (a, c), (b, c), (c, d)]
 -- The complete extensions of the argumentation frameworks 'exampleAF3'
 -- and 'exampleAF4':
 --
--- >>> semiStableExt exampleAF3
+-- >>> printList (semiStableExt exampleAF3)
 -- [
 --   ["B","D"]
 -- ]
--- >>> semiStableExt exampleAF4
+-- >>> printList (semiStableExt exampleAF4)
 -- [
---   ["B","D"],
+--   ["B","D"]
 -- ]
 --
 exampleAF4 :: DungAF AbsArg
diff --git a/src/Language/Dung/Input.hs b/src/Language/Dung/Input.hs
index 65a4d6e..d408a8b 100644
--- a/src/Language/Dung/Input.hs
+++ b/src/Language/Dung/Input.hs
@@ -19,10 +19,8 @@ module Language.Dung.Input
 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 Text.Parsec.Language (haskellStyle)
 import Data.Either (partitionEithers)
 
 lexer :: P.TokenParser ()
@@ -44,24 +42,24 @@ argName =  try identifier <|> stringLiteral
 
 -- |A complete argument consists of @arg(argName).@
 pArgument :: Parser String
-pArgument = do 
-               string "arg("
+pArgument = do
+               _ <- string "arg("
                arg <- argName
-               string ")."
+               _ <- 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("
+pAttack = do
+             _ <- string "at"
+             _ <- string "t(" <|> string "k("
              arg1 <- argName
-             char ','
+             _ <- char ','
              whiteSpace
              arg2 <- argName
-             string ")."
+             _ <- string ")."
              return (arg1, arg2)
 
 -- |Parses one attack or argument and returns the result
diff --git a/src/Main.hs b/src/Main.hs
deleted file mode 100644
index 1f3662d..0000000
--- a/src/Main.hs
+++ /dev/null
@@ -1,97 +0,0 @@
--- |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.0.1"
-_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."
\ No newline at end of file
diff --git a/test/Doctest.hs b/test/Doctest.hs
new file mode 100644
index 0000000..676bf8c
--- /dev/null
+++ b/test/Doctest.hs
@@ -0,0 +1,11 @@
+module Main (main) where
+
+import Test.DocTest
+
+main :: IO ()
+main = doctest
+  [ "-isrc"
+  , "-package", "containers"
+  , "-package", "parsec"
+  , "src/Language/Dung/Examples.hs"
+  ]
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
index 0000000..f656bf8
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,14 @@
+module Main (main) where
+
+import Test.Tasty
+
+import qualified Test.Language.Dung.AF as AF
+import qualified Test.Language.Dung.Input as Input
+import qualified Test.Language.Dung.Properties as Properties
+
+main :: IO ()
+main = defaultMain $ testGroup "Dung"
+  [ AF.tests
+  , Input.tests
+  , Properties.tests
+  ]
diff --git a/test/Test/Language/Dung/AF.hs b/test/Test/Language/Dung/AF.hs
new file mode 100644
index 0000000..40168da
--- /dev/null
+++ b/test/Test/Language/Dung/AF.hs
@@ -0,0 +1,184 @@
+module Test.Language.Dung.AF (tests) where
+
+import Data.List (sort)
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Language.Dung.AF
+
+-- Convenience definitions matching Examples.hs
+a, b, c, d, e :: String
+a = "A"
+b = "B"
+c = "C"
+d = "D"
+e = "E"
+
+-- A -> B -> C
+exampleAF :: DungAF String
+exampleAF = AF [a, b, c] [(a, b), (b, c)]
+
+-- A <-> B
+exampleAF2 :: DungAF String
+exampleAF2 = AF [a, b] [(a, b), (b, a)]
+
+-- Fig1 LHS in Caminada: {(a,a), (a,c), (b,c), (c,d)}
+exampleAF3 :: DungAF String
+exampleAF3 = AF [a, b, c, d] [(a, a), (a, c), (b, c), (c, d)]
+
+-- Fig1 RHS in Caminada: {(a,b), (b,a), (b,c), (c,d), (d,e), (e,c)}
+exampleAF4 :: DungAF String
+exampleAF4 = AF [a, b, c, d, e] [(a, b), (b, a), (b, c), (c, d), (d, e), (e, c)]
+
+tests :: TestTree
+tests = testGroup "Language.Dung.AF"
+  [ setAttacksTests
+  , conflictFreeTests
+  , acceptableTests
+  , admissibleTests
+  , groundedTests
+  , groundedExtTests
+  , groundedFTests
+  , completeTests
+  , completeExtTests
+  , preferredExtTests
+  , stableExtTests
+  , semiStableTests
+  , semiStableExtTests
+  ]
+
+setAttacksTests :: TestTree
+setAttacksTests = testGroup "setAttacks"
+  [ testCase "[a,b] attacks c in exampleAF" $
+      setAttacks exampleAF [a, b] c @?= True
+  , testCase "[b,c] does not attack a in exampleAF" $
+      setAttacks exampleAF [b, c] a @?= False
+  , testCase "[] does not attack b in exampleAF2" $
+      setAttacks exampleAF2 [] b @?= False
+  ]
+
+conflictFreeTests :: TestTree
+conflictFreeTests = testGroup "conflictFree"
+  [ testCase "[a,c] is conflict-free in exampleAF" $
+      conflictFree exampleAF [a, c] @?= True
+  , testCase "[a,b,c] is not conflict-free in exampleAF" $
+      conflictFree exampleAF [a, b, c] @?= False
+  , testCase "[a,b] is not conflict-free in exampleAF2" $
+      conflictFree exampleAF2 [a, b] @?= False
+  ]
+
+acceptableTests :: TestTree
+acceptableTests = testGroup "acceptable"
+  [ testCase "c acceptable w.r.t. [a,b] in exampleAF" $
+      acceptable exampleAF c [a, b] @?= True
+  , testCase "c not acceptable w.r.t. [] in exampleAF" $
+      acceptable exampleAF c [] @?= False
+  , testCase "b not acceptable w.r.t. [a,b,c] in exampleAF" $
+      acceptable exampleAF b [a, b, c] @?= False
+  ]
+
+admissibleTests :: TestTree
+admissibleTests = testGroup "admissible"
+  [ testCase "[a,b,c] not admissible in exampleAF" $
+      admissible exampleAF [a, b, c] @?= False
+  , testCase "[a,c] is admissible in exampleAF" $
+      admissible exampleAF [a, c] @?= True
+  , testCase "[a] is admissible in exampleAF" $
+      admissible exampleAF [a] @?= True
+  ]
+
+groundedTests :: TestTree
+groundedTests = testGroup "grounded"
+  [ testCase "grounded exampleAF" $
+      sort (grounded exampleAF) @?= sort [("A", In), ("C", In), ("B", Out)]
+  , testCase "grounded exampleAF2" $
+      sort (grounded exampleAF2) @?= sort [("A", Undecided), ("B", Undecided)]
+  ]
+
+groundedExtTests :: TestTree
+groundedExtTests = testGroup "groundedExt"
+  [ testCase "groundedExt exampleAF" $
+      sort (groundedExt exampleAF) @?= sort ["A", "C"]
+  , testCase "groundedExt exampleAF2" $
+      groundedExt exampleAF2 @?= []
+  ]
+
+groundedFTests :: TestTree
+groundedFTests = testGroup "groundedF"
+  [ testCase "groundedF (f exampleAF)" $
+      sort (groundedF (f exampleAF)) @?= sort ["A", "C"]
+  , testCase "groundedF (f exampleAF2)" $
+      groundedF (f exampleAF2) @?= []
+  , testCase "groundedF' (f exampleAF)" $
+      sort (groundedF' (f exampleAF)) @?= sort ["A", "C"]
+  , testCase "groundedF' (f exampleAF2)" $
+      groundedF' (f exampleAF2) @?= []
+  ]
+
+completeTests :: TestTree
+completeTests = testGroup "complete"
+  [ testCase "complete exampleAF3 has one labelling" $
+      length (complete exampleAF3) @?= 1
+  , testCase "complete exampleAF3 content" $ case complete exampleAF3 of
+      (lab:_) -> sort lab @?= sort [("A", Undecided), ("B", In), ("C", Out), ("D", In)]
+      []    -> assertFailure "Expected at least one complete labelling"
+  , testCase "complete exampleAF4 has three labellings" $
+      length (complete exampleAF4) @?= 3
+  ]
+
+completeExtTests :: TestTree
+completeExtTests = testGroup "completeExt"
+  [ testCase "completeExt exampleAF3" $
+      map sort (completeExt exampleAF3) @?= [sort ["B", "D"]]
+  , testCase "completeExt exampleAF4 has three extensions" $
+      length (completeExt exampleAF4) @?= 3
+  , testCase "completeExt exampleAF4 content" $ do
+      let exts = map sort (completeExt exampleAF4)
+      sort ["B", "D"] `elem` exts @?= True
+      sort ["A"] `elem` exts @?= True
+      sort ["B"] `elem` exts @?= True
+  ]
+
+preferredExtTests :: TestTree
+preferredExtTests = testGroup "preferredExt"
+  [ testCase "preferredExt exampleAF" $
+      map sort (preferredExt exampleAF) @?= [sort ["A", "C"]]
+  , testCase "preferredExt exampleAF2" $ do
+      let exts = map sort (preferredExt exampleAF2)
+      length exts @?= 2
+      ["A"] `elem` exts @?= True
+      ["B"] `elem` exts @?= True
+  ]
+
+stableExtTests :: TestTree
+stableExtTests = testGroup "stableExt"
+  [ testCase "stableExt exampleAF" $
+      map sort (stableExt exampleAF) @?= [sort ["A", "C"]]
+  , testCase "stableExt exampleAF2" $ do
+      let exts = map sort (stableExt exampleAF2)
+      length exts @?= 2
+      ["A"] `elem` exts @?= True
+      ["B"] `elem` exts @?= True
+  ]
+
+semiStableTests :: TestTree
+semiStableTests = testGroup "semiStable"
+  [ testCase "semiStable exampleAF3 has one labelling" $
+      length (semiStable exampleAF3) @?= 1
+  , testCase "semiStable exampleAF3 content" $ case semiStable exampleAF3 of
+      (s:_) -> sort s @?= sort [("A", Undecided), ("B", In), ("C", Out), ("D", In)]
+      []    -> assertFailure "Expected at least one semi-stable labelling"
+  , testCase "semiStable exampleAF4 has one labelling" $
+      length (semiStable exampleAF4) @?= 1
+  , testCase "semiStable exampleAF4 content" $ case semiStable exampleAF4 of
+      (s:_) -> sort s @?= sort [("A", Out), ("B", In), ("C", Out), ("D", In), ("E", Out)]
+      []    -> assertFailure "Expected at least one semi-stable labelling"
+  ]
+
+semiStableExtTests :: TestTree
+semiStableExtTests = testGroup "semiStableExt"
+  [ testCase "semiStableExt exampleAF3" $
+      map sort (semiStableExt exampleAF3) @?= [sort ["B", "D"]]
+  , testCase "semiStableExt exampleAF4" $
+      map sort (semiStableExt exampleAF4) @?= [sort ["B", "D"]]
+  ]
diff --git a/test/Test/Language/Dung/Input.hs b/test/Test/Language/Dung/Input.hs
new file mode 100644
index 0000000..da3e0a1
--- /dev/null
+++ b/test/Test/Language/Dung/Input.hs
@@ -0,0 +1,79 @@
+module Test.Language.Dung.Input (tests) where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Language.Dung.AF
+import Language.Dung.Input
+import Language.Dung.Output
+
+tests :: TestTree
+tests = testGroup "Language.Dung.Input"
+  [ parseTests
+  , roundTripTests
+  , edgeCaseTests
+  ]
+
+-- Helper to unwrap a Right or fail the test
+expectRight :: Show a => Either a b -> IO b
+expectRight (Right x) = return x
+expectRight (Left err) = assertFailure ("Expected Right but got Left: " ++ show err)
+
+parseTests :: TestTree
+parseTests = testGroup "parseAF"
+  [ testCase "parses single argument" $ do
+      af <- expectRight $ parseAF "arg(a)."
+      af @?= AF ["a"] []
+  , testCase "parses argument and attack" $ do
+      af <- expectRight $ parseAF "arg(a). arg(b). att(a,b)."
+      af @?= AF ["a", "b"] [("a", "b")]
+  , testCase "parses atk syntax" $ do
+      af <- expectRight $ parseAF "arg(a). arg(b). atk(a,b)."
+      af @?= AF ["a", "b"] [("a", "b")]
+  , testCase "parses multi-line input" $ do
+      let input = unlines
+            [ "arg(a)."
+            , "arg(b)."
+            , "arg(c)."
+            , "att(a,b)."
+            , "att(b,c)."
+            ]
+      af <- expectRight $ parseAF input
+      af @?= AF ["a", "b", "c"] [("a", "b"), ("b", "c")]
+  , testCase "parses exampleaf.txt format" $ do
+      let input = "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)."
+      af <- expectRight $ parseAF input
+      af @?= AF ["a","b","c","d","e","f","g"]
+                [("a","b"),("c","b"),("c","d"),("d","c"),("d","e"),("e","g"),("f","e"),("g","f")]
+  , testCase "returns Left on invalid input" $ do
+      let result = parseAF "invalid input"
+      case result of
+        Left _  -> return ()
+        Right _ -> assertFailure "Expected parse error"
+  ]
+
+roundTripTests :: TestTree
+roundTripTests = testGroup "round-trip"
+  [ testCase "parse . toCegartix identity for simple AF" $ do
+      let af = AF ["a", "b", "c"] [("a", "b"), ("b", "c")] :: DungAF String
+          output = toCegartix af
+      case parseAF output of
+        Left err  -> assertFailure $ "Parse error: " ++ show err
+        Right af' -> af' @?= af
+  , testCase "parse . toCegartix identity for self-attacking AF" $ do
+      let af = AF ["a", "b"] [("a", "a"), ("a", "b")] :: DungAF String
+          output = toCegartix af
+      case parseAF output of
+        Left err  -> assertFailure $ "Parse error: " ++ show err
+        Right af' -> af' @?= af
+  ]
+
+edgeCaseTests :: TestTree
+edgeCaseTests = testGroup "edge cases"
+  [ testCase "single argument, no attacks" $ do
+      af <- expectRight $ parseAF "arg(x)."
+      af @?= AF ["x"] []
+  , testCase "string literal argument names" $ do
+      af <- expectRight $ parseAF "arg(\"hello\"). arg(\"world\"). att(\"hello\", \"world\")."
+      af @?= AF ["hello", "world"] [("hello", "world")]
+  ]
diff --git a/test/Test/Language/Dung/Properties.hs b/test/Test/Language/Dung/Properties.hs
new file mode 100644
index 0000000..1fe6b32
--- /dev/null
+++ b/test/Test/Language/Dung/Properties.hs
@@ -0,0 +1,81 @@
+module Test.Language.Dung.Properties (tests) where
+
+import Data.List (sort)
+import qualified Data.Set as Set
+import Test.Tasty
+import Test.Tasty.QuickCheck
+
+import Language.Dung.AF
+
+-- Generate small AFs with 3-5 arguments for tractable computation
+newtype SmallAF = SmallAF (DungAF String)
+  deriving (Show)
+
+instance Arbitrary SmallAF where
+  arbitrary = do
+    n <- choose (3, 5 :: Int)
+    let args = map (\i -> "a" ++ show i) [1..n]
+    numAtks <- choose (0, n * n `div` 2)
+    atks <- vectorOf numAtks $ do
+      from <- elements args
+      to   <- elements args
+      return (from, to)
+    -- Remove duplicate attacks
+    let uniqueAtks = Set.toList . Set.fromList $ atks
+    return $ SmallAF (AF args uniqueAtks)
+
+-- Helper: check if a set is a subset of another
+isSubsetOf :: Ord a => [a] -> [a] -> Bool
+isSubsetOf xs ys = Set.fromList xs `Set.isSubsetOf` Set.fromList ys
+
+tests :: TestTree
+tests = testGroup "QuickCheck Properties"
+  [ groundedProperties
+  , preferredProperties
+  , stableProperties
+  , semanticRelationProperties
+  ]
+
+groundedProperties :: TestTree
+groundedProperties = testGroup "grounded"
+  [ testProperty "grounded extension is conflict-free" $ \(SmallAF af) ->
+      conflictFree af (groundedExt af)
+  , testProperty "grounded extension is admissible" $ \(SmallAF af) ->
+      admissible af (groundedExt af)
+  , testProperty "grounded labelling covers all arguments" $ \(SmallAF af@(AF args _)) ->
+      sort (map fst (grounded af)) == sort args
+  ]
+
+preferredProperties :: TestTree
+preferredProperties = testGroup "preferred"
+  [ testProperty "every preferred extension is admissible" $ \(SmallAF af) ->
+      all (admissible af) (preferredExt af)
+  , testProperty "every preferred extension is conflict-free" $ \(SmallAF af) ->
+      all (conflictFree af) (preferredExt af)
+  , testProperty "at least one preferred extension exists" $ \(SmallAF af) ->
+      not (null (preferredExt af))
+  ]
+
+stableProperties :: TestTree
+stableProperties = testGroup "stable"
+  [ testProperty "every stable extension is also a preferred extension" $ \(SmallAF af) ->
+      let stExts = map sort (stableExt af)
+          prExts = map sort (preferredExt af)
+      in all (`elem` prExts) stExts
+  , testProperty "every stable extension is conflict-free" $ \(SmallAF af) ->
+      all (conflictFree af) (stableExt af)
+  ]
+
+semanticRelationProperties :: TestTree
+semanticRelationProperties = testGroup "semantic relations"
+  [ testProperty "grounded is the smallest complete extension" $ \(SmallAF af) ->
+      let gExt = sort (groundedExt af)
+          cExts = completeExt af
+      in all (\ce -> gExt `isSubsetOf` ce) cExts
+  , testProperty "every complete extension is admissible" $ \(SmallAF af) ->
+      all (admissible af) (completeExt af)
+  , testProperty "groundedF agrees with groundedExt" $ \(SmallAF af) ->
+      sort (groundedF (f af)) == sort (groundedExt af)
+  , testProperty "groundedF' agrees with groundedExt" $ \(SmallAF af) ->
+      sort (groundedF' (f af)) == sort (groundedExt af)
+  ]