diff --git a/src/UniqueLogic/ST/Example/Expression.hs b/src/UniqueLogic/ST/Example/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/Example/Expression.hs
@@ -0,0 +1,26 @@
+module UniqueLogic.ST.Example.Expression
+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
+ where
+
+import qualified UniqueLogic.ST.Expression as Expr
+import qualified UniqueLogic.ST.System as Sys
+import UniqueLogic.ST.Expression ((=:=))
+
+import Control.Monad.ST (runST, )
+import Control.Monad (liftM2, )
+
+
+example :: (Maybe Double, Maybe Double)
+example =
+   runST (do
+      xv <- Sys.globalVariable
+      yv <- Sys.globalVariable
+      Sys.solve $ do
+         let x = Expr.fromVariable xv
+             y = Expr.fromVariable yv
+         x*3 =:= y/2
+         5 =:= 2+x
+      liftM2
+         (,)
+         (Sys.query xv)
+         (Sys.query yv))
diff --git a/src/UniqueLogic/ST/Example/Label.hs b/src/UniqueLogic/ST/Example/Label.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/Example/Label.hs
@@ -0,0 +1,105 @@
+module UniqueLogic.ST.Example.Label
+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
+ where
+
+import qualified UniqueLogic.ST.Expression as Expr
+import qualified UniqueLogic.ST.Rule as Rule
+import qualified UniqueLogic.ST.SystemLabel as Sys
+import UniqueLogic.ST.Expression ((=:=))
+
+import qualified Control.Monad.Trans.Writer as MW
+import qualified Control.Monad.Trans.Class as MT
+import Control.Monad.Trans.Writer (writer, )
+import Control.Monad.ST (ST, runST, )
+import Control.Monad (liftM2, liftM3, )
+
+import qualified Prelude as P
+import Prelude hiding (max, log)
+
+
+
+data Assign = Assign Name Term
+   deriving (Show)
+
+type Assigns = [Assign]
+
+data Term =
+     Const Rational
+   | Var Name
+   | Max Term Term
+   | Add Term Term
+   | Sub Term Term
+   | Mul Term Term
+   | Div Term Term
+   | Abs Term
+   | Signum Term
+   deriving (Show)
+
+type Name = String
+
+
+instance Num Term where
+   fromInteger n = Const $ fromInteger n
+   (+) = Add
+   (-) = Sub
+   (*) = Mul
+   abs = Abs
+   signum = Signum
+
+instance Fractional Term where
+   fromRational x = Const x
+   (/) = Div
+
+globalVariable ::
+   Name -> ST s (Sys.Variable Assigns s Term)
+globalVariable name =
+   Sys.globalVariable $
+      \x -> writer (Var name, [Assign name x])
+
+constant ::
+   Rational -> Sys.T Assigns s (Sys.Variable Assigns s Term)
+constant = Sys.constant . Const
+
+
+{- |
+> x=1
+> y=2
+> z=3
+
+> x+y=3
+> y*z=6
+> z=3
+-}
+rule :: ((Maybe Term, Maybe Term, Maybe Term), Assigns)
+rule =
+   runST (do
+      x <- globalVariable "x"
+      y <- globalVariable "y"
+      z <- globalVariable "z"
+      MW.runWriterT $ do
+         Sys.solve $ do
+            c3 <- constant 3
+            c6 <- constant 6
+            Rule.add x y c3
+            Rule.mul y z c6
+            Rule.equ z c3
+         MT.lift $ liftM3
+            (,,)
+            (Sys.query x)
+            (Sys.query y)
+            (Sys.query z))
+
+expression :: ((Maybe Term, Maybe Term), Assigns)
+expression =
+   runST (do
+      xv <- globalVariable "x"
+      yv <- globalVariable "y"
+      MW.runWriterT $ do
+         Sys.solve $ do
+            let x = Expr.fromVariable xv
+                y = Expr.fromVariable yv
+            x*3 =:= y/2
+            5 =:= 2+x
+         MT.lift $ liftM2 (,)
+            (Sys.query xv)
+            (Sys.query yv))
diff --git a/src/UniqueLogic/ST/Example/Rule.hs b/src/UniqueLogic/ST/Example/Rule.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/Example/Rule.hs
@@ -0,0 +1,46 @@
+module UniqueLogic.ST.Example.Rule
+{-# DEPRECATED "This module is intended for documentation purposes. Do not import it!" #-}
+ where
+
+import qualified UniqueLogic.ST.Rule as Rule
+import qualified UniqueLogic.ST.System as Sys
+
+import Control.Monad.ST (runST, )
+import Control.Monad (liftM4, )
+
+import qualified Prelude as P
+import Prelude hiding (max)
+
+
+{- |
+> x=1
+> y=2
+> z=3
+> w=3
+
+> x+y=3
+> y*z=6
+> z=3
+> y^w=8
+-}
+example :: (Maybe Double, Maybe Double, Maybe Double, Maybe Double)
+example =
+   runST (do
+      x <- Sys.globalVariable
+      y <- Sys.globalVariable
+      z <- Sys.globalVariable
+      w <- Sys.globalVariable
+      Sys.solve $ do
+         c3 <- Sys.constant 3
+         c6 <- Sys.constant 6
+         c8 <- Sys.constant 8
+         Rule.add x y c3
+         Rule.mul y z c6
+         Rule.equ z c3
+         Rule.pow y w c8
+      liftM4
+         (,,,)
+         (Sys.query x)
+         (Sys.query y)
+         (Sys.query z)
+         (Sys.query w))
diff --git a/src/UniqueLogic/ST/Expression.hs b/src/UniqueLogic/ST/Expression.hs
--- a/src/UniqueLogic/ST/Expression.hs
+++ b/src/UniqueLogic/ST/Expression.hs
@@ -18,10 +18,11 @@
 import qualified UniqueLogic.ST.Rule as Rule
 import qualified UniqueLogic.ST.System as Sys
 
-import Control.Monad.ST (runST, )
-import Control.Monad (liftM2, ap, )
+import Control.Monad (ap, )
 import Control.Applicative (Applicative, pure, liftA, liftA2, (<*>), )
 
+import Data.Monoid (Monoid, )
+
 -- import Control.Category ((.))
 -- import Data.Maybe (Maybe)
 
@@ -35,30 +36,32 @@
 and the variable at the top-level.
 The value of the expression equals the value of the top variable.
 -}
