diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2014, Stephen Diehl
+Copyright (c) 2014-2016, 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
diff --git a/picologic.cabal b/picologic.cabal
--- a/picologic.cabal
+++ b/picologic.cabal
@@ -1,5 +1,5 @@
 name:                picologic
-version:             0.1.2
+version:             0.2.0
 synopsis:            Utilities for symbolic predicate logic expressions
 homepage:            https://github.com/sdiehl/picologic
 license:             MIT
@@ -36,12 +36,12 @@
   hs-source-dirs:      src
   other-extensions:    DeriveDataTypeable, BangPatterns
   build-depends:       
-    base >= 2   && <5,
-    picosat,
-    containers,
-    mtl,
-    pretty,
-    parsec
+    base        >= 4.6 && <4.10,
+    picosat     >= 0.1 && <0.2,
+    containers  >= 0.5 && <0.6,
+    mtl         >= 2.1 && <2.4,
+    pretty      >= 1.1 && <1.2,
+    parsec      >= 3.1 && <3.2
   default-language:    Haskell2010
 
 executable picologic
@@ -54,7 +54,7 @@
       base        >= 2   && <5,
       picosat     >= 0.1 && <0.2,
       containers  >= 0.5 && <0.6,
-      mtl         >= 2.1 && <2.2,
+      mtl         >= 2.1 && <2.4,
       pretty      >= 1.1 && <1.2,
       parsec      >= 3.1 && <3.2,
       process     >= 1.1 && <1.2,
diff --git a/src/Picologic/AST.hs b/src/Picologic/AST.hs
--- a/src/Picologic/AST.hs
+++ b/src/Picologic/AST.hs
@@ -13,6 +13,10 @@
   cnf,
   nnf,
   simp,
+  isConst,
+  propConst,
+  subst,
+  partEval
 ) where
 
 import Data.List
@@ -34,6 +38,8 @@
   | Disj      Expr Expr  -- ^ Logical disjunction
   | Iff       Expr Expr  -- ^ Logical biconditional
   | Implies   Expr Expr  -- ^ Material implication
+  | Top                  -- ^ Constant true
+  | Bottom               -- ^ Constant false
   deriving (Eq, Ord, Data, Typeable)
 
 -- | Evaluate expression.
