diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) Tom Hawkins 2011
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. 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.
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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,8 @@
+#! /usr/bin/env runhaskell
+
+> module Main (main) where
+>
+> import Distribution.Simple (defaultMain)
+>
+> main :: IO ()
+> main = defaultMain
diff --git a/TheoremQuest.hs b/TheoremQuest.hs
new file mode 100644
--- /dev/null
+++ b/TheoremQuest.hs
@@ -0,0 +1,8 @@
+module TheoremQuest
+  ( module TheoremQuest.Logic
+  , module TheoremQuest.Transactions
+  ) where
+
+import TheoremQuest.Logic
+import TheoremQuest.Transactions
+
diff --git a/TheoremQuest/Logic.hs b/TheoremQuest/Logic.hs
new file mode 100644
--- /dev/null
+++ b/TheoremQuest/Logic.hs
@@ -0,0 +1,161 @@
+module TheoremQuest.Logic
+  ( Term          (..)
+  , Proposition
+  , Variable      (..)
+  , Theorem
+  , Type          (..)
+  , Inference     (..)
+  , Axiom         (..)
+  , TypeOf        (..)
+  , (=.)
+  , assumptions
+  , conclusion
+  , inference
+  , wellTyped
+  , freeIn
+  , freeVariables
+  ) where
+
+import Data.List
+
+infix  4 =.
+infixr 1 :->
+
+data Term
+  = Const String Type
+  | Var   Variable
+  | Abs   Variable Term
+  | Comb  Term Term
+  deriving (Show, Read, Eq)
+
+-- | A boolean term.
+type Proposition = Term
+
+data Variable = Variable String Type
+  deriving (Show, Read)
+
+instance Eq Variable where
+  Variable a _ == Variable b _ = a == b
+
+data Theorem = Theorem [Proposition] Proposition
+
+-- | Assumptions of a 'Theorem'.
+assumptions :: Theorem -> [Proposition]
+assumptions (Theorem a _) = a
+
+-- | Conclusion of a 'Theorem'.
+conclusion :: Theorem -> Proposition
+conclusion (Theorem _ a) = a
+
+data Type
+  = Bool
+  | Type :-> Type
+  deriving (Show, Read)
+
+instance Eq Type where
+  Bool == Bool = True
+  (a :-> b) == (x :-> y) = a == x && b == y
+  _ == _ = False
+
+
+data Inference a
+  = REFL           Term
+  | TRANS          a a
+  | MK_COMB        a a
+  | ABS            Term a
+  | BETA           Term
+  | ASSUME         Term
+  | EQ_MP          a a
+  | DEDUCT_ANTISYM a a
+  | INST           [(Variable, Term)] a
+  | INST_TYPE      [(Type, Type)] a
+  | AXIOM          Axiom
+  deriving (Show, Read)
+
+data Axiom
+  = Axiom
+  deriving (Show, Read)
+
+class    TypeOf a        where typeOf :: a -> Type
+instance TypeOf Type     where typeOf = id
+instance TypeOf Variable where typeOf (Variable _ t) = t
+instance TypeOf Term where
+  typeOf a = case a of
+    Const _ t -> t
+    Var v -> typeOf v
+    Comb f _ -> case typeOf f of
+      _ :-> a -> a
+      _ -> error "invalid type for Comb"
+    Abs (Variable _ t) b -> t :-> typeOf b
+
+(=.) :: Term -> Term -> Term
+a =. b = Comb (Comb (Const "=" $ typeOf a :-> typeOf a :-> Bool) a) b
+-- XXX Need to better understand mk_eq.
+
+-- | Creates a 'Theorem' from an 'Inference' rule application.
+inference :: Inference Theorem -> Maybe Theorem
+inference rule = case rule of
+  REFL a -> validateTheorem [] (a =. a)
+  TRANS (Theorem a1 (Comb (Comb (Const "=" _) a2) a3)) (Theorem b1 (Comb (Comb (Const "=" _) b2) b3)) | a3 == b2 -> validateTheorem (union a1 b1) (a2 =. b3)
+  MK_COMB (Theorem a1 (Comb (Comb (Const "=" _) a2) a3)) (Theorem b1 (Comb (Comb (Const "=" _) b2) b3)) -> validateTheorem (union a1 b1) (Comb a2 b2 =. Comb a3 b3)
+  ABS (Var x) (Theorem a1 (Comb (Comb (Const "=" _) a2) a3)) | not $ any (freeIn x) a1 -> validateTheorem a1 (Abs x a2 =. Abs x a3)
+  BETA a@(Comb (Abs x1 t)(Var x2)) | x1 == x2 -> validateTheorem [] $ a =. t
+  ASSUME p -> validateTheorem [p] p
+  EQ_MP (Theorem a1 (Comb (Comb (Const "=" _) a2) a3)) (Theorem b1 b2) | a2 == b2 -> validateTheorem (union a1 b1) a3
+  DEDUCT_ANTISYM (Theorem a1 a2) (Theorem b1 b2) -> validateTheorem (union (delete b2 a1) (delete a2 b1)) $ a2 =. b2
+  INST subs (Theorem assumes prop) -> validateTheorem (map (replace subs) assumes) (replace subs prop)
+    where
+    replace subs a = case a of
+      Const _ _ -> a
+      Var v -> case lookup v subs of
+        Nothing -> a
+	Just t  -> t
+      Abs v a -> Abs v $ replace [ (v', t) | (v', t) <- subs, v /= v' ] a
+      Comb a b -> Comb (replace subs a) (replace subs b)
+  -- INST_TYPE           Theorem [(Type, Type)]
+  -- AXIOM               Axiom
+  _ -> Nothing
+
+-- | Validates (type checks) a theorem.
+validateTheorem :: [Term] -> Term -> Maybe Theorem
+validateTheorem assumptions conclusion
+  | all (\ t -> wellTyped t && typeOf t == Bool) (conclusion : assumptions) = Just $ Theorem assumptions conclusion
+  | otherwise = Nothing
+
+-- | Checks if a term is well-typed.
+wellTyped :: Term -> Bool
+wellTyped a = wellTyped (freeVariables a) a
+  where
+  wellTyped :: [Variable] -> Term -> Bool
+  wellTyped env a = case a of
+    Const _ (_ :-> _) -> False
+    Const _ _ -> True
+    Var v -> wellTypedVar env v
+    Comb fun arg -> case typeOf fun of
+      argType :-> _ -> typeOf arg == argType && wellTyped env fun && wellTyped env arg
+      _ -> False
+    Abs x t -> wellTyped (x : env) t
+
+  wellTypedVar :: [Variable] -> Variable -> Bool
+  wellTypedVar [] _ = False
+  wellTypedVar (Variable name t : rest) v@(Variable name' t')
+    | name == name' = t == t'
+    | otherwise = wellTypedVar rest v
+
+-- | Checks if a variable is free in a term.
+freeIn :: Variable -> Term -> Bool
+freeIn (Variable name _) t = elem name [ n | Variable n _ <- freeVariables t ]
+
+-- | All free variables in a term.
+freeVariables :: Term -> [Variable]
+freeVariables = nub . variables []
+  where
+  variables :: [Variable] -> Term -> [Variable]
+  variables env a = case a of
+    Const _ _ -> []
+    Var v
+      | elem v env -> []
+      | otherwise -> [v]
+    Comb a b -> variables env a ++ variables env b
+    Abs x a -> variables (x : env) a
+
diff --git a/TheoremQuest/Transactions.hs b/TheoremQuest/Transactions.hs
new file mode 100644
--- /dev/null
+++ b/TheoremQuest/Transactions.hs
@@ -0,0 +1,81 @@
+module TheoremQuest.Transactions
+  ( Req (..)
+  , Rsp (..)
+  , User
+  , Email
+  , TheoremId
+  , formatJSON
+  , formatText
+  , formatHaskell
+  , maybeRead
+  ) where
+
+import Codec.Binary.UTF8.String (encodeString)
+import Network.HTTP
+import Text.JSON
+
+import TheoremQuest.Logic
+
+type User = String
+type Email = String
+type TheoremId = Int
+
+-- | Requests from client to server.
+data Req
+  = Ping                                   -- ^ Ping server.
+  | NewUser User Email                     -- ^ New user: username, email.
+  | RspInJSON Req                          -- ^ Send response in JSON.
+  | Inference User (Inference TheoremId)   -- ^ Submit an inference.  Server will validate the inference and return a theorem.
+  | TheoremAssumptions TheoremId           -- ^ Request a theorem's assumptions.
+  | TheoremConclusion  TheoremId           -- ^ Request a theorem's conclusion.
+  | TheoremSearch Term Int                 -- ^ Search for a theorem similar to a term.  Return a list of ids starting at the given index.
+  deriving (Show, Read)
+
+-- | Responses to client requests.
+data Rsp
+  = DeprecatedReq Rsp   -- ^ A warning to clients that the associated 'Req' will soon be obsolete.
+  | UnknownReq          -- ^ Server did not recognize 'Req'.
+  | Ack                 -- ^ Acknowledge.
+  | Nack String         -- ^ No acknowledge with reason.
+  | Id Int              -- ^ A unique id.  Usually a 'TheoremId'.
+  | Ids [Int]           -- ^ A list of unique ids.
+  | Term Term           -- ^ A term.
+  | Terms [Term]        -- ^ A list of terms.
+  deriving (Show, Read)
+
+instance JSON Rsp where
+  readJSON = undefined
+  showJSON = undefined
+  {-
+  showJSON a = case a of
+    DeprecatedReq a -> JSArray [JSString $ toJSString "DeprecatedReq", showJSON a]
+    UnknownReq      -> JSArray [JSString $ toJSString "UnknownReq"]
+    Ack             -> JSArray [JSString $ toJSString "Ack"]
+    Nack a          -> JSArray $ map (JSString . toJSString) ["Nack", a]
+    -}
+
+instance JSON Term where
+  readJSON = undefined
+  showJSON = undefined
+
+-- | HTTP headers and body for JSON transfer.
+formatJSON :: JSON a => a -> ([Header], String)
+formatJSON a = ([Header HdrContentLength $ show $ length msg, Header HdrContentEncoding "UTF-8", Header HdrContentType "application/json"], msg)
+  where
+  msg = encodeString $ encode a
+
+-- | HTTP headers and body for text transfer.
+formatText :: String -> ([Header], String)
+formatText a = ([Header HdrContentLength $ show $ length msg, Header HdrContentEncoding "UTF-8", Header HdrContentType "text/plain"], msg)
+  where
+  msg = encodeString a
+
+-- | HTTP headers and body for shown Haskell type transfer.
+formatHaskell :: Show a => a -> ([Header], String)
+formatHaskell = formatText . show
+
+-- | Maybe read, on parse errors return Nothing.
+maybeRead :: Read a => String -> Maybe a
+maybeRead s = case [x | (x,t) <- reads s, ("","") <- lex t] of
+  [x] -> Just x
+  _ -> Nothing
diff --git a/theoremquest.cabal b/theoremquest.cabal
new file mode 100644
--- /dev/null
+++ b/theoremquest.cabal
@@ -0,0 +1,34 @@
+name:    theoremquest
+version: 0.0.0
+
+category: Game, Formal Methods, Theorem Provers
+
+synopsis: A common library for TheoremQuest, a theorem proving game.
+
+description:
+  TODO
+
+author:     Tom Hawkins <tomahawkins@gmail.com>
+maintainer: Tom Hawkins <tomahawkins@gmail.com>
+
+build-type:    Simple
+cabal-version: >= 1.6
+
+license:      BSD3
+license-file: LICENSE
+
+library
+  build-depends:     base         >= 4.0    && < 5,
+                     HTTP         >= 4000.1 && < 4000.2,
+                     utf8-string  >= 0.3   && < 0.4,
+                     json         >= 0.4.4  && < 0.5
+  exposed-modules:
+    TheoremQuest
+    TheoremQuest.Logic
+    TheoremQuest.Transactions
+  ghc-options: -W
+
+source-repository head
+  type:     git
+  location: git://github.com/tomahawkins/theoremquest.git
+