-newtype T s a = Cons (Sys.M s (Sys.Variable s a))
+newtype T var w s a = Cons (Sys.T w s (var w s a))
 
 
 {- |
 Make a constant expression of a simple numeric value.
 -}
-constant :: a -> T s a
+constant :: (Sys.Var var, Monoid w) => a -> T var w s a
 constant = Cons . Sys.constant
 
-fromVariable :: Sys.Variable s a -> T s a
+fromVariable :: var w s a -> T var w s a
 fromVariable = Cons . return
 
 
 fromRule1 ::
-   (Sys.Variable s a -> Sys.M s ()) ->
-   (T s a)
+   (Sys.Var var, Monoid w) =>
+   (var w s a -> Sys.T w s ()) ->
+   (T var w s a)
 fromRule1 rule = Cons $ do
    xv <- Sys.localVariable
    rule xv
    return xv
 
 fromRule2, _fromRule2 ::
-   (Sys.Variable s a -> Sys.Variable s b -> Sys.M s ()) ->
-   (T s a -> T s b)
+   (Sys.Var var, Monoid w) =>
+   (var w s a -> var w s b -> Sys.T w s ()) ->
+   (T var w s a -> T var w s b)
 fromRule2 rule (Cons x) = Cons $ do
    xv <- x
    yv <- Sys.localVariable
@@ -66,8 +69,9 @@
    return yv
 
 fromRule3, _fromRule3 ::
-   (Sys.Variable s a -> Sys.Variable s b -> Sys.Variable s c -> Sys.M s ()) ->
-   (T s a -> T s b -> T s c)
+   (Sys.Var var, Monoid w) =>
+   (var w s a -> var w s b -> var w s c -> Sys.T w s ()) ->
+   (T var w s a -> T var w s b -> T var w s c)
 fromRule3 rule (Cons x) (Cons y) = Cons $ do
    xv <- x
    yv <- y
@@ -76,12 +80,12 @@
    return zv
 
 
-newtype Apply s f = Apply (Sys.M s f)
+newtype Apply w s f = Apply (Sys.T w s f)
 
-instance Functor (Apply s) where
+instance Functor (Apply w s) where
    fmap f (Apply a) = Apply $ fmap f a
 
-instance Applicative (Apply s) where
+instance Applicative (Apply w s) where
    pure a = Apply $ return a
    Apply f <*> Apply a = Apply $ ap f a
 
@@ -100,12 +104,13 @@
 than using auxiliary 'pair' rules!
 -}
 arg ::
-   T s a -> Apply s (Sys.Variable s a)
+   T var w s a -> Apply w s (var w s a)
 arg (Cons x) = Apply x
 
 runApply ::
-   Apply s (Sys.Variable s a -> Sys.M s ()) ->
-   T s a
+   (Sys.Var var, Monoid w) =>
+   Apply w s (var w s a -> Sys.T w s ()) ->
+   T var w s a
 runApply (Apply rule) = Cons $ do
    f <- rule
    xv <- Sys.localVariable
@@ -119,28 +124,28 @@
 _fromRule3 rule x y = runApply $ liftA2 rule (arg x) (arg y)
 
 
