diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,6 +10,16 @@
 Unreleased
 ----------
 
+[0.1.3.0] - 2018-03-14
+----------------------
+
+### Changed
+
+    * Changed name and description of data files.
+    * Fixed bug that caused assumptions not to be simplified.
+
+
+
 [0.1.2.0] - 2018-01-19
 ----------------------
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -9,16 +9,20 @@
 Installation
 ------------------------------------------------------------------------------
 
-After cloning the repository, the recommended installation method is through 
-[Stack](https://www.stackage.org/):
+`judge` can be installed through 
+[Cabal](https://www.haskell.org/cabal/users-guide/):
 
-    stack install judge
+    cabal sandbox init
+    cabal install judge
 
-Alternatively, `judge` can be installed through 
-[Cabal](https://www.haskell.org/cabal/users-guide/).
 
+A recommended alternative is to use [Stack](https://www.stackage.org/), for 
+which you will need to clone the repository and do:
 
+    stack install
 
+
+
 Usage
 -------------------------------------------------------------------------------
 
@@ -26,7 +30,8 @@
 or [JSON](http://json.org/) format. This file will specify the type of proof 
 system and the logical family (although at the moment, only the respective 
 values `tableau` and `justification` are recognised). It also provides the 
-rules of inference. See the [logic](logic) directory for examples.
+rules of inference. See the [logic](logic) directory for example 
+specifications.
 
 If no target formula(s) are provided via `-g`, formulas are read off the 
 standard input. If no output file is provided via `-o`, the result is written 
@@ -34,10 +39,10 @@
 to obtain LaTeX code instead. 
 
 For example, the following will construct proofs for [theorems](formulas.txt) 
-of the logic [Jcs](logic/J.yml) (with `c:(A→B→A) ∊ CS`), and produces a PDF 
+of the logic [LP](logic/LP.yml) (with `c:(A→B→A) ∊ CS`), and produces a PDF 
 file to visualise them:
 
-    judge logic/J.yml \
+    judge LP \
         -a "c:(A->B->A)" \
         -f LaTeX \
          < formulas.txt \
@@ -49,8 +54,7 @@
 -------------------------------------------------------------------------------
 
 Notable missing features are detailed on the [issue 
-tracker](https://github.com/slakkenhuis/judge/issues) 
-([export](https://api.github.com/repos/slakkenhuis/judge/issues)).
+tracker](https://github.com/slakkenhuis/judge/issues).
 
 Contributions that extend `judge` to different logical families (modal, first 
 order...) or proof systems (sequent, natural deduction...) are welcomed.
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -46,12 +46,6 @@
                     <$> (deserialise yaml :: IO (T.TableauSystem F.Justification))
                     <*> (CLI.assumptions arg :: IO [F.FormulaJL])
 
-                -- Tableau system is not prettyprinted well, so won't be shown
-                -- even in verbose mode for now
-                --if CLI.verbose arg
-                --    then write stderr $ pretty sys
-                --    else return ()
-
                 targets <- CLI.goals arg :: IO [F.FormulaJL]
                 file <- CLI.outfile arg
                 let format = CLI.format arg 
diff --git a/formulas.txt b/formulas.txt
--- a/formulas.txt
+++ b/formulas.txt
@@ -3,18 +3,21 @@
 ##############################################################################
 
 # A simple propositional test
-(~r → p) & (r → q) -> (p | q)
+(~r -> p) & (r -> q) -> (p | q)
 
-# The Application axiom should derive instantly in both j0-new and j0-ghari
-x:A → y:(A → B) -> y*x:B
+# The Application axiom should derive instantly in both J0 and J0-PB
+x:A → y:(A → B) → y*x:B
 
 # ... and this one should fail instantly
-x:A → y:(A → B) -> x*y:B
+x:A → y:(A → B) → x*y:B
 
-# This is a good one: it works in both j0-new and j0-ghari, but inspects about 
+# Using proof checker, should work only in LP
+x:a → y:(x:a → b) → y·!x:b
+
+# This is a good one: it works in both J0 and J0-PB, but inspects about 
 # 18000 formulas in the latter (or 8000 if x:A is in the CS instead of the
 # antecedent)
 x:A → y:(A → B) → y*(x+x'):B
 
-# ... And this one just gets too complex to find at all
+# ... and this one just gets too complex to find at all
 x:A → y:(A → B) → (y+y')*x:B
diff --git a/judge.cabal b/judge.cabal
--- a/judge.cabal
+++ b/judge.cabal
@@ -1,8 +1,8 @@
 name:                   judge
-version:                0.1.2.0
-synopsis:               Tableau-based theorem prover.
+version:                0.1.3.0
+synopsis:               Tableau-based theorem prover for justification logic.
 description:            An implementation of a decision procedure for classical 
-                        logic and justification logic.
+                        propositional logic and justification logic.
 homepage:               https://github.com/slakkenhuis/judge#readme
 license:                GPL-3
 license-file:           LICENSE
@@ -13,9 +13,10 @@
 extra-source-files:     README.md
                       , CHANGELOG.md
                       , formulas.txt
-data-files:             logic/J.yml
+data-files:             logic/J0.yml
                       , logic/LP.yml
-                      , logic/J-ghari.yml
+                      , logic/J0-PB.yml
+                      , logic/example.yml
 cabal-version:          >=1.10
 
 library
diff --git a/logic/J-ghari.yml b/logic/J-ghari.yml
deleted file mode 100644
--- a/logic/J-ghari.yml
+++ /dev/null
@@ -1,81 +0,0 @@
-logic: justification
-system: tableau
-name: J₀
-description: |
-    This system stays mostly faithful to the one described in Ghari 2016. The 
-    CSr rule was not present in the original; it emulates closure upon
-    encountering [F] φ on the branch for some φ ∊ CS.
-rules:
-    - name: "Te"
-      consume: ["[T] T:A"]
-      produce:
-            - ["[T, e] T:A"]
-
-    - name: "Fe"
-      consume: ["[F] T:A"]
-      produce:
-          - ["[F, e] T:A"]
-
-    - name: "F→"
-      consume: ["[F] A → B"]
-      produce: 
-          - ["[T] A", "[F] B"]
-
-    - name: "T→"
-      consume: ["[T] A -> B"]
-      produce:
-          - ["[F] A"]
-          - ["[T] B"]
-
-    - name: "F+"
-      consume: ["[F, e] T+S:A"]
-      produce:
-          - ["[F, e] T:A", "[F, e] S:A"]
-
-    - name: "T·"
-      consume: ["[T, e] S:(A → B)", "[T, e] T:A"]
-      produce:
-          - ["[T, e] (S * T) : B"]
-      restrict:
-          and:
-              - match: "A → B"
-                with: [subterms, formulas]
-                in:
-                    union: [root, assumptions]
-              - match: "S * T"
-                with: subterms
-                in: root
-    - name: "CSr"
-      consume: []
-      produce:
-          - ["[T] A"]
-      generate:
-          match: "A"
-          with: all
-          in: assumptions
-    - name: "PBe"
-      consume: []
-      produce:
-          - ["[T, e] T:A"]
-          - ["[F, e] T:A"]
-      generate:
-          and:
-              - match: "A"
-                with: [subterms, formulas]
-                in: 
-                    union: [root, assumptions]
-              - match: "T"
-                with: [subterms, justifications]
-                in: root
-
-    - name: "PBf"
-      consume: []
-      produce:
-          - ["[T] A"]
-          - ["[F] A"]
-      generate:
-          match: "A"
-          with: [subterms, formulas]
-          in: 
-              union: [root, assumptions]
-
diff --git a/logic/J.yml b/logic/J.yml
deleted file mode 100644
--- a/logic/J.yml
+++ /dev/null
@@ -1,38 +0,0 @@
-logic: justification
-system: tableau
-name: J₀
-description: |
-    This is the system described in my thesis.
-rules:
-    - name: "F→"
-      consume: ["[F] A → B"]
-      produce: 
-          - ["[T] A", "[F] B"]
-    - name: "F+"
-      consume: ["[F] T+S:A"]
-      produce: 
-          - ["[F] T:A", "[F] S:A"]
-    - name: "T→"
-      consume: ["[T] A -> B"]
-      produce:
-          - ["[F] A"]
-          - ["[T] B"]
-    - name: "F·"
-      consume: ["[F] (S * T) : B"]
-      produce:
-          - ["[F] S:(A → B)"]
-          - ["[F] T:A"]
-      generate:
-          match: "A → B"
-          with: [subterms, formulas]
-          in:
-              union: [root, assumptions]
-    - name: "CSr"
-      consume: []
-      produce:
-          - ["[T] A"]
-      generate:
-          match: "A"
-          with: all
-          in: assumptions
-assumptions: []
diff --git a/logic/J0-PB.yml b/logic/J0-PB.yml
new file mode 100644
--- /dev/null
+++ b/logic/J0-PB.yml
@@ -0,0 +1,86 @@
+logic: justification
+system: tableau
+name: J₀
+description: |
+    This is a system for the justification logic J0 (and Jcs, when formulas 
+    from the constant specification are added.
+    
+    It is decidable through the addition of the principle of bivalence, as 
+    suggested by Finger (2010) and Ghari (2016). This particular system is 
+    based on the one described by Ghari, although the rule CSr was not
+    present in the original; it emulates closure of the branch upon 
+    encountering [F] φ for some φ ∊ CS.
+rules:
+    - name: "Te"
+      consume: ["[T] T:A"]
+      produce:
+            - ["[T, e] T:A"]
+
+    - name: "Fe"
+      consume: ["[F] T:A"]
+      produce:
+          - ["[F, e] T:A"]
+
+    - name: "F→"
+      consume: ["[F] A → B"]
+      produce: 
+          - ["[T] A", "[F] B"]
+
+    - name: "T→"
+      consume: ["[T] A -> B"]
+      produce:
+          - ["[F] A"]
+          - ["[T] B"]
+
+    - name: "F+"
+      consume: ["[F, e] T+S:A"]
+      produce:
+          - ["[F, e] T:A", "[F, e] S:A"]
+
+    - name: "T·"
+      consume: ["[T, e] S:(A → B)", "[T, e] T:A"]
+      produce:
+          - ["[T, e] (S * T) : B"]
+      restrict:
+          and:
+              - match: "A → B"
+                with: [subterms, formulas]
+                in:
+                    union: [root, assumptions]
+              - match: "S · T"
+                with: subterms
+                in: root
+    - name: "CSr"
+      consume: []
+      produce:
+          - ["[T] A"]
+      generate:
+          match: "A"
+          with: all
+          in: assumptions
+    - name: "PBe"
+      consume: []
+      produce:
+          - ["[T, e] T:A"]
+          - ["[F, e] T:A"]
+      generate:
+          and:
+              - match: "A"
+                with: [subterms, formulas]
+                in: 
+                    union: [root, assumptions]
+              - match: "T"
+                with: [subterms, justifications]
+                in: root
+
+    - name: "PBf"
+      consume: []
+      produce:
+          - ["[T] A"]
+          - ["[F] A"]
+      generate:
+          match: "A"
+          with: [subterms, formulas]
+          in: 
+              union: [root, assumptions]
+
diff --git a/logic/J0.yml b/logic/J0.yml
new file mode 100644
--- /dev/null
+++ b/logic/J0.yml
@@ -0,0 +1,38 @@
+logic: justification
+system: tableau
+name: J₀
+description: |
+    This is the system for J₀ (and Jcs, if the constant specification is 
+    added) described in my Master's thesis.
+rules:
+    - name: "F→"
+      consume: ["[F] φ → ψ"]
+      produce: 
+          - ["[T] φ", "[F] ψ"]
+    - name: "F+"
+      consume: ["[F] T+S:φ"]
+      produce: 
+          - ["[F] T:φ", "[F] S:φ"]
+    - name: "T→"
+      consume: ["[T] φ → ψ"]
+      produce:
+          - ["[F] φ"]
+          - ["[T] ψ"]
+    - name: "F·"
+      consume: ["[F] (S · T) : ψ"]
+      produce:
+          - ["[F] S:(φ → ψ)"]
+          - ["[F] T:φ"]
+      generate:
+          match: "φ → ψ"
+          with: [subterms, formulas]
+          in:
+              union: [root, assumptions]
+    - name: "CSr"
+      consume: []
+      produce:
+          - ["[T] φ"]
+      generate:
+          match: "φ"
+          with: all
+          in: assumptions
diff --git a/logic/LP.yml b/logic/LP.yml
--- a/logic/LP.yml
+++ b/logic/LP.yml
@@ -2,7 +2,8 @@
 system: tableau
 name: Logic of proofs
 description: |
-    This is the system for LP described in my thesis.
+    This is the system for LP (and LPcs, if the constant specification is 
+    added) described in my Master's thesis.
 rules:
     - name: "F→"
       consume: ["[F] A → B"]
@@ -21,7 +22,7 @@
       produce:
           - ["[F] T:A"]
     - name: "T→"
-      consume: ["[T] A -> B"]
+      consume: ["[T] A → B"]
       produce:
           - ["[F] A"]
           - ["[T] B"]
diff --git a/logic/example.yml b/logic/example.yml
new file mode 100644
--- /dev/null
+++ b/logic/example.yml
@@ -0,0 +1,38 @@
+logic: "justification"
+system: "tableau"
+rules:
+    - name: "F→"
+      consume: ["[F] φ → ψ"]
+      produce: 
+          - - "[T] φ"
+            - "[F] ψ"
+    - name: "T→"
+      consume: ["[T] φ → ψ"]
+      produce:
+          - - "[F] φ"
+          - - "[T] ψ"
+    - name: "T·"
+      consume: ["[T] S:(φ → ψ)", "[T] T:φ"]
+      produce:
+          - - "[T] S·T:ψ"
+      restrict:
+          and:
+              - match: "φ → ψ"
+                with: ["subterms", "formulas"]
+                in:
+                    union: ["root", "assumptions"]
+              - match: "S · T"
+                with: "subterms"
+                in: "root"
+    - name: "CSr"
+      consume: []
+      produce:
+          - - "[T] φ"
+      generate:
+          match: "φ"
+          with: "all"
+          in: "assumptions"
+      compose: "greedy"
+assumptions:
+    - "c:(A→(B→A))"
+
diff --git a/src/Logic/Judge/Formula/Datastructure.hs b/src/Logic/Judge/Formula/Datastructure.hs
--- a/src/Logic/Judge/Formula/Datastructure.hs
+++ b/src/Logic/Judge/Formula/Datastructure.hs
@@ -116,9 +116,6 @@
 instance Functor Marked where
     fmap f (Marked marks x) = Marked marks (f x)
 
---mark :: [String] -> Marked a -> Marked a
---mark new (Marked old x) = Marked (new ++ old) x
-
 
 
 -- BASIC MANIPULATIONS -------------------------------------------------------
diff --git a/src/Logic/Judge/Prover/Tableau.hs b/src/Logic/Judge/Prover/Tableau.hs
--- a/src/Logic/Judge/Prover/Tableau.hs
+++ b/src/Logic/Judge/Prover/Tableau.hs
@@ -360,7 +360,7 @@
     initκ = TableauSettings
         { rulesC = rulesC
         , root = value $ L.current root
-        , assumptions = assumptions' system
+        , assumptions = map F.simplify $ assumptions' system
         }
 
     -- | Initial branch