diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2012, Henning Thielemann
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * The names of contributors may not be used to endorse or promote
+      products derived from this software without specific prior
+      written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#! /usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
diff --git a/src/UniqueLogic/ST/Expression.hs b/src/UniqueLogic/ST/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/Expression.hs
@@ -0,0 +1,191 @@
+module UniqueLogic.ST.Expression (
+   T,
+   -- * Construct primitive expressions
+   constant, fromVariable,
+   -- * Operators from rules with small numbers of arguments
+   fromRule1, fromRule2, fromRule3,
+   -- * Operators from rules with any number of arguments
+   Apply, arg, runApply,
+   -- * Predicates on expressions
+   (=:=),
+   -- * Common operators (see also 'Num' and 'Fractional' instances)
+   (=!=),
+   sqr, sqrt,
+   max, maximum,
+   pair,
+   ) where
+
+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.Applicative (Applicative, pure, liftA, liftA2, (<*>), )
+
+-- import Control.Category ((.))
+-- import Data.Maybe (Maybe)
+
+-- import Prelude (Double, Eq, Ord, (+), (*), (/))
+import qualified Prelude as P
+import Prelude hiding (max, maximum, sqrt)
+
+
+{- |
+An expression is defined by a set of equations
+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))
+
+
+{- |
+Make a constant expression of a simple numeric value.
+-}
+constant :: a -> T s a
+constant = Cons . Sys.constant
+
+fromVariable :: Sys.Variable s a -> T s a
+fromVariable = Cons . return
+
+
+fromRule1 ::
+   (Sys.Variable s a -> Sys.M s ()) ->
+   (T 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)
+fromRule2 rule (Cons x) = Cons $ do
+   xv <- x
+   yv <- Sys.localVariable
+   rule xv yv
+   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)
+fromRule3 rule (Cons x) (Cons y) = Cons $ do
+   xv <- x
+   yv <- y
+   zv <- Sys.localVariable
+   rule xv yv zv
+   return zv
+
+
+newtype Apply s f = Apply (Sys.M s f)
+
+instance Functor (Apply s) where
+   fmap f (Apply a) = Apply $ fmap f a
+
+instance Applicative (Apply s) where
+   pure a = Apply $ return a
+   Apply f <*> Apply a = Apply $ ap f a
+
+
+{- |
+This function allows to generalize 'fromRule2' and 'fromRule3' to more arguments
+using 'Applicative' combinators.
+
+Example:
+
+> fromRule3 rule x y
+>    = runApply $ liftA2 rule (arg x) (arg y)
+>    = runApply $ pure rule <*> arg x <*> arg y
+
+Building rules with 'arg' provides more granularity
+than using auxiliary 'pair' rules!
+-}
+arg ::
+   T s a -> Apply s (Sys.Variable s a)
+arg (Cons x) = Apply x
+
+runApply ::
+   Apply s (Sys.Variable s a -> Sys.M s ()) ->
+   T s a
+runApply (Apply rule) = Cons $ do
+   f <- rule
+   xv <- Sys.localVariable
+   f xv
+   return xv
+
+{-
+examples of how to use 'arg' and 'runApply'
+-}
+_fromRule2 rule x = runApply $ liftA rule $ arg x
+_fromRule3 rule x y = runApply $ liftA2 rule (arg x) (arg y)
+
+
+instance (P.Fractional a) => P.Num (T 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)
+
+instance (P.Fractional a) => P.Fractional (T 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 = fromRule2 Rule.square
+
+sqrt :: P.Floating a => T s a -> T s a
+sqrt = fromRule2 (flip Rule.square)
+
+
+infixl 4 =!=
+
+(=!=) :: (Eq a) => T s a -> T s a -> T s a
+(=!=) (Cons x) (Cons y) = Cons $ do
+   xv <- x
+   yv <- y
+   Rule.equ xv yv
+   return xv
+
+infix 0 =:=
+
+(=:=) :: (Eq a) => T s a -> T s a -> Sys.M s ()
+(=:=) (Cons x) (Cons y) = do
+   xv <- x
+   yv <- y
+   Rule.equ xv yv
+
+
+{- |
+We are not able to implement a full Ord instance
+including Eq superclass and comparisons,
+but we need to compute maxima.
+-}
+max :: (Ord a) => T s a -> T s a -> T s a
+max = fromRule3 Rule.max
+
+maximum :: (Ord a) => [T s a] -> T s a
+maximum = foldl1 max
+
+
+{- |
+Construct or decompose a pair.
+-}
+pair :: T s a -> T s b -> T 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
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/Rule.hs
@@ -0,0 +1,102 @@
+module UniqueLogic.ST.Rule (
+   -- * Custom rules
+   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 qualified Prelude as P
+import Prelude hiding (max)
+
+
+generic2 :: String ->
+   (b -> a) -> (a -> b) ->
+   Sys.Variable s a -> Sys.Variable s b -> Sys.M s ()
+generic2 name f g x y =
+   sequence_ $
+   Sys.assignment2 (name++"0") f y x :
+   Sys.assignment2 (name++"1") g x y :
+   []
+
+generic3 :: String ->
+   (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 =
+   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 :
+   []
+
+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 ()
+max =
+   Sys.assignment3 "Max" P.max
+
+pair ::
+   Sys.Variable s a -> Sys.Variable s b -> Sys.Variable s (a,b) -> Sys.M 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) (**)
+
+
+-- * Example equation system
+
+{- |
+> 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
+         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))
diff --git a/src/UniqueLogic/ST/System.hs b/src/UniqueLogic/ST/System.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/System.hs
@@ -0,0 +1,152 @@
+module UniqueLogic.ST.System (
+   -- * Preparation
+   Variable,
+   globalVariable,
+   -- * Posing statements
+   M,
+   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.Maybe (MaybeT(MaybeT), runMaybeT, )
+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
+
+
+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
+
+query :: Variable s a -> ST s (Maybe a)
+query = readSTRef . valueRef
+
+
+
+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 ->
+   (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 :)
+
+assignment3, _assignment3 ::
+   String ->
+   (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
+
+
+{- |
+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 :)
+
+
+{-
+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))
diff --git a/src/UniqueLogic/ST/Test.hs b/src/UniqueLogic/ST/Test.hs
new file mode 100644
--- /dev/null
+++ b/src/UniqueLogic/ST/Test.hs
@@ -0,0 +1,76 @@
+module Main where
+
+import qualified UniqueLogic.ST.Expression as Expr
+import qualified UniqueLogic.ST.System as Sys
+import UniqueLogic.ST.Expression ((=:=))
+
+import qualified Control.Monad.Trans.Class as MT
+import qualified Control.Monad.Trans.Writer as MW
+import Control.Monad.ST (ST, runST, )
+import Control.Monad (join, liftM2, )
+import Data.Monoid (Monoid(mempty, mappend))
+
+import Data.List (sortBy, )
+import Data.Ord.HT (comparing, )
+
+import qualified Data.NonEmpty as NonEmpty
+import qualified Test.QuickCheck as QC
+
+
+shuffle :: NonEmpty.T [] Int -> [a] -> [a]
+shuffle order =
+   map snd . sortBy (comparing fst) .
+   zip (NonEmpty.flatten $ NonEmpty.cycle order)
+
+newtype Check s = Check {runCheck :: ST s Bool}
+
+instance Monoid (Check s) where
+   mempty = Check $ return True
+   mappend (Check x) (Check y) = Check $ liftM2 (&&) x y
+
+{-
+Take a system of six equations and seven variables
+where one variable is randomly chosen and initialized with the correct value.
+The other six variables must be determined by the solver.
+Then we pose the six equations and
+finally check whether all variables got the right value.
+-}
+example :: Int -> NonEmpty.T [] Int -> Bool
+example var order =
+   runST
+      (join . fmap runCheck . Sys.solve $ MW.execWriterT $ do
+         let variable ::
+                Int -> Rational ->
+                MW.WriterT (Check s) (Sys.M s) (Expr.T s Rational)
+             variable n x = do
+                v <-
+                   MT.lift $
+                   if mod var 7 == n
+                     then Sys.constant x
+                     else Sys.localVariable
+                MW.tell $ Check $ fmap (Just x ==) $ Sys.query v
+                return $ Expr.fromVariable v
+
+         c  <- variable 0 1
+         x0 <- variable 1 2
+         x1 <- variable 2 3
+         y0 <- variable 3 4
+         y1 <- variable 4 5
+         z0 <- variable 5 6
+         z1 <- variable 6 7
+
+         MT.lift $ sequence_ $ shuffle order $
+            (c+1 =:= x0) :
+            (x1*2 =:= x0*3) :
+            (2*c + y0/2 =:= 4) :
+            (y0 =:= subtract 1 y1) :
+            (c =:= z0/6) :
+            (z0*z1 =:= 42) :
+            [] )
+
+
+tests :: [(String, IO ())]
+tests = [("example", QC.quickCheck example)]
+
+main :: IO ()
+main = mapM_ (\(msg, test) -> putStr (msg ++ " ") >> test) tests
diff --git a/unique-logic.cabal b/unique-logic.cabal
new file mode 100644
--- /dev/null
+++ b/unique-logic.cabal
@@ -0,0 +1,74 @@
+Name:             unique-logic
+Version:          0.2
+License:          BSD3
+License-File:     LICENSE
+Author:           Henning Thielemann
+Maintainer:       Henning Thielemann <haskell@henning-thielemann.de>
+Homepage:         http://code.haskell.org/~thielema/unique-logic/
+Category:         Logic programming
+Synopsis:         Solve simple simultaneous equations
+Description:
+  Solve a number of equations simultaneously.
+  This is not Computer Algebra,
+  better think of a kind of type inference algorithm
+  or logic programming with only one allowed solution.
+  .
+  Only one solution is computed.
+  Simultaneous equations with multiple solutions are not allowed.
+  However, variables may remain undefined.
+  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:
+  .
+  * "UniqueLogic.ST.System":
+    Construct and solve sets of functional dependencies.
+    Example: @assignment3 (+) a b c@ meaning dependency @a+b -> c@.
+  .
+  * "UniqueLogic.ST.Rule":
+    Combine functional dependencies to rules
+    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@.
+  .
+  * "UniqueLogic.ST.Expression":
+    Allow to write rules using arithmetic operators.
+    It creates temporary variables automatically.
+    Example: @(a+b)*c =:= d@ resolves to @a+b = x, x*c = d@.
+Tested-With:       GHC==7.4.2
+Cabal-Version:     >=1.8
+Build-Type:        Simple
+
+Source-Repository this
+  Tag:         0.2
+  Type:        darcs
+  Location:    http://code.haskell.org/~thielema/unique-logic/
+
+Source-Repository head
+  Type:        darcs
+  Location:    http://code.haskell.org/~thielema/unique-logic/
+
+Library
+  Build-Depends:
+    transformers >=0.2 && <0.4,
+    utility-ht >=0.0.1 && <0.1,
+    base >= 4 && <5
+  GHC-Options:      -Wall
+  Hs-Source-Dirs:   src
+
+  Exposed-modules:
+    UniqueLogic.ST.System
+    UniqueLogic.ST.Rule
+    UniqueLogic.ST.Expression
+
+Test-Suite test-unique-logic
+  Type:    exitcode-stdio-1.0
+  Main-Is: src/UniqueLogic/ST/Test.hs
+  GHC-Options: -Wall
+  Build-Depends:
+    QuickCheck >=2.4 && <2.6,
+    unique-logic,
+    non-empty >=0.0 && <0.1,
+    transformers,
+    utility-ht,
+    base