-instance (P.Fractional a) => P.Num (T s a) where
+instance (P.Fractional a, Sys.Var var, Monoid w) => P.Num (T var w s a) where
    fromInteger = constant . fromInteger
    (+) = fromRule3 Rule.add
    (-) = fromRule3 (\z x y -> Rule.add x y z)
    (*) = fromRule3 Rule.mul
-   abs = fromRule2 (Sys.assignment2 "abs" abs)
-   signum = fromRule2 (Sys.assignment2 "signum" signum)
+   abs = fromRule2 (Sys.assignment2 abs)
+   signum = fromRule2 (Sys.assignment2 signum)
 
-instance (P.Fractional a) => P.Fractional (T s a) where
+instance (P.Fractional a, Sys.Var var, Monoid w) => P.Fractional (T var w s a) where
    fromRational = constant . fromRational
    (/) = fromRule3 (\z x y -> Rule.mul x y z)
 
-sqr :: P.Floating a => T s a -> T s a
+sqr :: (P.Floating a, Sys.Var var, Monoid w) => T var w s a -> T var w s a
 sqr = fromRule2 Rule.square
 
-sqrt :: P.Floating a => T s a -> T s a
+sqrt :: (P.Floating a, Sys.Var var, Monoid w) => T var w s a -> T var w s a
 sqrt = fromRule2 (flip Rule.square)
 
 
 infixl 4 =!=
 
-(=!=) :: (Eq a) => T s a -> T s a -> T s a
+(=!=) :: (Sys.Var var, Monoid w) => T var w s a -> T var w s a -> T var w s a
 (=!=) (Cons x) (Cons y) = Cons $ do
    xv <- x
    yv <- y
@@ -149,7 +154,7 @@
 
 infix 0 =:=
 
-(=:=) :: (Eq a) => T s a -> T s a -> Sys.M s ()
+(=:=) :: (Sys.Var var, Monoid w) => T var w s a -> T var w s a -> Sys.T w s ()
 (=:=) (Cons x) (Cons y) = do
    xv <- x
    yv <- y
@@ -161,31 +166,15 @@
 including Eq superclass and comparisons,
 but we need to compute maxima.
 -}
-max :: (Ord a) => T s a -> T s a -> T s a
+max :: (Ord a, Sys.Var var, Monoid w) => T var w s a -> T var w s a -> T var w s a
 max = fromRule3 Rule.max
 
-maximum :: (Ord a) => [T s a] -> T s a
+maximum :: (Ord a, Sys.Var var, Monoid w) => [T var w s a] -> T var w s a
 maximum = foldl1 max
 
 
 {- |
 Construct or decompose a pair.
 -}
-pair :: T s a -> T s b -> T s (a,b)
+pair :: (Sys.Var var, Monoid w) => T var w s a -> T var w s b -> T var w s (a,b)
 pair = fromRule3 Rule.pair
-
-
-_example :: (Maybe Double, Maybe Double)
-_example =
-   runST (do
-      xv <- Sys.globalVariable
-      yv <- Sys.globalVariable
-      Sys.solve $ do
-         let x = fromVariable xv
-             y = fromVariable yv
-         x*3 =:= y/2
-         5 =:= 2+x
-      liftM2
-         (,)
-         (Sys.query xv)
-         (Sys.query yv))
diff --git a/src/UniqueLogic/ST/Rule.hs b/src/UniqueLogic/ST/Rule.hs
--- a/src/UniqueLogic/ST/Rule.hs
+++ b/src/UniqueLogic/ST/Rule.hs
@@ -1,102 +1,81 @@
 module UniqueLogic.ST.Rule (
    -- * Custom rules
-   generic2, generic3,
+   generic2,
+   generic3,
    -- * Common rules
    equ, pair, max, add, mul, square, pow,
    ) where
 
 import qualified UniqueLogic.ST.System as Sys
 
-import Control.Monad.ST (runST, )
-import Control.Monad (liftM4, )
+import Data.Monoid (Monoid, )
 
 import qualified Prelude as P
 import Prelude hiding (max)
 
 
-generic2 :: String ->
+generic2 ::
+   (Sys.Var var, Monoid w) =>
    (b -> a) -> (a -> b) ->
-   Sys.Variable s a -> Sys.Variable s b -> Sys.M s ()
-generic2 name f g x y =
+   var w s a -> var w s b -> Sys.T w s ()
+generic2 f g x y =
    sequence_ $
-   Sys.assignment2 (name++"0") f y x :
-   Sys.assignment2 (name++"1") g x y :
+   Sys.assignment2 f y x :
+   Sys.assignment2 g x y :
    []
 
-generic3 :: String ->
+generic3 ::
+   (Sys.Var var, Monoid w) =>
    (b -> c -> a) -> (c -> a -> b) -> (a -> b -> c) ->
