diff --git a/Data/BoolSimplifier.hs b/Data/BoolSimplifier.hs
new file mode 100644
--- /dev/null
+++ b/Data/BoolSimplifier.hs
@@ -0,0 +1,396 @@
+{- |
+Module      :  Data.BoolSimplifier
+Copyright   :  (c) Gershom Bazerman, Jeff Polakow 2011
+License     :  BSD 3 Clause
+Maintainer  :  gershomb@gmail.com
+Stability   :  experimental
+
+Machinery for representing and simplifying simple propositional formulas. Type families are used to maintain a simple normal form, taking advantage of the duality between "And" and "Or". Additional tools are provided to pull out common atoms in subformulas and otherwise iterate until a simplified fixpoint. Full and general simplification is NP-hard, but the tools here can take typical machine-generated formulas and perform most simplifications that could be spotted and done by hand by a reasonable programmer.
+
+-}
+
+{-# LANGUAGE
+             EmptyDataDecls,
+             FlexibleContexts,
+             FlexibleInstances,
+             FunctionalDependencies,
+             GADTs,
+             MultiParamTypeClasses,
+             OverlappingInstances,
+             PatternGuards,
+             ScopedTypeVariables,
+             TypeFamilies,
+             TypeSynonymInstances,
+             UndecidableInstances
+ #-}
+
+module Data.BoolSimplifier where
+
+import Prelude hiding (tail, init, head, last, minimum, maximum, foldr1, foldl1, (!!), read)
+
+import Data.List(intercalate, maximumBy)
+import Data.Ord(comparing)
+import qualified Data.Map as M
+import Data.Monoid
+import qualified Data.Set as S
+import Data.Set(Set)
+import Data.Foldable (foldMap)
+import qualified Data.Foldable as F
+
+{-
+-}
+
+
+-- | We'll start with three types of formulas: disjunctions, conjunctions, and atoms
+data QOrTyp
+data QAndTyp
+data QAtomTyp
+
+instance Show QOrTyp where
+    show _ = "|"
+instance Show QAndTyp where
+    show _ = "&"
+
+
+-- | disjunction is the dual of conjunction and vice-versa
+type family QFlipTyp t :: *
+type instance QFlipTyp QOrTyp = QAndTyp
+type instance QFlipTyp QAndTyp = QOrTyp
+
+{-|
+
+  A formula is either an atom (of some type, e.g. @String@).
+
+  A non-atomic formula (which is either a disjunction or a conjunction) is
+  n-ary and consists of a @Set@ of atoms and a set of non-atomic subformulas of
+  dual connective, i.e. the non-atomic subformulas of a disjunction must all
+  be conjunctions.  The type system enforces this since there is no @QFlipTyp@
+  instance for @QAtomTyp@.
+
+-}
+data QueryRep qtyp a where
+    QAtom :: (Ord a) => a -> QueryRep QAtomTyp a
+    QOp   :: (Show qtyp, Ord a) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a
+
+
+extractAs :: QueryRep qtyp a -> Set (QueryRep QAtomTyp a)
+extractAs (QOp as _) = as
+extractAs _ = S.empty
+
+extractCs :: QueryRep qtyp a -> Set (QueryRep (QFlipTyp qtyp) a)
+extractCs (QOp _ cs) = cs
+extractCs _ = S.empty
+
+-- | convenience constructors, not particularly smart
+qOr :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QAndTyp a) -> QueryRep QOrTyp a
+qOr = QOp
+qAnd :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QOrTyp a) -> QueryRep QAndTyp a
+qAnd = QOp
+
+
+instance (Eq a) => Eq (QueryRep qtyp a) where
+    (QAtom x) == (QAtom y) = x == y
+    (QOp as cs) == (QOp as' cs') = as == as' && cs == cs'
+    _ == _ = False  -- can't happen
+
+instance (Ord a) => Ord (QueryRep qtyp a) where
+    compare (QAtom x) (QAtom y) = compare x y
+    compare (QOp as cs) (QOp as' cs') = compare as as' `mappend` compare cs cs'
+    compare (QAtom _) _ = GT  -- can't happen
+    compare _ _ = LT  -- can't happen
+
+instance (Show a) => Show (QueryRep qtyp a) where
+    show (QAtom x) = "QAtom " ++ show x
+    show (QOp as cs) = intercalate " " ["QOp", show (undefined :: qtyp), show as, show cs]
+
+-- | pretty printer class
+class PPQueryRep a where
+    ppQueryRep :: a -> String
+
+instance PPQueryRep (QueryRep qtyp String) where
+    ppQueryRep (QAtom s) = s
+    ppQueryRep (QOp as cs) = "(" ++
+                             intercalate (" " ++ show (undefined::qtyp) ++ " ")
+                                         (map ppQueryRep (S.toList as) ++ map ppQueryRep (S.toList cs)) ++
+                             ")"
+
+
+-- | smart constructor for @QOp@
+--   does following optimization: a /\ (a \/ b) <-> a, or dually: a \/ (a /\ b) <-> a
+qop :: (Ord a,
+        Show qtyp,
+        Show (QFlipTyp qtyp),
+        QFlipTyp (QFlipTyp qtyp) ~ qtyp
+       ) =>
+       Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a
+qop as cs = QOp as' $ S.filter (\c -> not $ any (c `hasClause`) $ S.toList as') cs'
+    where
+      as' = S.unions [as, newas, neweras]
+
+      cs' = S.unions [remainingcs, newcs]
+
+      isUnaryOp (QOp as'' cs'') = S.size cs'' + S.size as'' == 1
+      isUnaryOp _ = False
+
+      -- | Each @unarycs@ has type @QOp (QFlipTyp qtyp) a@ and is either @QOp {a} {}@ or @QOp {} {q}@
+      --   Note that @QOp {a} {}@ = @a@ and @QOp {} {q}@ = @q@
+      (unarycs, remainingcs) = S.partition isUnaryOp cs
+
+      newas = foldMap extractAs unarycs
+
+      (newcs, neweras) = extractAtomCs unarycs
+
+
+extractAtomCs :: (Ord a,
+                  Show qtyp,
+                  Show (QFlipTyp qtyp),
+                  QFlipTyp (QFlipTyp qtyp) ~ qtyp
+                 ) =>
+                 Set (QueryRep qtyp a) -> (Set (QueryRep qtyp a), Set (QueryRep QAtomTyp a))
+extractAtomCs cs = (opClauses, atomClauses)
+    where
+      cs' = foldMap extractCs cs
+      atomClauses = foldMap extractAs cs'
+      opClauses = foldMap extractCs cs'
+
+
+{-|
+
+QueryReps can be queried for clauses within them, and clauses within them can be extracted.  
+
+-}
+class HasClause fife qtyp
+    where hasClause :: QueryRep fife a -> QueryRep qtyp a -> Bool
+          stripClause :: QueryRep qtyp a -> QueryRep fife a -> QueryRep fife a
+
+instance HasClause fife QAtomTyp
+    where hasClause (QOp as _) c@(QAtom _) = c `S.member` as
+          hasClause _ _ = False
+          stripClause c (QOp as cs) = QOp (S.delete c as) cs
+          stripClause _ x = x
+
+instance (QFlipTyp fife ~ qtyp) => HasClause fife qtyp
+    where hasClause (QOp _ cs) c@(QOp _ _) = c `S.member` cs
+          hasClause _ _ = False
+          stripClause c (QOp as cs) = QOp as (S.delete c cs)
+          stripClause _ x = x
+
+-- | convenience functions
+andqs :: Ord a => (CombineQ a qtyp QAndTyp) => [QueryRep qtyp a] -> QueryRep QAndTyp a
+andqs = foldr andq (qop S.empty S.empty)
+
+orqs :: Ord a => (CombineQ a qtyp QOrTyp) => [QueryRep qtyp a] -> QueryRep QOrTyp a
+orqs = foldr orq (qop S.empty S.empty)
+
+
+-- | smart constructors for @QueryRep@
+class CombineQ a qtyp1 qtyp2 where
+    andq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QAndTyp a
+    orq  :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QOrTyp  a
+
+instance Ord a => CombineQ a QAndTyp QAndTyp where
+    andq (QOp as cs) (QOp as' cs') = qop (S.union as as') (S.union cs cs')
+
+    orq x y = qop S.empty (S.fromList [x,y])
+
+instance Ord a => CombineQ a QAndTyp QOrTyp where
+    andq (QOp as cs) y = qop as (S.insert y cs)
+
+    orq x (QOp as cs)  = qop as (S.insert x cs)
+
+instance Ord a => CombineQ a QAndTyp QAtomTyp where
+    andq (QOp as cs) y = qop (S.insert y as) cs
+
+    orq x y = qop (S.singleton y) (S.singleton x)
+
+
+instance Ord a => CombineQ a QOrTyp QAndTyp where
+    andq x y = andq y x
+    orq  x y = orq  y x
+
+instance Ord a => CombineQ a QOrTyp QOrTyp where
+    andq x y = qop S.empty (S.fromList [x,y])
+    orq (QOp as cs) (QOp as' cs') = qop (S.union as as') (S.union cs cs')
+
+instance Ord a => CombineQ a QOrTyp QAtomTyp where
+    andq x y = qop (S.singleton y) (S.singleton x)
+    orq (QOp as cs) y = qop (S.insert y as) cs
+
+instance Ord a => CombineQ a QAtomTyp QAndTyp where
+    andq x y = andq y x
+    orq  x y = orq  y x
+
+instance Ord a => CombineQ a QAtomTyp QOrTyp where
+    andq x y = andq y x
+    orq  x y = orq  y x
+
+instance Ord a => CombineQ a QAtomTyp QAtomTyp where
+    andq x y = qop (S.fromList [x,y]) S.empty
+    orq  x y = qop (S.fromList [x,y]) S.empty
+
+
+-- | (a /\ b) \/ (a /\ c) \/ d <-> (a /\ (b \/ c)) \/ d
+-- (and also the dual)
+simplifyQueryRep :: (Ord a, Show (QFlipTyp qtyp), Show (QFlipTyp (QFlipTyp qtyp)), QFlipTyp (QFlipTyp qtyp) ~ qtyp) =>
+                    QueryRep qtyp a -> QueryRep qtyp a
+simplifyQueryRep (QOp as cs')
+        | Just (comVal, comCs, restCs) <- getCommonClauseAs cs = simplifyQueryRep $
+                  qop as (S.insert (qop (S.singleton comVal) (S.singleton $ qop S.empty comCs)) restCs)
+
+        | Just (comVal, comCs, restCs) <- getCommonClauseCs cs = simplifyQueryRep $
+                  qop as (S.insert (qop S.empty $ S.fromList [comVal, qop S.empty comCs]) restCs)
+
+        | otherwise = QOp as cs
+      where
+        cs = S.map simplifyQueryRep cs'
+
+simplifyQueryRep x = x
+
+-- | Given a set of QueryReps, extracts a common clause if possible, returning the clause, the terms from which the clause has been extracted, and the rest.
+getCommonClauseAs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep QAtomTyp a,
+                                                              Set (QueryRep fife a),
+                                                              Set (QueryRep fife a))
+getCommonClauseAs cs
+    | M.size mp > 0 && countMax > (1::Int) = Just $ (maxClause, S.map (stripClause maxClause) com, rest)
+    | otherwise = Nothing
+  where
+    (com, rest) = S.partition (`hasClause` maxClause) cs
+    mp = mkClauseMap cs
+    (maxClause, countMax) =  maximumByNote "getCommonClause" (comparing snd) $ M.toList mp
+    mkClauseMap = foldr go M.empty . F.concatMap (S.toList . extractAs)
+      where go c x = M.insertWith (+) c 1 x
+
+getCommonClauseCs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep (QFlipTyp fife) a,
+                                                              Set (QueryRep fife a),
+                                                              Set (QueryRep fife a))
+getCommonClauseCs cs
+    | M.size mp > 0 && countMax > (1::Int) = Just $ (maxClause, S.map (stripClauseLocal maxClause) com, rest)
+    | otherwise = Nothing
+  where
+    (com, rest) = S.partition (`hasClauseLocal` maxClause) cs
+    mp = mkClauseMap cs
+    (maxClause, countMax) =  maximumByNote "getCommonClause" (comparing snd) $ M.toList mp
+    mkClauseMap = foldr go M.empty . F.concatMap (S.toList . extractCs)
+    
+    go c x = M.insertWith (+) c 1 x
+
+    hasClauseLocal (QOp _ css) c@(QOp _ _) = c `S.member` css
+    hasClauseLocal _ _ = False
+    
+    stripClauseLocal c (QOp as css) = QOp as (S.delete c css)
+    stripClauseLocal _ x = x
+
+-- | Takes any given simplifier and repeatedly applies it until it ceases to reduce the size of the query reprepresentation.
+fixSimplifyQueryRep  :: (QueryRep qtyp a -> QueryRep qtyp a) -> QueryRep qtyp a -> QueryRep qtyp a
+fixSimplifyQueryRep simplify x
+    | initl <= endl = x
+    | otherwise = fixSimplifyQueryRep simplify res
+  where
+    res = simplify x
+    initl = qSize x
+    endl  = qSize res
+
+    qSize :: QueryRep qtyp a -> Int
+    qSize (QOp as cs) = sum (map qSize $ S.toList as) +
+                        sum (map qSize $ S.toList cs)
+    qSize (QAtom _) = 1
+
+
+-- | We can wrap any underying atom dype in an Ion to give it a "polarity" and add handling of "not" to our simplification tools.
+data Ion a = Neg a | Pos a deriving (Eq, Ord, Show)
+
+qAtom :: Ord a => a -> QueryRep QAtomTyp (Ion a)
+qAtom = QAtom . Pos
+
+isEmptyQR, isConstQR :: QueryRep qtyp a -> Bool
+isEmptyQR (QOp as cs) = S.null as && S.null cs
+isEmptyQR _ = False
+
+isConstQR (QOp as cs) | S.null as && S.size cs == 1 = isEmptyQR (S.findMin cs)
+isConstQR _ = False
+
+instance PPQueryRep (QueryRep QAndTyp (Ion String)) where
+--    ppQueryRep (QAtom (Pos s)) = s
+--    ppQueryRep (QAtom (Neg s)) = "~" ++ s
+    ppQueryRep q@(QOp as cs)
+        | isEmptyQR q || isConstQR q = ppConstQR q
+        | otherwise = "(" ++
+                      intercalate (" " ++ show (undefined::QAndTyp) ++ " ")
+                                  (map ppQueryRep (S.toList as) ++ map ppQueryRep (S.toList cs)) ++
+                      ")"
+
+instance PPQueryRep (QueryRep QOrTyp (Ion String)) where
+--    ppQueryRep (QAtom (Pos s)) = s
+--    ppQueryRep (QAtom (Neg s)) = "~" ++ s
+    ppQueryRep q@(QOp as cs)
+        | isEmptyQR q || isConstQR q = ppConstQR q
+        | otherwise = "(" ++
+                      intercalate (" " ++ show (undefined::QOrTyp) ++ " ")
+                                  (map ppQueryRep (S.toList as) ++ map ppQueryRep (S.toList cs)) ++
+                      ")"
+
+instance PPQueryRep (QueryRep QAtomTyp (Ion String)) where
+    ppQueryRep (QAtom (Pos s)) = s
+    ppQueryRep (QAtom (Neg s)) = "~" ++ s
+    ppQueryRep (QOp _ _) = error "the type system does not work"
+
+class PPConstQR qtyp where
+    ppConstQR :: QueryRep qtyp a -> String
+instance PPConstQR QAndTyp where
+    ppConstQR q | isEmptyQR q = "False"
+                | otherwise = "True"
+instance PPConstQR QOrTyp where
+    ppConstQR q | isEmptyQR q = "True"
+                | otherwise = "False"
+instance PPConstQR a where
+    ppConstQR _ = error "impossible PPConstQR"
+
+
+class QNot qtyp where
+    type QNeg qtyp
+    qNot :: QueryRep qtyp (Ion a) -> QueryRep (QNeg qtyp) (Ion a)
+
+instance QNot QAtomTyp where
+    type QNeg QAtomTyp = QAtomTyp
+    qNot (QAtom (Neg a)) = QAtom (Pos a)
+    qNot (QAtom (Pos a)) = QAtom (Neg a)
+    qNot _ = error "qNot"
+
+instance QNot QOrTyp where
+    type QNeg QOrTyp = QAndTyp
+    qNot (QOp as cs) = QOp (S.map qNot as) (S.map qNot cs)
+
+instance QNot QAndTyp where
+    type QNeg QAndTyp = QOrTyp
+    qNot (QOp as cs) = QOp (S.map qNot as) (S.map qNot cs)
+
+-- | a  /\  (b \/ ~b)  /\  (c \/ d)   <->   a /\ (c \/ d)
+--   a  /\  ~a         /\  (b \/ c)   <->   False
+--          (a \/ ~a)  /\  (b \/ ~b)  <->   True  (*)
+--
+-- and duals
+--
+-- N.B. 0-ary \/ is False and 0-ary /\ is True
+--
+simplifyIons :: (Ord a, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp (Ion a) -> QueryRep qtyp (Ion a)
+simplifyIons (QOp as cs)
+    | nullified = QOp S.empty S.empty
+    | S.null as && S.null cs' = QOp S.empty (S.singleton $ QOp S.empty S.empty)  -- for (*) above
+    | otherwise = qop as cs'
+  where
+    cs' = S.filter (not . isEmptyQR) $ S.map simplifyIons cs  -- simplify sub formulas
+
+    go acc (a:as') | qNot a `S.member` acc = True        -- check for opposite polarity atoms in this formula
+                  | otherwise = go (S.insert a acc) as'
+    go _ [] = False
+
+    nullified = go S.empty (S.toList as) || any isConstQR (S.toList cs')  -- isConstQR detects whether a formula is 0-ary
+simplifyIons x = x
+
+
+--simpleTest = orq (qAtom "a") (qAtom "b") `andq` orq (qAtom "a") (qAtom "c")
+--simpleTest1 = orq (qNot $ qAtom "a") (qAtom "b") `andq` orq (qAtom "a") (qAtom "c")
+
+maximumByNote :: String -> (a -> a -> Ordering) -> [a] -> a
+maximumByNote err _ [] = error $ "maximumByNote: " ++ err
+maximumByNote _   f xs = maximumBy f xs
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c)2012, Gershom Bazerman, Jeff Polakow
+
+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.
+
+    * Neither the name of Gershom Bazerman, Jeff Polakow nor the names of other
+      contributors may 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.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/boolsimplifier.cabal b/boolsimplifier.cabal
new file mode 100644
--- /dev/null
+++ b/boolsimplifier.cabal
@@ -0,0 +1,38 @@
+Name:                boolsimplifier
+Version:             0.1
+Synopsis:            Normal form representation for boolean expressions. Typically simplifies such expressions, but is not guaranteed to produce the absolute simplest form.
+
+-- A longer description of the package.
+-- Description:         
+
+License:             BSD3
+License-file:        LICENSE
+Author:              Gershom Bazerman, Jeff Polakow
+Maintainer:          gershomb@gmail.com
+
+-- A copyright notice.
+-- Copyright:           
+
+Category:            Math, Language
+
+Build-type:          Simple
+
+-- Constraint on the version of Cabal needed to build this package.
+Cabal-version:       >=1.2
+
+
+Library
+  -- Modules exported by the library.
+  Exposed-modules:     Data.BoolSimplifier
+  
+  -- Packages needed in order to build this package.
+  Build-depends: base >= 4, base < 7, containers >= 0.4
+  
+  ghc-options: -Wall
+
+  -- Modules not exported by this package.
+  -- Other-modules:       
+  
+  -- Extra tools (e.g. alex, hsc2hs, ...) needed to build the source.
+  -- Build-tools:         
+