diff --git a/Control/CP/Herbrand/Herbrand.hs b/Control/CP/Herbrand/Herbrand.hs
--- a/Control/CP/Herbrand/Herbrand.hs
+++ b/Control/CP/Herbrand/Herbrand.hs
@@ -4,6 +4,9 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleContexts #-}
+-- |This module provides a Herbrand solver.
+--
+--  The type of terms is parameterized by the "HTerm" type class.
 module Control.CP.Herbrand.Herbrand where 
 
 import Control.Monad.State.Lazy
@@ -13,7 +16,7 @@
 
 import Control.CP.Solver
 
--- Herbrand terms
+-- |Herbrand terms
 
 type VarId = Int
 
@@ -22,37 +25,50 @@
   isVar    :: t   -> Maybe VarId
   children :: t -> ([t], [t] -> t)
   nonvar_unify
-        :: (MonadState (HState t) m) => t -> t -> m Bool
+        :: (MonadState (HState t m) m) => t -> t -> m Bool
 
--- Herbrand monad
+-- |Herbrand monad
 
-newtype Herbrand t a = Herbrand { unH :: State (HState t) a }
-  deriving (Monad, MonadState (HState t))
+data Herbrand t a = Herbrand { unH :: State (HState t (Herbrand t)) a }
 
+instance Monad (Herbrand t) where
+  return x  = Herbrand $ return x
+  m >>=  f  = Herbrand $ unH m >>= unH . f
+
+instance MonadState (HState t (Herbrand t)) (Herbrand t) where
+  get  = Herbrand $ get
+  put  = Herbrand . put
+
 instance Functor (Herbrand t) where
   fmap f fa  = fa >>= return . f 
 
-
 instance Applicative (Herbrand t) where
   pure         = return
   (<*>) ff fa  = do f <- ff 
                     a <- fa
 	            return $ f a
 
-type Subst t = Map VarId t
+-- |State
 
-data HState t = HState {var_supply :: VarId
-                       ,subst      :: Subst t
-                       }
+type Heap t m   = Map VarId (Binding t m)
 
-updateState :: (HTerm t, MonadState (HState t) m) => (HState t -> HState t) -> m ()
+data Binding t m 
+  = VAR VarId 		-- | indirection to other variable
+  | NONVAR t 		-- | bound to term
+  | ACTION (m Bool)	-- | attributed variable, with given action
+
+data HState t m = HState {var_supply :: VarId
+                         ,heap       :: Heap t m
+                         }
+
+updateState :: (HTerm t, MonadState (HState t m) m) => (HState t m -> HState t m) -> m ()
 updateState f = get >>= put . f
 
--- Solver instance 
+-- |Solver instance 
 
 instance HTerm t => Solver (Herbrand t) where
   type Constraint (Herbrand t)  = Unify t 
-  type Label      (Herbrand t)  = HState t
+  type Label      (Herbrand t)  = HState t (Herbrand t)
   add     = addH
   mark    = get
   goto    = put
@@ -66,54 +82,109 @@
 
 -- New variable
 
-newvarH :: (HTerm t,MonadState (HState t) m) => m t
+newvarH :: (HTerm t,MonadState (HState t m) m) => m t
 newvarH = do state <- get
              let varid = var_supply state
              put state{var_supply = varid + 1}
              return $ mkVar varid
 
+{- Representatin of variables
+   --------------------------
+
+   Each variable is represented by
+   * a VarId
+   * a possible Binding on the Heap
+       - if there is a binding, then the variable's meaning 
+         is that of the binding
+       - if there is no binding, then variable's meaning is 
+         that of an unbound variable
+
+-}
+
 -- Unification
 
 data Unify t = t `Unify` t
 
-addH :: (HTerm t, MonadState (HState t) m) => Unify t -> m Bool
+addH :: (HTerm t, MonadState (HState t m) m) => Unify t -> m Bool
 addH (Unify t1 t2) = unify t1 t2
 