-   Sys.Variable s a -> Sys.Variable s b -> Sys.Variable s c -> Sys.M s ()
-generic3 name f g h x y z =
+   var w s a -> var w s b -> var w s c -> Sys.T w s ()
+generic3 f g h x y z =
    sequence_ $
-   Sys.assignment3 (name++"0") f y z x :
-   Sys.assignment3 (name++"1") g z x y :
-   Sys.assignment3 (name++"2") h x y z :
+   Sys.assignment3 f y z x :
+   Sys.assignment3 g z x y :
+   Sys.assignment3 h x y z :
    []
 
-equ :: (Eq a) =>
-   Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()
-equ = generic2 "Equ" id id
 
-max :: (Ord a) =>
-   Sys.Variable s a -> Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()
+equ ::
+   (Sys.Var var, Monoid w) =>
+   var w s a -> var w s a -> Sys.T w s ()
+equ = generic2 id id
+
+max ::
+   (Ord a, Sys.Var var, Monoid w) =>
+   var w s a -> var w s a -> var w s a -> Sys.T w s ()
 max =
-   Sys.assignment3 "Max" P.max
+   Sys.assignment3 P.max
 
+{- |
+You might be tempted to use the 'pair' rule to collect parameters
+for rules with more than three arguments.
+This is generally not a good idea since this way you lose granularity.
+For building rules with more than three arguments,
+please build according assignments with 'Sys.arg' and 'Sys.runApply'
+and bundle these assignments to rules.
+This is the way, 'generic2' and 'generic3' work.
+-}
 pair ::
-   Sys.Variable s a -> Sys.Variable s b -> Sys.Variable s (a,b) -> Sys.M s ()
+   (Sys.Var var, Monoid w) =>
+   var w s a -> var w s b -> var w s (a,b) -> Sys.T w s ()
 pair x y xy =
-   Sys.assignment3 "Pair" (,) x y xy >>
-   Sys.assignment2 "Fst" fst xy x >>
-   Sys.assignment2 "Snd" snd xy y
-
-add :: (Num a) =>
-   Sys.Variable s a -> Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()
-add = generic3 "Add" subtract (-) (+)
-
-mul :: (Fractional a) =>
-   Sys.Variable s a -> Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()
-mul = generic3 "Mul" (flip (/)) (/) (*)
-
-square :: (Floating a) =>
-   Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()
-square = generic2 "Square" sqrt (^(2::Int))
-
-pow :: (Floating a) =>
-   Sys.Variable s a -> Sys.Variable s a -> Sys.Variable s a -> Sys.M s ()
-pow = generic3 "Pow" (\x y -> y ** recip x) (flip logBase) (**)
+   Sys.assignment3 (,) x y xy >>
+   Sys.assignment2 fst xy x >>
+   Sys.assignment2 snd xy y
 
+add :: (Num a, Sys.Var var, Monoid w) =>
+   var w s a -> var w s a -> var w s a -> Sys.T w s ()
+add = generic3 subtract (-) (+)
 
--- * Example equation system
+mul :: (Fractional a, Sys.Var var, Monoid w) =>
+   var w s a -> var w s a -> var w s a -> Sys.T w s ()
+mul = generic3 (flip (/)) (/) (*)
 