@@ -41,9 +47,11 @@
 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 (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
+eval vs (Top)             = True
+eval vs (Bottom)          = False
 
 -- | Variables in expression
 variables :: Expr -> [Ident]
@@ -55,31 +63,28 @@
     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
+    go (Top)           !vs = vs
+    go (Bottom)        !vs = vs
 
 -- | Negation normal form.
 -- (May result in exponential growth)
 nnf :: Expr -> Expr
-nnf ex = case ex of
-  e@(Var _)             -> e
-  e@(Neg (Var _))       -> e
-  Neg (Neg e)           -> nnf e
-
-  Conj e1 e2            -> nnf e1 `Conj` nnf e2
-  Neg (Conj e1 e2)      -> nnf $ Neg e1 `Disj` 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 `Disj` Neg e2
-                               b = Neg e1 `Disj` e2
-                               in nnf $ a `Conj` b
+nnf = transformDown nnf1 . propConst
 
-  Neg (Iff e1 e2)       -> let a = e1 `Disj` e2
-                               b = Neg e1 `Disj` Neg e2
-                               in nnf $ a `Conj` b
+nnf1 :: Expr -> Expr
+nnf1 ex = case ex of
+  Neg (Neg e) -> nnf1 e
+  Neg (Conj e1 e2) -> Neg e1 `Disj` Neg e2
+  Neg (Disj e1 e2) -> Neg e1 `Conj` Neg e2
+  Implies e1 e2 -> Neg e1 `Disj` e2
+  Neg (Implies e1 e2) -> e1 `Conj` Neg e2
+  Iff e1 e2 -> let a = e1 `Disj` Neg e2
+                   b = Neg e1 `Disj` e2
+               in a `Conj` b
+  Neg (Iff e1 e2) -> let a = e1 `Disj` e2
+                         b = Neg e1 `Disj` Neg e2
+                     in a `Conj` b
+  e -> e
 
 -- | Conjunctive normal form.
 -- (May result in exponential growth)
@@ -98,10 +103,96 @@
 
 -- | Remove tautologies.
 simp :: Expr -> Expr
-simp ex = case ex of
-  -- Disj e1 (Neg e2) | e1 == e2 -> True
-  -- Disj (Neg e1) e2 | e1 == e2 -> True
-  Disj e1 e2 -> Disj (simp e1) (simp e2)
+simp = transformUp (propConst1 . simp1)
+
+simp1 :: Expr -> Expr
+simp1 ex = case ex of
+  Disj e1 (Neg e2) | e1 == e2 -> Top
+  Disj (Neg e1) e2 | e1 == e2 -> Top
   Conj e1 e2       | e1 == e2 -> e1
-                   | otherwise -> Conj (simp e1) (simp e2)
   e -> e
+
+-- | Test if expression is constant.
+isConst :: Expr -> Bool
+isConst Top = True
+isConst Bottom = True
+isConst e = False
+
+-- | Transform expression up from the bottom.
+transformUp :: (Expr -> Expr) -> Expr -> Expr
+-- TODO: This could probably be done with Data.Data, but it's outside my capabilities for now. 
+transformUp f ex = case ex of
+  Neg e -> f $ Neg (transformUp f e)
+  Conj e1 e2 -> f $ Conj (transformUp f e1) (transformUp f e2)
+  Disj e1 e2 -> f $ Disj (transformUp f e1) (transformUp f e2)
+  Iff e1 e2 -> f $ Iff (transformUp f e1) (transformUp f e2)
+  Implies e1 e2 -> f $ Implies (transformUp f e1) (transformUp f e2)
+  e -> f e
+
+-- | Transform expression down from the top.
+transformDown :: (Expr -> Expr) -> Expr -> Expr
+-- TODO: This could probably be done with Data.Data, but it's outside my capabilities for now. 
+transformDown f ex = case f ex of
+  Neg e -> Neg (transformDown f e)
+  Conj e1 e2 -> Conj (transformDown f e1) (transformDown f e2)
+  Disj e1 e2 -> Disj (transformDown f e1) (transformDown f e2)
+  Iff e1 e2 -> Iff (transformDown f e1) (transformDown f e2)
+  Implies e1 e2 -> Implies (transformDown f e1) (transformDown f e2)
+  e -> e
+
+-- | Convert expression to list of all subexpressions.
+toList :: Expr -> [Expr]
+-- TODO: This could probably be done with Data.Data, but it's outside my capabilities for now.
+toList ex = ex : case ex of
+  Var ident -> []
+  Neg e -> toList e
+  Conj e1 e2 -> toList e1 ++ toList e2
+  Disj e1 e2 -> toList e1 ++ toList e2
+  Iff e1 e2 -> toList e1 ++ toList e2
+  Implies e1 e2 -> toList e1 ++ toList e2
+  Top -> []
+  Bottom -> []
+
+-- | Propagate constants (to simplify expression).
+propConst :: Expr -> Expr
+propConst = transformUp propConst1
+
+propConst1 :: Expr -> Expr
+propConst1 ex = case ex of
+  Neg (Neg e) -> e
+  Neg Top -> Bottom
+  Neg Bottom -> Top
+  Conj Top e2 -> e2
+  Conj Bottom e2 -> Bottom
+  Conj e1 Top -> e1
+  Conj e1 Bottom -> Bottom
+  Disj Top e2 -> Top
+  Disj Bottom e2 -> e2
+  Disj e1 Top -> Top
+  Disj e1 Bottom -> e1
+  Iff Top Bottom -> Bottom
+  Iff Bottom Top -> Bottom
+  Iff Bottom Bottom -> Top
+  Iff Top e2 -> e2
+  Iff Bottom e2 -> Neg e2
+  Iff e1 Top -> e1
+  Iff e1 Bottom -> Neg e1
+  Implies Top e2 -> e2
+  Implies Bottom e2 -> Top
+  Implies e1 Top -> Top
+  Implies e1 Bottom -> Neg e1
+  e -> e
+
+-- | Substitute expressions for variables. This doesn't resolve any potential variable name conflicts.
+subst :: M.Map Ident Expr -> Expr -> Expr
+subst vs = transformUp (propConst1 . subst1 vs)
+  where
+    subst1 vs ex = case ex of
+      Var ident -> M.findWithDefault ex ident vs
+      e -> e
+
+-- | Partially evaluate expression.
+partEval :: Ctx -> Expr -> Expr
+partEval vs = subst (M.map constants vs)
+  where constants True = Top
+        constants False = Bottom
diff --git a/src/Picologic/Lexer.hs b/src/Picologic/Lexer.hs
--- a/src/Picologic/Lexer.hs
+++ b/src/Picologic/Lexer.hs
@@ -34,7 +34,7 @@
   ]
 
 reservedNames :: [String]