-unify :: (HTerm t, MonadState (HState t) m) => t -> t -> m Bool
+-- | unify two arbitrary terms
+unify :: (HTerm t, MonadState (HState t m) m) => t -> t -> m Bool
 unify t1 t2 = 
   do nt1 <- shallow_normalize t1
      nt2 <- shallow_normalize t2
      case (isVar nt1, isVar nt2) of
        (Just v1, Just v2) 
           | v1 == v2      -> success
-       (Just v1, _      ) -> bind v1 nt2 >> success
-       (_      , Just v2) -> bind v2 nt1 >> success
-       (_      , _      ) -> nonvar_unify nt1 nt2
+	  | otherwise     -> bindv v1 v2
+       (Just v1, Nothing) -> bindt v1 nt2
+       (Nothing, Just v2) -> bindt v2 nt1
+       (Nothing, Nothing) -> nonvar_unify nt1 nt2
 
 success, failure :: Monad m => m Bool
 success  = return True
 failure  = return False
+m1 `andM` m2  = m1 >>= \b -> if b then m2 else return b 
 
-bind :: (HTerm t, MonadState (HState t) m) => VarId -> t -> m ()
-bind v t  = updateState $ \state -> state{subst = insert v t (subst state)}
+-- | bind a variable to a term
+bindt :: (HTerm t, MonadState (HState t m) m) => VarId -> t -> m Bool
+bindt v t  = do r <- lookupVar v
+                updater v (NONVAR t)
+                case r of
+		  Just (ACTION action) -> action
+                  Nothing              -> success
 
+-- | alias one variable to another
+bindv :: (HTerm t, MonadState (HState t m) m) => VarId -> VarId -> m Bool
+bindv v1 v2  = do r1 <- lookupVar v1
+                  r2 <- lookupVar v2
+                  case (r1,r2) of
+                    (Just (ACTION a1), Just (ACTION a2)) 
+				      -> let r3 = noACTION
+                                         in do updater v1 r3
+                                               updater v2 r3
+				               a1 `andM` a2
+                    (Just _, Nothing) -> updater v1 (VAR v2) >> success
+                    (Nothing, Just _) -> updater v2 (VAR v1) >> success
+                    (Nothing,Nothing) -> updater v1 (VAR v2) >> success
+
+             where noACTION = ACTION success
+
+updater v  r  = updateState $ \state -> state{heap = insert v r (heap state)}
+
+lookupVar v  = do state <- get
+                  return $ Data.Map.lookup v (heap state)
+
+-- Actions
+
+registerAction :: (HTerm t, MonadState (HState t m) m) => t -> m Bool -> m ()
+registerAction t action  =
+  do nt <- shallow_normalize t
+     case isVar nt of
+       Just v  ->
+         do r <- lookupVar v
+            case r of
+              Nothing          -> updater v (ACTION action)
+              Just (ACTION a1) -> updater v (ACTION (a1 `andM` action))
+       Nothing -> return ()
+
+-- TODO: unregister action?
+
 -- Normalization
 
-shallow_normalize :: (HTerm t, MonadState (HState t) m) => t -> m t
-shallow_normalize t
-  | Just v <- isVar t    
-     = do state <- get
-          case Data.Map.lookup v (subst state) of
-            Just t' -> shallow_normalize t'
-            Nothing -> return t 
-  | otherwise  
-     = return t
+shallow_normalize :: (HTerm t, MonadState (HState t m) m) => t -> m t
+shallow_normalize t  = gnormalize return t
 