-{- |
-> x=1
-> y=2
-> z=3
-> w=3
+square :: (Floating a, Sys.Var var, Monoid w) =>
+   var w s a -> var w s a -> Sys.T w s ()
+square = generic2 sqrt (^(2::Int))
 
-> x+y=3
-> y*z=6
-> z=3
-> y^w=8
--}
-_example :: (Maybe Double, Maybe Double, Maybe Double, Maybe Double)
-_example =
-   runST (do
-      x <- Sys.globalVariable
-      y <- Sys.globalVariable
-      z <- Sys.globalVariable
-      w <- Sys.globalVariable
-      Sys.solve $ do
-         c3 <- Sys.constant 3
-         c6 <- Sys.constant 6
-         c8 <- Sys.constant 8
-         add x y c3
-         mul y z c6
-         equ z c3
-         pow y w c8
-      liftM4
-         (,,,)
-         (Sys.query x)
-         (Sys.query y)
-         (Sys.query z)
-         (Sys.query w))
+pow :: (Floating a, Sys.Var var, Monoid w) =>
+   var w s a -> var w s a -> var w s a -> Sys.T w s ()
+pow = generic3 (\x y -> y ** recip x) (flip logBase) (**)
diff --git a/src/UniqueLogic/ST/RuleLog.hs b/src/UniqueLogic/ST/RuleLog.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/RuleLog.hs
@@ -0,0 +1,35 @@
+module UniqueLogic.ST.RuleLog (
+   -- * Custom rules
+   generic2,
+   generic3,
+   ) where
+
+import qualified UniqueLogic.ST.SystemLog as Sys
+
+import Control.Monad.Trans.Writer (Writer, )
+import Data.Monoid (Monoid, )
+
+import qualified Prelude as P
+import Prelude hiding (max)
+
+
+generic2 ::
+   Monoid w =>
+   (b -> Writer w a) -> (a -> Writer w b) ->
+   Sys.Variable w s a -> Sys.Variable w s b -> Sys.T w s ()
+generic2 f g x y =
+   sequence_ $
+   Sys.assignment2 f y x :
+   Sys.assignment2 g x y :
+   []
+
+generic3 ::
+   Monoid w =>
+   (b -> c -> Writer w a) -> (c -> a -> Writer w b) -> (a -> b -> Writer w c) ->
+   Sys.Variable w s a -> Sys.Variable w s b -> Sys.Variable w s c -> Sys.T w s ()
+generic3 f g h x y z =
+   sequence_ $
+   Sys.assignment3 f y z x :
+   Sys.assignment3 g z x y :
+   Sys.assignment3 h x y z :
+   []
diff --git a/src/UniqueLogic/ST/System.hs b/src/UniqueLogic/ST/System.hs
--- a/src/UniqueLogic/ST/System.hs
+++ b/src/UniqueLogic/ST/System.hs
@@ -1,152 +1,69 @@
 module UniqueLogic.ST.System (
    -- * Preparation
+   Var,
    Variable,
-   globalVariable,
+   Sys.globalVariable,
+   plainVariable,
    -- * Posing statements
-   M,
+   T,
    localVariable,
    constant,
    assignment2,
    assignment3,
-   Apply, arg, runApply,
+   Sys.Apply, arg, runApply,
    -- * Solution
    solve,
    query,
    ) where
 
+import qualified UniqueLogic.ST.SystemLog as Sys
+import UniqueLogic.ST.SystemLog (T, Variable)
+
 import qualified Control.Monad.Trans.Writer as MW
-import qualified Control.Monad.Trans.Class  as MT
-import qualified Data.Foldable as Fold
-import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT, )
+import Control.Applicative (liftA, liftA2, )
 import Control.Monad.ST (ST, )
-import Control.Monad.HT ((<=<), )
-import Control.Monad (when, liftM2, ap, void, )
-import Control.Applicative (Applicative, pure, liftA, liftA2, (<*>), )
-import Data.Functor.Compose (Compose(Compose))
 
-import Data.STRef (STRef, newSTRef, modifySTRef, readSTRef, writeSTRef, )
-import Data.Maybe (isNothing, )
-
-
-data Variable s a =
-   Variable {
-      dependsRef :: STRef s [ST s ()],
-      valueRef :: STRef s (Maybe a)
-   }
-
-newtype M s a =
-   M {runM :: MW.WriterT [STRef s [ST s ()]] (ST s) a}
-
-instance Functor (M s) where
-   fmap f (M x) = M (fmap f x)
-
-instance Applicative (M s) where
-   pure = M . return
-   (<*>) = ap
-
-instance Monad (M s) where
-   return = M . return
-   M x >>= k  = M $ runM . k =<< x
+import Data.Monoid (Monoid, )
 
 
-lift :: ST s a -> M s a
-lift = M . MT.lift
-
-localVariable :: M s (Variable s a)
-localVariable = lift globalVariable
-
-globalVariable :: ST s (Variable s a)
-globalVariable = object Nothing
-
-constant :: a -> M s (Variable s a)
-constant a =
-   do v <- lift $ object $ Just a
-      M $ MW.tell [dependsRef v]
-      return v
-
-object :: Maybe a -> ST s (Variable s a)
-object ma =
-   liftM2 Variable (newSTRef []) (newSTRef ma)
-
-resolve ::
-   STRef s [ST s ()] -> ST s ()
-resolve =
-   sequence_ <=< readSTRef
-
-solve :: M s a -> ST s a
-solve (M m) =
-   do (a,w) <- MW.runWriterT m
-      mapM_ resolve w
-      return a
+class Var var where
+   plainVariable :: var w s a -> Variable w s a
+   runApply ::
+      Monoid w =>
+      Sys.Apply w s a -> var w s a -> T w s ()
+   constant :: (Monoid w) => a -> T w s (var w s a)
+   localVariable :: (Monoid w) => T w s (var w s a)
 
-query :: Variable s a -> ST s (Maybe a)
-query = readSTRef . valueRef
+instance Var Variable where
+   plainVariable = id
+   runApply f = Sys.runApply (fmap return f)
+   constant = Sys.constant
+   localVariable = Sys.localVariable
 
