diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,19 @@
+Copyright (c) 2014, Stephen Diehl
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to
+deal in the Software without restriction, including without limitation the
+rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
+sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
+IN THE SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/picologic.cabal b/picologic.cabal
new file mode 100644
--- /dev/null
+++ b/picologic.cabal
@@ -0,0 +1,60 @@
+name:                picologic
+version:             0.1
+synopsis:            Utilities for symbolic predicate logic expressions
+homepage:            https://github.com/sdiehl/picologic
+license:             MIT
+license-file:        LICENSE
+author:              Stephen Diehl
+maintainer:          stephen.m.diehl@gmail.com
+copyright:           2014 Stephen Diehl
+category:            Logic
+build-type:          Simple
+cabal-version:       >=1.10
+tested-with:         GHC == 7.6.3
+Bug-Reports:         https://github.com/sdiehl/picologic/issues
+
+description:
+  `picologic` provides symbolic logic expressions that can be integrated with the `picosat` solver.
+Source-Repository head
+    type: git
+    location: git@github.com:sdiehl/picologic.git
+
+Flag shell
+  description: Build the interactive shell
+  default:     False
+
+library
+  exposed-modules:     
+    Picologic,
+    Picologic.Solver,
+    Picologic.AST,
+    Picologic.Parser
+  hs-source-dirs:      src
+  other-extensions:    DeriveDataTypeable, BangPatterns
+  build-depends:       
+    base        >= 4.6 && <4.7,
+    picosat     >= 0.1 && <0.2,
+    containers  >= 0.5 && <0.6,
+    mtl         >= 2.1 && <2.2,
+    pretty      >= 1.1 && <1.2,
+    parsec      >= 3.1 && <3.2
+  default-language:    Haskell2010
+
+executable picologic
+  main-is:     Picologic/Main.hs
+  if flag(shell)
+    hs-source-dirs:      src
+    other-modules: Picologic.Repl
+    other-extensions:    DeriveDataTypeable, BangPatterns
+    build-depends:       
+      base        >= 4.6 && <4.7,
+      picosat     >= 0.1 && <0.2,
+      containers  >= 0.5 && <0.6,
+      mtl         >= 2.1 && <2.2,
+      pretty      >= 1.1 && <1.2,
+      parsec      >= 3.1 && <3.2,
+      process     >= 1.1 && <1.2,
+      haskeline   >= 0.7 && <0.8
+    default-language:    Haskell2010
+  else
+    buildable: False
diff --git a/src/Picologic.hs b/src/Picologic.hs
new file mode 100644
--- /dev/null
+++ b/src/Picologic.hs
@@ -0,0 +1,41 @@
+{- |
+
+Example usage:
+
+@
+import Picologic
+p, q, r :: Expr
+p = readExpr \"~(A | B)\"
+q = readExpr \"(A | ~B | C) & (B | D | E) & (D | F)\"
+r = readExpr \"(φ \<-\> ψ)\"
+@
+
+The expression can be pretty printed using logical symbols:
+
+>>> ppExprU p
+¬(A ∨ B)
+>>> ppExprU q
+((((A ∨ ¬B) ∨ C) ∧ ((B ∨ D) ∨ E)) ∧ (D ∨ F))
+>>> ppExprU (cnf r)
+((φ ∧ (φ ∨ ¬ψ)) ∧ ((ψ ∨ ¬φ) ∧ ψ))
+
+To run the expression against the SAT solver run:
+
+>>> solveProp p >>= putStrLn . ppSolutions
+~A ~B
+~A B
+A ~B
+
+-}
+
+module Picologic (
+  module Picologic.AST,
+  module Picologic.Parser,
+  module Picologic.Solver,
+  module Picologic.Pretty,
+) where
+
+import Picologic.AST
+import Picologic.Parser
+import Picologic.Solver
+import Picologic.Pretty
diff --git a/src/Picologic/AST.hs b/src/Picologic/AST.hs
new file mode 100644
--- /dev/null
+++ b/src/Picologic/AST.hs
@@ -0,0 +1,106 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
+module Picologic.AST (
+  Expr(..),
+  Ident(..),
+  Solutions(..),
+  Ctx,
+
+  variables,
+  eval,
+
+  cnf,
+  nnf,
+  simp,
+) where
+
+import Data.List
+import Data.Data
+import Data.Maybe
+import qualified Data.Map as M
+
+
+newtype Ident = Ident String
+  deriving (Eq, Ord, Show, Data, Typeable)
+
+newtype Solutions = Solutions [[Expr]]
+
+type Ctx = M.Map Ident Bool
+
+data Expr
+  = Var       Ident      -- ^ Variable
+  | Neg       Expr       -- ^ Logical negation
+  | Conj      Expr Expr  -- ^ Logical conjunction
+  | Disj      Expr Expr  -- ^ Logical disjunction
+  | Iff       Expr Expr  -- ^ Logical biconditional
+  | Implies   Expr Expr  -- ^ Material implication
+  deriving (Eq, Ord, Show, Data, Typeable)
+
+-- | Evaluate expression.
+eval :: Ctx -> Expr -> Bool
+eval vs (Var v)           = fromMaybe False (M.lookup v vs)
+eval vs (Neg expr)        = not $ eval vs expr
+eval vs (Conj e1 e2)      = eval vs e1 && eval vs e2
+eval vs (Disj   e1 e2)    = eval vs e1 || eval vs e2
+eval vs (Implies   e1 e2) = not (eval vs e1) || eval vs e2
+eval vs (Iff e1 e2)       = eval vs e1 == eval vs e2
+
+-- | Variables in expression
+variables :: Expr -> [Ident]
+variables expr = map head . group . sort $ go expr []
+  where
+    go (Var v)         !vs = v : vs
+    go (Neg e)         !vs = go e vs
+    go (Conj e1 e2)    !vs = go e1 vs ++ go e2 vs
+    go (Disj e1 e2)    !vs = go e1 vs ++ go e2 vs
+    go (Iff e1 e2)     !vs = go e1 vs ++ go e2 vs
+    go (Implies e1 e2) !vs = go e1 vs ++ go e2 vs
+
+-- | Negation normal form.
+nnf :: Expr -> Expr
+nnf ex = case ex of
+  e@(Var _)             -> e
+  e@(Neg (Var _))       -> e
+  Neg (Neg e)           -> e
+
+  Conj e1 e2            -> nnf e1 `Conj` nnf e2
+  Neg (Conj e1 e2)      -> nnf $ Neg e1 `Conj` Neg e2
+
+  Disj e1 e2            -> nnf e1 `Disj` nnf e2
+  Neg (Disj e1 e2)      -> nnf $ Neg e1 `Conj` Neg e2
+
+  Implies e1 e2         -> nnf $ Neg e1 `Disj` e2
+  Neg (Implies e1 e2)   -> nnf $ e1 `Conj` Neg e2
+
+  Iff e1 e2             -> let a = e1 `Conj` e2
+                               b = Neg e1 `Conj` Neg e2
+                               in nnf $ a `Disj` b
+
+  Neg (Iff e1 e2)       -> let a = e1 `Disj` e2
+                               b = Neg e1 `Disj` Neg e2
+                               in nnf $ a `Conj` b
+
+-- | Conjunctive normal form.
+cnf :: Expr -> Expr
+cnf = simp . cnf' . nnf
+  where
+    cnf' :: Expr -> Expr
+    cnf' (Conj e1 e2) = cnf' e1 `Conj` cnf' e2
+    cnf' (Disj e1 e2) = cnf' e1 `dist` cnf' e2
+    cnf' e            = e
+
+    dist :: Expr -> Expr -> Expr
+    dist (Conj e11 e12) e2 = (e11 `dist` e2) `Conj` (e12 `dist` e2)
+    dist e1 (Conj e21 e22) = (e1 `dist` e21) `Conj` (e1 `dist` e22)
+    dist e1 e2             = e1 `Disj` e2
+
+-- | Remove tautologies.
+simp :: Expr -> Expr
+simp ex = case ex of
+  Disj e1 (Neg e2) | e1 == e2 -> e1
+  Disj (Neg e1) e2 | e1 == e2 -> e1
+  Disj e1 e2 -> Disj (simp e1) (simp e2)
+  Conj e1 e2       | e1 == e2 -> e1
+                   | otherwise -> Conj (simp e1) (simp e2)
+  e -> e
diff --git a/src/Picologic/Main.hs b/src/Picologic/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Picologic/Main.hs
@@ -0,0 +1,14 @@
+module Main where
+
+import Picologic.Repl
+import Control.Monad
+import System.Environment
+
+main :: IO ()
+main = do
+  args <- getArgs
+  case args of
+    []      -> void $ runRepl repl
+    ["-"]   -> stdin
+    [fname] -> void $ runRepl (file fname >> repl)
+    _ -> putStrLn "invalid arguments"
diff --git a/src/Picologic/Parser.hs b/src/Picologic/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Picologic/Parser.hs
@@ -0,0 +1,53 @@
+module Picologic.Parser (
+  parseFile,
+  parseExpr,
+  readExpr,
+) where
+
+import Text.Parsec hiding (State)
+import qualified Text.Parsec.Expr as Ex
+
+import Picologic.AST
+import Picologic.Lexer
+
+infixOp :: String -> (a -> a -> a) -> Ex.Assoc -> Op a
+infixOp x f = Ex.Infix (reservedOp x >> return f)
+
+prefixOp :: String -> (a -> a) -> Op a
+prefixOp x f = Ex.Prefix (reservedOp x >> return f)
+
+operators :: [[Op Expr]]
+operators = [
+    [ prefixOp "~" Neg ],
+    [
+      infixOp "&" Conj Ex.AssocLeft,
+      infixOp "|" Disj Ex.AssocLeft,
+      infixOp "->" Implies Ex.AssocLeft,
+      infixOp "<->" Iff Ex.AssocLeft
+    ]
+  ]
+
+var :: Parser Expr
+var = do
+  x <- identifier
+  return $ Var (Ident x)
+
+cexpr :: Parser Expr
+cexpr =  Ex.buildExpressionParser operators cfactor
+
+cfactor :: Parser Expr
+cfactor =  var
+       <|> parens cexpr
+
+parseExpr :: String -> Either ParseError Expr
+parseExpr = parse (contents cexpr) "<stdin>"
+
+readExpr :: String -> Expr
+readExpr s = case parseExpr s of
+  Left err -> error (show err)
+  Right expr -> expr
+
+parseFile :: FilePath -> IO (Either ParseError Expr)
+parseFile fname = do
+  fcontents <- readFile fname
+  return $ parse (contents cexpr) fname fcontents
diff --git a/src/Picologic/Repl.hs b/src/Picologic/Repl.hs
new file mode 100644
--- /dev/null
+++ b/src/Picologic/Repl.hs
@@ -0,0 +1,147 @@
+module Picologic.Repl (
+  repl,
+  stdin,
+  file,
+  runRepl,
+) where
+
+import Picologic.AST
+import Picologic.Parser
+import Picologic.Solver
+import Picologic.Pretty
+
+import Text.PrettyPrint
+
+import Control.Monad.State
+
+import Data.List (isPrefixOf)
+import System.Console.Haskeline
+
+-------------------------------------------------------------------------------
+-- REPL
+-------------------------------------------------------------------------------
+
+type Repl = StateT IState (InputT IO)
+
+data IState = IState
+  { _module :: Maybe Expr
+  , _curFile :: Maybe FilePath
+  }
+
+initState :: IState
+initState = IState Nothing Nothing
+
+preamble :: Repl ()
+preamble = liftIO $ do
+  putStrLn "Picologic 0.1"
+  putStrLn "Type :help for help"
+
+runRepl :: Repl a -> IO IState
+runRepl f = runInputT defaultSettings (execStateT (preamble >> f) initState)
+
+-------------------------------------------------------------------------------
+-- Commands
+-------------------------------------------------------------------------------
+
+load :: String -> Repl ()
+load arg = do
+  liftIO $ putStrLn $ "Loading " ++ arg
+  file arg
+  modify $ \s -> s { _curFile = Just arg }
+
+reload :: Repl ()
+reload = do
+  fname <- gets _curFile
+  case fname of
+    Just fname' -> handleCommand "load" [fname']
+    Nothing -> liftIO $ putStrLn "No such file"
+
+run :: Repl ()
+run = do
+  mod <- gets _module
+  case mod of
+    Nothing -> liftIO $ putStrLn "No expression."
+    Just ex -> liftIO $ do
+      sols <- solveProp ex
+      putStrLn "Solutions:"
+      putStrLn (ppSolutions sols)
+
+clauses :: Repl ()
+clauses = do
+  env <- gets _module
+  case env of
+    Just ex -> liftIO $ print (clausesExpr ex)
+    Nothing -> liftIO $ putStrLn "No file loaded."
+
+help :: Repl ()
+help = liftIO $ do
+  putStrLn ":clauses      Show the SAT solver clauses"
+  putStrLn ":load <file>  Load a program from file"
+
+-------------------------------------------------------------------------------
+-- Test
+-------------------------------------------------------------------------------
+
+-- evaluate a module
+modl :: FilePath -> Repl ()
+modl fname = do
+  mod <- liftIO $ parseFile fname
+  case mod of
+    Left  err -> liftIO $ print err
+    Right res ->
+      let ex = (simp . cnf $ res) in
+      modify $ \s -> s { _module = Just ex }
+
+-- evaluate an expression
+exec :: String -> Repl ()
+exec source = do
+  let mod = parseExpr source
+  case mod of
+    Left  err -> liftIO $ print err
+    Right res -> do
+      let ex = (simp . cnf $ res)
+      liftIO $ putStrLn (render $ ppExprU ex)
+      liftIO $ do
+        sols <- solveProp ex
+        putStrLn "Solutions:"
+        putStrLn (ppSolutions sols)
+      modify $ \s -> s { _module = Just ex }
+
+file :: FilePath -> Repl ()
+file fname = modl fname
+
+stdin :: IO ()
+stdin = do
+  contents <- getContents
+  case parseExpr contents of
+    Left err -> print err
+    Right ex -> do
+      sols <- solveProp ex
+      putStrLn (ppSolutions sols)
+
+handleCommand :: String -> [String] -> Repl ()
+handleCommand cmd args
+    | "ru"  `isPrefixOf` cmd = run
+    | "r"   `isPrefixOf` cmd = reload
+    | "cl"  `isPrefixOf` cmd = clauses
+    | "h"   `isPrefixOf` cmd = help
+    | length args == 0 = liftIO $ putStrLn "Not enough arguments"
+    | "l"  `isPrefixOf` cmd = load arg
+    | otherwise = liftIO $ putStrLn "Unknown command"
+  where
+    arg = head args
+
+repl :: Repl ()
+repl = do
+  minput <- lift $ getInputLine "Logic> "
+  case minput of
+    Nothing -> lift $ outputStrLn "Goodbye."
+
+    Just (':' : cmds) -> do
+      let (cmd:args) = words cmds
+      handleCommand cmd args
+      repl
+
+    Just input -> do
+      exec input
+      repl
diff --git a/src/Picologic/Solver.hs b/src/Picologic/Solver.hs
new file mode 100644
--- /dev/null
+++ b/src/Picologic/Solver.hs
@@ -0,0 +1,73 @@
+module Picologic.Solver (
+  solveProp,
+  clausesExpr,
+) where
+
+import Picologic.AST
+import Picosat
+
+import Data.List
+import Data.Map as M
+import Control.Monad.Writer
+
+data Clause
+  = CV Int       -- ^Clause variable ( a or -a )
+  | CL [Clause]  -- ^Set of clause under disjuntion
+
+instance Show Clause where
+  show (CV i) = show i
+  show (CL xs) = concat (intersperse " " (fmap show xs))
+
+-- | Yield the soutions for an expressions using the PicosSAT solver.
+solveProp :: Expr -> IO Solutions
+solveProp p = solveAll cs >>= return . Solutions . fmap (backSubst vs')
+  where
+    cs = fmap toInts $ execWriter $ clauses vs (cnf p)
+    vs  = M.fromList $ zip vars [1..]
+    vs' = M.fromList $ zip [1..] vars
+    vars = variables (cnf p)
+
+-- | Yield the integer clauses given to the SAT solver.
+clausesExpr :: Expr -> [[Int]]
+clausesExpr p = fmap toInts $ execWriter $ clauses vs (cnf p)
+  where
+    vs = M.fromList $ zip vars [1..]
+    vars = variables (cnf p)
+
+backSubst :: Map Int Ident -> Solution -> [Expr]
+backSubst env (Solution xs) = fmap go xs
+  where
+    go x | x >= 0 = Var (env M.! x)
+    go x | x < 0 = Neg (Var (env M.! (abs x)))
+backSubst _ Unsatisfiable = []
+backSubst _ Unknown = []
+
+toInts :: Clause -> [Int]
+toInts (CL xs) = fmap (\(CV n) -> n) xs
+
+neg :: Clause -> Clause
+neg (CV n) = CV (-n)
+neg (CL xs) = CL (fmap neg xs)
+
+combine :: Clause -> Clause -> Clause
+combine (CL x) (CL y) = CL (x++y)
+combine (CL x) y = combine (CL x) (CL [y])
+combine x (CL y) = combine (CL [x]) (CL y)
+combine x y = CL [x, y]
+
+clauses :: M.Map Ident Int -> Expr -> Writer [Clause] Clause
+clauses env ex = case ex of
+  Var v -> return $ CV (env M.! v)
+  Neg x -> do
+    cs <- clauses env x
+    return (neg cs)
+  Conj e1 e2 -> do
+    cs1 <- clauses env e1
+    cs2 <- clauses env e2
+    tell [combine cs1 cs2]
+    return (combine cs1 cs2)
+  Disj e1 e2 -> do
+    cs1 <- clauses env e1
+    cs2 <- clauses env e2
+    tell [combine cs1 cs2]
+    return (combine cs1 cs2)