-normalize :: (HTerm t, MonadState (HState t) m) => t -> m t
-normalize t
-  | Just v <- isVar t  = do state <- get
-                            case Data.Map.lookup v (subst state) of
-                              Just t' -> normalize t'
-                              Nothing -> return t
-  | otherwise          = let (ts,mkt)  = children t
-                         in mapM normalize ts >>= return . mkt
+normalize :: (HTerm t, MonadState (HState t m) m) => t -> m t
+normalize t          = gnormalize nvnormalize t
+  where nvnormalize t  =  let (ts,mkt)  = children t
+                          in mapM normalize ts >>= return . mkt
+
+gnormalize nvnormalize t
+  | Just v <- isVar t  = vnormalize v
+  | otherwise          = nvnormalize t
+  where vnormalize v   = do state <- get
+                            case Data.Map.lookup v (heap state) of
+                              Just (VAR v')   -> vnormalize v'
+                              Just (NONVAR t) -> nvnormalize t
+                              _               -> return $ mkVar v
diff --git a/Control/CP/Herbrand/HerbrandT.hs b/Control/CP/Herbrand/HerbrandT.hs
--- a/Control/CP/Herbrand/HerbrandT.hs
+++ b/Control/CP/Herbrand/HerbrandT.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 -- |This module provides a Herbrand solver as a monad transformer.
 --
@@ -19,12 +20,19 @@
 import Control.CP.Solver
 import Control.CP.Herbrand.Herbrand (HState, Unify, HTerm,initState,addH,newvarH)
 
-newtype HerbrandT t m a = HerbrandT { unHT :: StateT (HState t) m a }
-  deriving (MonadTrans, Monad, MonadState (HState t))
+newtype HerbrandT t s a = HerbrandT { unHT :: StateT (HState t (HerbrandT t s)) s a }
+  deriving Monad
 
+instance MonadTrans (HerbrandT t) where
+  lift = HerbrandT . lift
+
+instance Solver s =>MonadState (HState t (HerbrandT t s)) (HerbrandT t s)  where
+  get = HerbrandT get
+  put = HerbrandT . put
+
 instance (Solver s, HTerm t) => Solver (HerbrandT t s) where
   type Constraint (HerbrandT t s)  = Either (Unify t) (Constraint s)
-  type Label      (HerbrandT t s)  = (HState t, Label s)
+  type Label      (HerbrandT t s)  = (HState t (HerbrandT t s), Label s)
   add (Left  c)  = addH c
   add (Right c)  = lift $ add c
   mark           = do l <- get
diff --git a/Control/CP/Herbrand/Prolog.hs b/Control/CP/Herbrand/Prolog.hs
new file mode 100644
--- /dev/null
+++ b/Control/CP/Herbrand/Prolog.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Control.CP.Herbrand.Prolog 
+ ( Prolog
+ , module Control.CP.Herbrand.PrologTerm
+ , PConstraint (..) 
+ ) where 
+
+import Control.Monad (zipWithM)
+
+import Control.CP.Solver
+import Control.CP.Herbrand.Herbrand
+import Control.CP.Herbrand.PrologTerm
+
+-- Prolog Solver
+
+newtype Prolog a  = Prolog { runProlog :: Herbrand PrologTerm a }
+  deriving Monad
+
+instance Solver Prolog where
+  type Constraint Prolog  = PConstraint 
+  type Label      Prolog  = Label (Herbrand PrologTerm)
+  add     = addProlog
+  mark    = Prolog $ mark
+  goto    = Prolog . goto
+  run     = run . runProlog
+
+instance Term Prolog PrologTerm where
+  newvar  = Prolog $ newvar
+
+data PConstraint = PrologTerm := PrologTerm
+                 | NotFunctor PrologTerm String 
+                 | PrologTerm :/= PrologTerm
+
+addProlog :: PConstraint -> Prolog Bool
+addProlog (x := y)          = Prolog (unify x y)
+addProlog (x :/= y)          = Prolog (diff x y)
+addProlog (NotFunctor x f)  = Prolog (notFunctor x f)
+
+notFunctor :: PrologTerm -> String -> Herbrand PrologTerm Bool
+notFunctor x f  = do t <- shallow_normalize x
+                     case t of
+                       PVar _    ->
+                         registerAction t (notFunctor t f) >> success
+                       PTerm g _ ->
+                         if g == f then failure
+                                   else success
+
+diff :: PrologTerm -> PrologTerm -> Herbrand PrologTerm Bool
+diff x y  =
+  do x' <- shallow_normalize x
+     y' <- shallow_normalize y
+     b <- diff' x' y'
+     case b of
+       DYes        -> success
+       DNo         -> failure
+       DMaybe vars -> mapM (\v -> registerAction v (diff x y)) vars >> success
+ 
+
+  where diff' x@(PVar v1) (PVar v2)  =
+          if v1 == v2 then return $ DNo
+                      else return $ DMaybe [x]
+        diff' x@(PVar _) (PTerm _ _) =
+          return $ DMaybe [x]
+        diff' (PTerm _ _) y@(PVar _) =
+          return $ DMaybe [y]
+        diff' (PTerm f xs) (PTerm g ys) 
+          | x /= y                  = return $ DYes
+          | length xs /= length ys  = return $ DYes        
+          | otherwise               =
+              do xs' <- mapM shallow_normalize xs
+                 ys' <- mapM shallow_normalize ys
+                 bs  <- zipWithM diff' xs' ys'
+                 return $ foldr dand DYes bs
+                            
+data DiffBool  = DYes | DNo | DMaybe [PrologTerm]
+
+dand DNo         _          = DNo
+dand _          DNo         = DNo
+dand (DMaybe x) (DMaybe y)  = DMaybe (x ++ y)
+dand DYes       x           = x
+dand x          DYes        = x
+
diff --git a/Control/CP/Herbrand/PrologTerm.hs b/Control/CP/Herbrand/PrologTerm.hs
--- a/Control/CP/Herbrand/PrologTerm.hs
+++ b/Control/CP/Herbrand/PrologTerm.hs
@@ -1,6 +1,12 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
 module Control.CP.Herbrand.PrologTerm  where 
 
 import Data.List (intersperse)
+
 import Control.CP.Herbrand.Herbrand
 
 data PrologTerm = PTerm String [PrologTerm] | PVar VarId
@@ -26,4 +32,3 @@
 instance Show PrologTerm where
   show (PVar v)        = 'V' : show v
   show (PTerm f args)  = f ++ "(" ++ (concat $ intersperse "," $ map show args) ++ ")"
-
diff --git a/Control/CP/Main.hs b/Control/CP/Main.hs
deleted file mode 100644
--- a/Control/CP/Main.hs
+++ /dev/null
@@ -1,90 +0,0 @@
-{- 
- - 	Monadic Constraint Programming
- - 	http://www.cs.kuleuven.be/~toms/Haskell/
- - 	Tom Schrijvers
- -}
-module Control.CP.Main where
-
-import Control.CP.ComposableTransformers
-import Control.CP.FD
-import Control.CP.FDSugar
-import List (tails)
-import Control.CP.SearchTree hiding (label)
-import System (getArgs)
-
---------------------------------------------------------------------------------
--- MAIN FUNCTIONS
---------------------------------------------------------------------------------
-
-main = main1
-
-
-main1 = getArgs >>= print . solve dfs it . nqueens . read . head
-main2 = getArgs >>= print . solve dfs (nb 100 :- db  25 :- bb newBound)  . nqueens . read . head
-
-main3 = getArgs >>= print . solve dfs (db 9) . nqueens . read . head
-
-main4 = do (n1:_) <- getArgs 
-           let n = read n1
-           loop 1 n
-  where loop i n
-          | i > n     = return ()
-          | otherwise =
-              do -- print . (\(i,l) -> (i,not $ Prelude.null l)) . solve dfs (it :- fs :- ra 13 :- ld l) . nqueens $ i
-                 print . (\(i,l) -> (i, {- not $ Prelude.null-}  l)) . restart dfs (map db [3..10]) . nqueens $ i
-                 -- print . (\(i,l) -> (i, {- not $ Prelude.null-}  l)) . restartOpt dfs (replicate 10 fs) . nqueens $ i
-                 loop (i+1) n
-
-main5 = getArgs >>= loop 1 . read . head
-  where loop i n
-          | i > n     = return ()
-          | otherwise =
-              do print . (\(i,l) -> (i,minimum l)) . solve dfs (ld 5 :- bb newBoundBis) . gmodel $ i
-                 loop (i+1) n
-
---------------------------------------------------------------------------------
--- PATH MODEL
---------------------------------------------------------------------------------
-
-gmodel n = NewVar $ \_ -> path 1 n 0
-
-path :: Int -> Int -> Int -> Tree FD Int
-path x y d = if x == y 
-               then Return d
-               else disj [ Label (fd_objective >>= \o -> return (o @> (d+d' - 1) /\ (path z y (d+d')))) 
-                         | (z,d') <- edge x
-                         ]
-
-edge i | i < 20     = [ (i+1,4), (i+2,1) ]
-       | otherwise  = []
-
---------------------------------------------------------------------------------
--- N QUEENS MODEL
---------------------------------------------------------------------------------
-
-nqueens n = 
-  exist n $ \queens -> queens `allin` (1,n) /\ 
-                       alldifferent queens  /\ 
-                       diagonals queens     /\
-                       -- enumerate ({- middleout -} endsout queens) /\
-                       -- enumerate (middleout queens) /\
-                       enumerate (queens) /\
-		       assignments queens
-
-allin queens range  =  
-  conj [q `in_domain` range 
-       | q <- queens 
-       ] 
-
-alldifferent :: [ FD_Term ] -> Tree FD ()
-alldifferent queens =
-  conj [ qi @\= qj 
-       | qi:qjs <- tails queens 
-       , qj <- qjs 
-       ]
- 
-diagonals queens = 
-  conj [ qi @\== (qj @+ d) /\ qj @\== (qi @+ d) 
-       | qi:qjs <- tails queens 
-       , (qj,d) <- zip qjs [1..] 
-       ]
diff --git a/Control/CP/SearchTree.hs b/Control/CP/SearchTree.hs
--- a/Control/CP/SearchTree.hs
+++ b/Control/CP/SearchTree.hs
@@ -123,27 +123,42 @@
  -}
 
 -------------------------------------------------------------------------------