+arg :: (Var var, Monoid w) => var w s a -> Sys.Apply w s a
+arg = Sys.arg . plainVariable
 
 
-updateIfNew :: Variable s a -> MaybeT (ST s) a -> ST s ()
-updateIfNew (Variable al av) act = do
-   as <- readSTRef av
-   when (isNothing as) $ void $ runMaybeT $ do
-      MT.lift . writeSTRef av . Just =<< act
-      MT.lift $ resolve al
-
-readSTRefM :: STRef s (Maybe a) -> MaybeT (ST s) a
-readSTRefM = MaybeT . readSTRef
-
-assignment2, _assignment2 ::
-   String ->
+assignment2 ::
+   (Var var, Monoid w) =>
    (a -> b) ->
-   Variable s a -> Variable s b ->
-   M s ()
-assignment2 _ f (Variable al av) b =
-   let update =
-          updateIfNew b $ fmap f $ readSTRefM av
-   in  lift $
-       modifySTRef al (update :)
+   var w s a -> var w s b ->
+   T w s ()
+assignment2 f a =
+   runApply $ liftA f (arg a)
 
-assignment3, _assignment3 ::
-   String ->
+assignment3 ::
+   (Var var, Monoid w) =>
    (a -> b -> c) ->
-   Variable s a -> Variable s b -> Variable s c ->
-   M s ()
-assignment3 _ f (Variable al av) (Variable bl bv) c =
-   let update =
-          updateIfNew c $
-          liftM2 f (readSTRefM av) (readSTRefM bv)
-   in  lift $
-       modifySTRef al (update :) >>
-       modifySTRef bl (update :)
-
-
-newtype Apply s a =
-   Apply (Compose (MW.Writer [STRef s [ST s ()]]) (MaybeT (ST s)) a)
-
-instance Functor (Apply s) where
-   fmap f (Apply a) = Apply $ fmap f a
-
-instance Applicative (Apply s) where
-   pure a = Apply $ pure a
-   Apply f <*> Apply a = Apply $ f <*> a
+   var w s a -> var w s b -> var w s c ->
+   T w s ()
+assignment3 f a b =
+   runApply $ liftA2 f (arg a) (arg b)
 
 
-{- |
-This function allows to generalize 'assignment2' and 'assignment3' to more arguments.
-You could achieve the same with nested applications of @assignment3 (,)@.
--}
-arg :: Variable s a -> Apply s a
-arg (Variable al av) =
-   Apply $ Compose $ MW.writer (readSTRefM av, [al])
-
-runApply :: String -> Apply s a -> Variable s a -> M s ()
-runApply _ (Apply (Compose w)) a =
-   case MW.runWriter w of
-      (f, refs) ->
-         lift $ Fold.forM_ refs $ flip modifySTRef (updateIfNew a f :)
+solve :: T () s a -> ST s a
+solve = fmap fst . MW.runWriterT . Sys.solve
 
 
-{-
-examples of how to use 'arg' and 'runApply'
--}
-_assignment2 msg f x = runApply msg (liftA f $ arg x)
-_assignment3 msg f x y = runApply msg (liftA2 f (arg x) (arg y))
+query :: (Var var, Monoid w) => var w s a -> ST s (Maybe a)
+query = Sys.query . plainVariable
diff --git a/src/UniqueLogic/ST/SystemLabel.hs b/src/UniqueLogic/ST/SystemLabel.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/SystemLabel.hs
@@ -0,0 +1,46 @@
+module UniqueLogic.ST.SystemLabel (
+   -- * Preparation
+   Variable,
+   globalVariable,
+   -- * Posing statements
+   Sys.T,
+   Sys.localVariable,
+   Sys.constant,
+   Sys.assignment2,
+   Sys.assignment3,
+   Sys.Apply, Sys.arg, Sys.runApply,
+   -- * Solution
+   solve,
+   Sys.query,
+   ) where
+
+import qualified UniqueLogic.ST.System as Sys
+import qualified UniqueLogic.ST.SystemLog as SysLog
+
+import qualified Control.Monad.Trans.Writer as MW
+import Control.Monad.Trans.Writer (Writer, )
+import Control.Monad.ST (ST, )
+
+import Data.Monoid (Monoid, )
+
+import Prelude hiding (log, )
+
+
+data Variable w s a =
+   Variable
+      (a -> Writer w a)
+      (SysLog.Variable w s a)
+
+instance Sys.Var Variable where
+   plainVariable (Variable _ v) = v
+   runApply f (Variable log v) = SysLog.runApply (fmap log f) v
+   constant = fmap (Variable return) . SysLog.constant
+   localVariable = fmap (Variable return) SysLog.localVariable
+
+
+globalVariable :: (a -> MW.Writer w a) -> ST s (Variable w s a)
+globalVariable log = fmap (Variable log) Sys.globalVariable
+
+
+solve :: (Monoid w) => Sys.T w s a -> MW.WriterT w (ST s) a
+solve = SysLog.solve
diff --git a/src/UniqueLogic/ST/SystemLog.hs b/src/UniqueLogic/ST/SystemLog.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/SystemLog.hs
@@ -0,0 +1,167 @@
+module UniqueLogic.ST.SystemLog (
+   -- * Preparation
+   Variable,
+   globalVariable,
+   -- * Posing statements
+   T,
+   localVariable,
+   constant,
+   assignment2,
+   assignment3,
+   Apply, arg, runApply,
+   -- * Solution
+   solve,
+   query,
+   ) where
+
+import qualified Control.Monad.Trans.Writer as MW
+import qualified Control.Monad.Trans.Class  as MT
+import qualified Data.Foldable as Fold
+import Control.Monad.Trans.Writer (WriterT, Writer, )
+import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT, mapMaybeT, )
+import Control.Monad.ST (ST, )
+import Control.Monad.HT ((<=<), )
+import Control.Monad (when, liftM2, ap, void, )
+import Control.Applicative (Applicative, pure, (<*>), )
+import Data.Functor.Compose (Compose(Compose))
+
+import Data.STRef (STRef, newSTRef, modifySTRef, readSTRef, writeSTRef, )
+import Data.Monoid (Monoid, )
+import Data.Maybe (isNothing, )
+
+
+data Variable w s a =
+   Variable {
+      dependsRef :: STRef s [Update w s],
+      valueRef :: STRef s (Maybe a)
+   }
+
+type Update w s = WriterT w (ST s) ()
+
+newtype T w s a =
+   Cons {run :: WriterT [STRef s [Update w s]] (ST s) a}
+
+instance Functor (T w s) where
+   fmap f (Cons x) = Cons (fmap f x)
+
+instance Applicative (T w s) where
+   pure = Cons . return
+   (<*>) = ap
+
+instance Monad (T w s) where
+   return = Cons . return
+   Cons x >>= k  = Cons $ run . k =<< x
+
+
+lift :: ST s a -> T w s a
+lift = Cons . MT.lift
+
+localVariable :: T w s (Variable w s a)
+localVariable = lift globalVariable
+
+globalVariable :: ST s (Variable w s a)
+globalVariable = object Nothing
+
+constant :: a -> T w s (Variable w s a)
+constant a =
+   do v <- lift $ object $ Just a
+      Cons $ MW.tell [dependsRef v]
+      return v
+
+object :: Maybe a -> ST s (Variable w s a)
+object ma =
+   liftM2 Variable (newSTRef []) (newSTRef ma)
+
+resolve ::
+   Monoid w =>
+   STRef s [Update w s] -> Update w s
+resolve =
+   sequence_ <=< MT.lift . readSTRef
+
+solve ::
+   Monoid w =>
+   T w s a -> WriterT w (ST s) a
+solve (Cons m) = do
+   (a,w) <- MT.lift $ MW.runWriterT m
+   mapM_ resolve w
+   return a
+
+query :: Variable w s a -> ST s (Maybe a)
+query = readSTRef . valueRef
+
+
+mw ::
+   (Monoid w, Monad st) =>
+   MaybeT st (Writer w a) -> MaybeT (WriterT w st) a
+--   st (Maybe (Writer w a)) -> WriterT w st (Maybe a)
+mw act = do
+   mwa <- mapMaybeT MT.lift act
+   case MW.runWriter mwa of
+      (a,w) -> MT.lift $ MW.tell w >> return a
+
+updateIfNew ::
+   Monoid w =>
+   Variable w s a -> MaybeT (ST s) (Writer w a) -> Update w s
+updateIfNew (Variable al av) act = do
+   as <- MT.lift $ readSTRef av
+   when (isNothing as) $ void $ runMaybeT $ do
+      MT.lift . MT.lift . writeSTRef av . Just =<< mw act
+      MT.lift $ resolve al
+
+readSTRefM :: STRef s (Maybe a) -> MaybeT (ST s) a
+readSTRefM = MaybeT . readSTRef
+
+
+assignment2 ::
+   Monoid w =>
+   (a -> Writer w b) ->
+   Variable w s a -> Variable w s b ->
+   T w s ()
+assignment2 f (Variable al av) b =
+   let update =
+          updateIfNew b $ fmap f $ readSTRefM av
+   in  lift $
+       modifySTRef al (update :)
+
+assignment3 ::
+   Monoid w =>
+   (a -> b -> Writer w c) ->
+   Variable w s a -> Variable w s b -> Variable w s c ->
+   T w s ()
+assignment3 f (Variable al av) (Variable bl bv) c =
+   let update =
+          updateIfNew c $
+          liftM2 f (readSTRefM av) (readSTRefM bv)
+   in  lift $
+       modifySTRef al (update :) >>
+       modifySTRef bl (update :)
+
+
+data Apply w s a =
+   Apply (Compose (MW.Writer [STRef s [Update w s]]) (MaybeT (ST s)) a)
+
+
+{- |
+This function allows to generalize 'assignment2' and 'assignment3' to more arguments.
+You could achieve the same with nested applications of @assignment3 (,)@.
+-}
+arg :: Monoid w => Variable w s a -> Apply w s a
+arg (Variable al av) =
+   Apply $ Compose $ MW.writer (readSTRefM av, [al])
+
+
+instance Monoid w => Functor (Apply w s) where
+   fmap f (Apply a) = Apply $ fmap f a
+
+instance Monoid w => Applicative (Apply w s) where
+   pure a = Apply $ pure a
+   Apply f <*> Apply a = Apply $ f <*> a
+
+
+runApply ::
+   Monoid w =>
+   Apply w s (Writer w a) -> Variable w s a -> T w s ()
+runApply (Apply (Compose w)) a =
+   case MW.runWriter w of
+      (f, refs) ->
+         lift $ Fold.forM_ refs $ flip modifySTRef (updateIfNew a f :)
diff --git a/src/UniqueLogic/ST/Test.hs b/src/UniqueLogic/ST/Test.hs
--- a/src/UniqueLogic/ST/Test.hs
+++ b/src/UniqueLogic/ST/Test.hs
@@ -40,8 +40,10 @@
    runST
       (join . fmap runCheck . Sys.solve $ MW.execWriterT $ do
          let variable ::
+                (Monoid w) =>
                 Int -> Rational ->
-                MW.WriterT (Check s) (Sys.M s) (Expr.T s Rational)
+                MW.WriterT (Check s) (Sys.T w s)
+                   (Expr.T Sys.Variable w s Rational)
              variable n x = do
                 v <-
                    MT.lift $
diff --git a/unique-logic.cabal b/unique-logic.cabal
--- a/unique-logic.cabal
+++ b/unique-logic.cabal
@@ -1,5 +1,5 @@
 Name:             unique-logic
-Version:          0.2
+Version:          0.3
 License:          BSD3
 License-File:     LICENSE
 Author:           Henning Thielemann
@@ -19,7 +19,7 @@
   We do not even check for consistency,
   since with floating point numbers even simple rules may not be consistent.
   .
-  The modules ordered with respect to abstraction level:
+  The modules ordered with respect to abstraction level are:
   .
   * "UniqueLogic.ST.System":
     Construct and solve sets of functional dependencies.
@@ -30,17 +30,34 @@
     that can apply in multiple directions.
     Example: @add a b c@ means relation @a+b = c@
     which resolves to dependencies @a+b -> c, c-a -> b, c-b -> a@.
+    For an executable example see "UniqueLogic.ST.Example.Rule".
   .
   * "UniqueLogic.ST.Expression":
-    Allow to write rules using arithmetic operators.
+    Allows to write rules using arithmetic operators.
     It creates temporary variables automatically.
     Example: @(a+b)*c =:= d@ resolves to @a+b = x, x*c = d@.
+    For an executable example see "UniqueLogic.ST.Example.Expression".
+  .
+  * "UniqueLogic.ST.SystemLabel":
+    Provides a new type for named variables.
+    When creating a variable you decide whether and how
+    an assignment to this variable shall be logged.
+    There is an example that shows how to solve a logic system
+    using symbolic expressions.
+    The naming and logging allows us to observe shared intermediate results.
+    For an executable example see "UniqueLogic.ST.Example.Label".
+  .
+  * "UniqueLogic.ST.SystemLog", "UniqueLogic.ST.RuleLog":
+    These modules allow to log an assignment
+    depending on the arguments to an assignment.
+    This is more general than "UniqueLogic.ST.SystemLabel"
+    which allows only dependencies on the result of an assignment.
 Tested-With:       GHC==7.4.2
 Cabal-Version:     >=1.8
 Build-Type:        Simple
 
 Source-Repository this
-  Tag:         0.2
+  Tag:         0.3
   Type:        darcs
   Location:    http://code.haskell.org/~thielema/unique-logic/
 
@@ -56,10 +73,17 @@
   GHC-Options:      -Wall
   Hs-Source-Dirs:   src
 
-  Exposed-modules:
+  Exposed-Modules:
     UniqueLogic.ST.System
+    UniqueLogic.ST.SystemLog
+    UniqueLogic.ST.SystemLabel
     UniqueLogic.ST.Rule
+    UniqueLogic.ST.RuleLog
     UniqueLogic.ST.Expression
+    -- example modules
+    UniqueLogic.ST.Example.Rule
+    UniqueLogic.ST.Example.Label
+    UniqueLogic.ST.Example.Expression
 
 Test-Suite test-unique-logic
   Type:    exitcode-stdio-1.0