-reservedNames = []
+reservedNames = ["1","0"]
 
 lexerStyle :: Language
 lexerStyle = haskellStyle
diff --git a/src/Picologic/Parser.hs b/src/Picologic/Parser.hs
--- a/src/Picologic/Parser.hs
+++ b/src/Picologic/Parser.hs
@@ -32,11 +32,16 @@
   x <- identifier
   return $ Var (Ident x)
 
+constant :: Parser Expr
+constant = (reserved "1" >> return Top)
+       <|> (reserved "0" >> return Bottom)
+
 cexpr :: Parser Expr
 cexpr =  Ex.buildExpressionParser operators cfactor
 
 cfactor :: Parser Expr
-cfactor =  var
+cfactor =  constant
+       <|> var
        <|> parens cexpr
 
 parseExpr :: String -> Either ParseError Expr
diff --git a/src/Picologic/Pretty.hs b/src/Picologic/Pretty.hs
--- a/src/Picologic/Pretty.hs
+++ b/src/Picologic/Pretty.hs
@@ -5,10 +5,11 @@
   ppSolutions,
 ) where
 
-import Picologic.AST (Expr(..), Ident(..), Solutions(..))
+import Data.List (intersperse, intercalate)
 import Text.PrettyPrint
-import Data.List (intersperse)
 
+import Picologic.AST (Expr(..), Ident(..), Solutions(..))
+
 -- | Pretty print with unicode symbols.
 ppExprU :: Expr -> Doc
 ppExprU ex = case ex of
@@ -18,6 +19,8 @@
   Disj a b      -> con '∨' a b
   Implies a b   -> con '→' a b
   Iff a b       -> con '↔' a b
+  Top           -> char '⊤'
+  Bottom        -> char '⊥'
   where con c a b =
           parens $ sep [ppExprU a, char c <+> ppExprU b]
 
@@ -30,6 +33,8 @@
   Disj e1 e2     ->  parens $ ppExprA e1 <+> char '|' <+> ppExprA e2
   Implies e1 e2  ->  parens $ ppExprA e1 <+> text "->" <+> ppExprA e2
   Iff e1 e2      ->  parens $ ppExprA e1 <+> text "<->" <+> ppExprA e2
+  Top            ->  char '1'
+  Bottom         ->  char '0'
 
 -- | Pretty print into S-Expressions
 ppExprLisp :: Expr -> Doc
@@ -39,6 +44,8 @@
   Disj a b            -> con "or" $ ors [a, b]
   Implies a b         -> con "==>" [a, b]
   Iff a b             -> con "==" $ iffs [a, b]
+  Top                 -> text "true"
+  Bottom              -> text "false"
   Neg (Var (Ident n)) -> text $ "-" ++ n
   Neg (Conj a b)      -> con "nand" $ ands [a, b]
   Neg (Disj a b)      -> con "nor" $ ors [a, b]
@@ -62,12 +69,14 @@
 iffs (x:xs) = x : iffs xs
 
 instance Show Expr where
-  show = show . ppExprLisp
-
+  show = show . ppExprA
 
 ppSolutions :: Solutions -> String
 ppSolutions (Solutions xs) =
-  concat (concat $ intersperse ["\n"] (fmap showExprs xs))
+  concat (intercalate ["\n"] (fmap showExprs xs))
+
+instance Show Solutions where
+  show (Solutions sols) = show sols
 
 showExprs :: [Expr] -> [String]
 showExprs xs = intersperse " " $ fmap (render . ppExprU) xs
diff --git a/src/Picologic/Solver.hs b/src/Picologic/Solver.hs
--- a/src/Picologic/Solver.hs
+++ b/src/Picologic/Solver.hs
@@ -2,7 +2,8 @@
   solveProp,
   solveCNF,
   solveOneCNF,
-  clausesExpr
+  clausesExpr,
+  addVarsToSolutions
 ) where
 
 import Picologic.AST
@@ -10,7 +11,9 @@
 import Picosat
 
 import Data.List
+import Data.Maybe(mapMaybe)
 import qualified Data.Map as M