+----------------------------------- Monad Subclass ----------------------------
+-------------------------------------------------------------------------------
+
+infixl 2 \/
+
+class (Monad m, Solver (TreeSolver m)) => MonadTree m where
+  type TreeSolver m :: * -> *
+  addTo  :: Constraint (TreeSolver m) -> m a -> m a
+  false  :: m a
+  (\/)   :: m a -> m a -> m a
+  exists :: Term (TreeSolver m) t => (t -> m a) -> m a
+  label  :: (TreeSolver m) (m a) -> m a
+
+instance Solver solver => MonadTree (Tree solver) where
+  type TreeSolver (Tree solver)  = solver
+  addTo   =  Add
+  false   =  Fail
+  (\/)    =  Try
+  exists  =  NewVar
+  label   =  Label
+
+-------------------------------------------------------------------------------
 ----------------------------------- Sugar -------------------------------------
 -------------------------------------------------------------------------------
  
 infixr 3 /\
-(/\) :: Solver s => Tree s a -> Tree s b -> Tree s b
+(/\) :: MonadTree tree => tree a -> tree b -> tree b
 (/\) = (>>)
  
-infixl 2 \/
-(\/) :: Solver s => Tree s a -> Tree s a -> Tree s a
-(\/) = Try
-
-false :: Tree s a
-false = Fail
- 
-true :: Tree s ()
-true = Return ()
+true :: MonadTree tree  => tree ()
+true = return ()
 
-disj :: Solver s => [Tree s a] -> Tree s a
+disj :: MonadTree tree => [tree a] -> tree a
 disj = foldr (\/) false
 
-conj :: Solver s => [Tree s ()] -> Tree s ()
+conj :: MonadTree tree => [tree ()] -> tree ()
 conj = foldr (/\) true
 
 disj2 :: Solver s => [Tree s a] -> Tree s a
@@ -154,10 +169,7 @@
                                     in  (a:cs,bs)
                  in  Try (disj2 xs) (disj2 ys)
  
-exists :: Term s t => (t -> Tree s a) -> Tree s a
-exists f = NewVar f
-
-exist :: (Solver s, Term s t) => Int -> ([t] -> Tree s a) -> Tree s a
+exist :: (MonadTree tree, Term (TreeSolver tree) t) => Int -> ([t] -> tree a) -> tree a
 exist n ftree = f n []
          where f 0 acc  = ftree acc
                f n acc  = exists $ \v -> f (n-1) (v:acc)
@@ -165,11 +177,8 @@
 forall :: (Solver s, Term s t)  => [t] -> (t -> Tree s ()) -> Tree s ()
 forall list ftree = conj $ map ftree list
  
-label :: Solver s => s (Tree s a) -> Tree s a
-label = Label
-
-prim :: Solver s => (s a) -> Tree s a
-prim action = Label (action >>= return . return)
+prim :: MonadTree tree => TreeSolver tree a -> tree a
+prim action = label (action >>= return . return)
 