+import qualified Data.Set as S
 import Control.Monad.Writer
 
 -- | Yield the solutions for an expression using the PicoSAT solver.
@@ -20,9 +23,14 @@
 -- | Yield the solutions for an expression using the PicoSAT
 -- solver. The Expression must be in CNF form already.
 solveCNF :: Expr -> IO Solutions
-solveCNF p = do
-  solutions <- solveAll ds
-  return $ Solutions $ fmap (backSubst vs') solutions
+solveCNF p = if isConst p
+             then
+               return $ if eval M.empty p
+                        then Solutions [[]]
+                        else Solutions []
+             else do
+                 solutions <- solveAll ds
+                 return $ Solutions $ mapMaybe (backSubst vs') solutions
   where
     cs = clausesFromCNF p
     ds = cnfToDimacs vs cs
@@ -32,10 +40,15 @@
 
 -- | Yield one single solution for an expression using the PicoSAT
 -- solver. The Expression must be in CNF form already.
-solveOneCNF :: Expr -> IO [Expr]
-solveOneCNF p = do
-  solution <- solve ds
-  return $ backSubst vs' solution
+solveOneCNF :: Expr -> IO (Maybe [Expr])
+solveOneCNF p = if isConst p
+                then
+                  return $ if eval M.empty p
+                           then Just []
+                           else Nothing
+                else do
+                  solution <- solve ds
+                  return $ backSubst vs' solution
   where
     cs = clausesFromCNF p
     ds = cnfToDimacs vs cs
@@ -44,13 +57,12 @@
     vars = variables p
 
 clausesFromCNF :: Expr -> [[Expr]]
-clausesFromCNF p =
-  [ [ case lit of
-         v@(Var name) -> v
-         v@(Neg (Var name)) -> v
-         x -> error $ "input not in CNF: \n" ++ show p
-    | lit <- ors [clause] ]
-  | clause <- ands [p]]
+clausesFromCNF p = [ [ case lit of
+                       v@(Var name) -> v
+                       v@(Neg (Var name)) -> v
+                       x -> error $ "input not in CNF: \n" ++ show p
+                     | lit <- ors [clause] ]
+                   | clause <- ands [p]]
 
 ands :: [Expr] -> [Expr]
 ands [] = []
@@ -63,7 +75,7 @@
 ors (x:xs) = x : ors xs
 
 cnfToDimacs :: M.Map Ident Int -> [[Expr]] -> [[Int]]
-cnfToDimacs vs cs = map (map encode) cs
+cnfToDimacs vs = map (map encode)
   where encode (Var ident)       = vs M.! ident
         encode (Neg (Var ident)) = negate $ vs M.! ident
   
@@ -77,11 +89,16 @@
     vars = variables p
     ds = cnfToDimacs vs cs
 
-backSubst :: M.Map Int Ident -> Solution -> [Expr]
-backSubst env (Solution xs) = fmap go xs
+backSubst :: M.Map Int Ident -> Solution -> Maybe [Expr]
+backSubst env (Solution xs) = Just $ 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 = []
+    go x | x < 0 = Neg (Var (env M.! abs x))
+backSubst _ Unsatisfiable = Nothing
+backSubst _ Unknown = Nothing
 
+addVarsToSolutions :: [Ident] -> Solutions -> Solutions
+addVarsToSolutions vars (Solutions sols) = Solutions $ concatMap addVarsToSolution sols
+  where
+    addVarsToSolution sol = map (sol ++) $ sequence  [ [Var v, Neg(Var v)] | v <- newVars $ head sols ]
+    newVars sol = vars \\ concatMap variables sol
diff --git a/src/Picologic/Tseitin.hs b/src/Picologic/Tseitin.hs
--- a/src/Picologic/Tseitin.hs
+++ b/src/Picologic/Tseitin.hs
@@ -33,12 +33,12 @@
   put $ succ n
   return $ Var $ Ident $ "ts*" ++ show n
 
-or xs = foldl1 Disj xs
-and xs = foldl1 Conj xs
+or = foldl1 Disj
+and = foldl1 Conj
 
 tseitinCNF :: Expr -> Expr
 tseitinCNF e =
-  let (var, clauses) = evalTS $ tseitin $ simplify e
+  let (var, clauses) = evalTS $ tseitin $ propConst e
   in and (var : clauses)
 
 neg (Neg x) = x
@@ -156,6 +156,10 @@
         or [a, c]]
   return c
 
+tseitin Top = return Top
+
+tseitin Bottom = return Bottom
+
 dropTseitinVarsInSolutions (Solutions xs) =
   Solutions $ map dropTseitinVars xs
 
@@ -171,12 +175,3 @@
 tseitinName ('t':'s':'*':_) = True
 tseitinName _               = False
 
-simplify :: Expr -> Expr
-simplify (Neg (Neg x)) = simplify x
-simplify v@(Var _) = v
-simplify (Neg a) = neg $ simplify a
-simplify (Conj a b) = Conj (simplify a) (simplify b)
-simplify (Disj a b) = Disj (simplify a) (simplify b)
-simplify (Implies a b) = Implies (simplify a) (simplify b)
-simplify (Iff a b) = Iff (simplify a) (simplify b)
-                        
diff --git a/tests/tests.hs b/tests/tests.hs
--- a/tests/tests.hs
+++ b/tests/tests.hs
@@ -4,15 +4,15 @@
 import Picologic.Pretty
 
 import Test.QuickCheck
+import Data.List
 import qualified Data.Map as M
-import qualified Data.Set as S
 import System.Exit (exitFailure)
 import System.IO.Unsafe (unsafePerformIO)
 
 instance Arbitrary Expr where
   arbitrary = sized $ \n ->
                 tree (round $ sqrt $ fromIntegral n :: Int)
-    where tree 0 = elements $ map (Var . Ident) ["a", "b", "c", "d"]
+    where tree 0 = elements $ map (Var . Ident) (concat $ replicate 3 ["a", "b", "c", "d"]) ++ [Top, Bottom]
           tree n =
             oneof
             [do a <- tree (pred n)
@@ -38,12 +38,15 @@
   shrink (Iff a b) = [a, b]
                      ++ map (Iff a) (shrink b)
                      ++ map (\aa-> Iff aa b) (shrink a)
+  shrink Top = []
+  shrink Bottom = []
 
 
-env = M.fromList [(Ident "a", True),
-                  (Ident "b", True),
-                  (Ident "c", False),
-                  (Ident "d", False)]
+envl = [(Ident "a", True),
+        (Ident "b", True),
+        (Ident "c", False),
+        (Ident "d", False)]
+env = M.fromList envl
 
 test_nnf :: Expr -> Bool
 test_nnf e = eval env e == eval env (nnf e)
@@ -54,6 +57,7 @@
 test_tseitin :: Expr -> Bool
 test_tseitin e = unsafePerformIO test
   where test = do
+          let vars = variables e
           let ts = tseitinCNF e
           -- putStrLn "\nexpr"
           -- print $ ppExprLisp e
@@ -61,17 +65,28 @@
           -- print $ ppExprLisp ts
           -- putStrLn "tseitin clauses"
           -- mapM_ print $ clausesExpr ts
-          as <- solveCNF $ cnf e
+          let ce = cnf e
+          as <- solveCNF ce
           bs0 <- solveCNF ts
           let bs =  dropTseitinVarsInSolutions bs0
-          case (as, bs) of
-            (Solutions av, Solutions bv) -> do
-              --print ("as", av)
-              --print ("bs", bv)
-              return $ S.fromList av == S.fromList bv
+          let as1 = addVarsToSolutions vars as
+          let bs1 = addVarsToSolutions vars bs
+          --print ("as", as)
+          --print ("bs", bs)
+          return $ normalize as1 == normalize bs1
+        normalize (Solutions ssv) = sort $ map sort ssv
 
-qc = verboseCheckWith (stdArgs { maxSuccess = 1000 })
+test_partEval :: Expr -> Bool
+test_partEval e = if eval env e
+                  then elast == Top
+                  else elast == Bottom
+  where
+    envs = map (\(i,v) -> M.singleton i v) envl
+    elast = last $ scanl (flip partEval) e envs
 
+
+qc = verboseCheckWith (stdArgs { maxSuccess = 2000 })
+
 -- how to make an error fail a 'cabal test'?
 qcwf p = verboseCheckWith (stdArgs { maxSuccess = 1000 })
          (whenFail exitFailure p)
@@ -83,3 +98,5 @@
   qc test_cnf
   putStrLn "tseitin"
   qc test_tseitin
+  putStrLn "partEval"
+  qc test_partEval