-add :: Solver s => Constraint s -> Tree s ()
-add c = Add c true
+add :: MonadTree tree => Constraint (TreeSolver tree) -> tree ()
+add c = c `addTo` true
diff --git a/Control/CP/Solver.hs b/Control/CP/Solver.hs
--- a/Control/CP/Solver.hs
+++ b/Control/CP/Solver.hs
@@ -8,23 +8,37 @@
  -}
 module Control.CP.Solver where 
 
+import Control.Monad.Writer
+import Data.Monoid
+
 class Monad solver => Solver solver where
-	-- the constraints
+	-- | the constraints
 	type Constraint solver 	:: *
- 	-- the labels
+ 	-- | the labels
 	type Label solver	:: *
-	-- add a constraint to the current state, and
-	-- return whethe the resulting state is consistent
+	-- | add a constraint to the current state, and
+	--   return whethe the resulting state is consistent
 	add		:: Constraint solver -> solver Bool
-	-- run a computation
+	-- | run a computation
 	run		:: solver a -> a
-	-- mark the current state, and return its label
+	-- | mark the current state, and return its label
 	mark		:: solver (Label solver)
-	-- go to the state with given label
+	-- | go to the state with given label
 	goto		:: Label solver -> solver ()
 
 class Solver solver => Term solver term where
-	-- produce a fresh constraint variable
+	-- | produce a fresh constraint variable
 	newvar 	:: solver term
   
+-- | WriterT decoration of a solver
+--   useful for producing statistics during solving
+instance (Monoid w, Solver s) => Solver (WriterT w s) where
+  type Constraint (WriterT w s)  = Constraint s
+  type Label (WriterT w s)       = Label s
+  add  = lift . add
+  run  = fst . run . runWriterT
+  mark = lift mark
+  goto = lift . goto 
 
+instance (Monoid w, Term s t) => Term (WriterT w s) t where
+  newvar  = lift newvar
diff --git a/monadiccp.cabal b/monadiccp.cabal
--- a/monadiccp.cabal
+++ b/monadiccp.cabal
@@ -1,5 +1,5 @@
 Name:                monadiccp
-Version:             0.4.1
+Version:             0.5
 Description:         Monadic Constraint Programming framework
 License:             BSD3
 License-file:        LICENSE
@@ -7,8 +7,9 @@
 Maintainer:          tom.schrijvers@cs.kuleuven.be
 Build-Depends:       base, containers, mtl, haskell98, random
 Build-Type:          Simple
-Exposed-modules:     Control.CP.ComposableTransformers  Control.CP.PriorityQueue  Control.CP.Queue  Control.CP.Solver  Control.CP.SearchTree  Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.HerbrandT
+Exposed-modules:     Control.CP.ComposableTransformers  Control.CP.PriorityQueue  Control.CP.Queue  Control.CP.Solver  Control.CP.SearchTree  Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.Prolog Control.CP.Herbrand.HerbrandT
 ghc-options:         
 Category:            control
-Synopsis:	     Package for Constraint Programming
+Synopsis:	     Constraint Programming
 Homepage:            http://www.cs.kuleuven.be/~toms/Haskell/
+bug-reports:         http://trac.haskell.org/monadiccp/