diff --git a/Folly.cabal b/Folly.cabal
new file mode 100644
--- /dev/null
+++ b/Folly.cabal
@@ -0,0 +1,38 @@
+-- Initial Folly.cabal generated by cabal init.  For further documentation,
+--  see http://haskell.org/cabal/users-guide/
+
+name:                Folly
+version:             0.1.0.0
+synopsis:            A first order logic library in Haskell
+description:         An implementation of first order logic in Haskell that
+		     includes a library of modules for incorporating first
+		     order logic into other programs as well as an executable
+		     theorem prover that uses resolution to prove theorems
+		     in first order logic.
+license:             BSD3
+license-file:        LICENSE
+author:              Dillon Huff
+maintainer:          Dillon Huff
+homepage:	     https://github.com/dillonhuff/Folly
+-- copyright:           
+-- category:            
+build-type:          Simple
+cabal-version:       >=1.8
+
+library
+  exposed-modules:     Folly.Formula, Folly.Unification, Folly.Resolution, Folly.Utils
+  -- other-modules:       
+  build-depends:       base < 6, containers
+  hs-source-dirs:      src
+
+executable Folly
+  main-is:             Main.hs
+  -- other-modules:       
+  build-depends:       base < 6, containers, parsec
+  hs-source-dirs:      src
+
+executable Folly-tests
+  main-is:             Main.hs
+  -- other-modules:       
+  build-depends:       base < 6, HUnit, containers, parsec
+  hs-source-dirs:      test, src
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Dillon Huff
+
+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 Dillon Huff 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/src/Folly/Formula.hs b/src/Folly/Formula.hs
new file mode 100644
--- /dev/null
+++ b/src/Folly/Formula.hs
@@ -0,0 +1,283 @@
+module Folly.Formula(
+  Term, Formula,
+  fvt, subTerm, isVar, isConst, isFunc,
+  funcName, funcArgs,
+  appendVarName,
+  var, func, constant,
+  te, fa, pr, con, dis, neg, imp, bic, t, f,
+  vars, freeVars,
+  generalize, subFormula,
+  applyToTerms,
+  literalArgs,
+  toPNF, toSkolemForm, skf,
+  Clause,
+  toClausalForm,
+  matchingLiterals) where
+
+import Control.Monad
+import Data.Set as S
+import Data.List as L
+import Data.Map as M
+
+data Term =
+  Constant String    |
+  Var String         |
+  Func String [Term]
+  deriving (Eq, Ord)
+           
+instance Show Term where
+  show = showTerm
+   
+showTerm :: Term -> String
+showTerm (Constant name) = name
+showTerm (Var name) = name
+showTerm (Func name args) = name ++ "(" ++ (concat $ intersperse ", " $ L.map showTerm args) ++ ")"
+
+isVar (Var _) = True
+isVar _ = False
+
+isFunc (Func _ _) = True
+isFunc _ = False
+
+isConst (Constant _) = True
+isConst _ = False
+
+funcName (Func n _) = n
+
+funcArgs (Func _ a) = a
+
+var n = Var n
+func n args = case (L.take 3 n) == "skl" of
+  True -> error $ "Function names beginning with skl are reserved for skolemization"
+  False -> Func n args
+constant n = Constant n
+
+appendVarName :: String -> Term -> Term
+appendVarName suffix (Var n) = Var (n ++ suffix)
+appendVarName suffix (Func name args) = Func name $ L.map (appendVarName suffix) args
+appendVarName _ t = t
+
+fvt :: Term -> Set Term
+fvt (Constant _) = S.empty
+fvt (Var n) = S.fromList [(Var n)]
+fvt (Func name args) = S.foldl S.union S.empty (S.fromList (L.map fvt args))
+
+subTerm :: Map Term Term -> Term -> Term
+subTerm _ (Constant name) = Constant name
+subTerm sub (Func name args) = (Func name (L.map (subTerm sub) args))
+subTerm sub (Var x) = case M.lookup (Var x) sub of
+  Just s -> s
+  Nothing -> (Var x)
+
+data Formula =
+  T                            | 
+  F                            |
+  P String [Term]              |
+  B String Formula Formula     |
+  N Formula                    |
+  Q String Term Formula
+  deriving (Eq, Ord)
+           
+instance Show Formula where
+  show = showFormula
+  
+showFormula :: Formula -> String
+showFormula T = "True"
+showFormula F = "False"
+showFormula (P predName args) = predName ++ "[" ++ (concat $ intersperse ", " $ L.map showTerm args)  ++ "]"
+showFormula (N (P name args)) = "~" ++ show (P name args)
+showFormula (N f) = "~(" ++ show f ++ ")"
+showFormula (B op f1 f2) = "(" ++ show f1 ++ " " ++ op ++ " "  ++ show f2 ++ ")"
+showFormula (Q q t f) = "(" ++ q ++ " "  ++ show t ++ " . " ++ show f ++ ")"
+
+applyToTerms :: Formula -> (Term -> Term) -> Formula
+applyToTerms (P n args) f = P n $ L.map f args
+applyToTerms (B n l r) f = B n (applyToTerms l f) (applyToTerms r f)
+applyToTerms (Q n v l) f = Q n (f v) (applyToTerms l f)
+applyToTerms (N l) f = N (applyToTerms l f)
+
+te :: Term -> Formula -> Formula
+te v@(Var _) f = Q "E" v f
+te t _ = error $ "Cannot quantify over non-variable term " ++ show t
+
+fa :: Term -> Formula -> Formula
+fa v@(Var _) f = Q "V" v f
+fa t _ = error $ "Cannot quantify over non-variable term " ++ show t
+
+pr name args = P name args
+con f1 f2 = B "&" f1 f2
+dis f1 f2 = B "|" f1 f2
+imp f1 f2 = B "->" f1 f2
+bic f1 f2 = B "<->" f1 f2
+neg f = N f
+t = T
+f = F
+
+vars :: Formula -> Set Term
+vars T = S.empty
+vars F = S.empty
+vars (P name terms) = S.fold S.union S.empty $ S.fromList (L.map fvt terms)
+vars (B _ f1 f2) = S.union (vars f1) (vars f2)
+vars (N f) = vars f
+vars (Q _ v f) = S.insert v (vars f)
+
+freeVars :: Formula -> Set Term
+freeVars T = S.empty
+freeVars F = S.empty
+freeVars (P name terms) = S.fold S.union S.empty $ S.fromList (L.map fvt terms)
+freeVars (B _ f1 f2) = S.union (freeVars f1) (freeVars f2)
+freeVars (N f) = freeVars f
+freeVars (Q _ v f) = S.delete v (freeVars f)
+
+literalArgs :: Formula -> [Term]
+literalArgs (P _ a) = a
+literalArgs (N (P _ a)) = a
+literalArgs l = error $ show l ++ " is not a literal"
+
+matchingLiterals :: Formula -> Formula -> Bool
+matchingLiterals (P n1 _) (N (P n2 _)) = n1 == n2
+matchingLiterals (N (P n1 _)) (P n2 _) = n1 == n2
+matchingLiterals (P _ _) (P _ _) = False
+matchingLiterals (N (P _ _)) (N (P _ _)) = False
+matchingLiterals l1 l2 = error $ show l1 ++ " or " ++ show l2 ++ " is not a literal"
+
+generalize :: Formula -> Formula
+generalize f = applyList genFreeVar f
+  where
+    genFreeVar = L.map fa (S.toList (freeVars f))
+
+applyList :: [a -> a] -> a -> a
+applyList [] a = a
+applyList (f:fs) a = applyList fs (f a)
+
+variant :: Set Term -> Term -> Term
+variant vars x@(Var n) = case S.member x vars of
+  True -> variant vars (Var (n ++ "'"))
+  False -> x
+  
+subFormula :: Map Term Term -> Formula -> Formula
+subFormula subst (P name args) = P name $ L.map (subTerm subst) args
+subFormula subst (B op f1 f2) = B op (subFormula subst f1) (subFormula subst f2)
+subFormula subst (N f) = N (subFormula subst f)
+subFormula subst q@(Q _ _ _) = subQuant subst q
+subFormula subst f = f
+
+subQuant :: Map Term Term -> Formula -> Formula
+subQuant subst (Q n v f) = case (M.filter (== v) subst) == M.empty of
+  True -> Q n v (subFormula subst f)
+  False -> Q n vNew $ subFormula (M.insert v vNew subst) f
+  where
+    vNew = variant (freeVars (subFormula (M.delete v subst) f)) v
+    
+    
+toPNF :: Formula -> Formula
+toPNF = (transformFormula pullQuantifiers) .
+        (transformFormula simplifyFormula) .
+        (transformFormula pushNegation) .
+        (transformFormula elimVacuousQuantifiers) .
+        (transformFormula replaceImp) .
+        (transformFormula replaceBic)
+
+pullQuantifiers f@(B "&" (Q "V" x p) (Q "V" y q)) = pullQ True True f fa con x y p q
+pullQuantifiers f@(B "|" (Q "E" x p) (Q "E" y q)) = pullQ True True f te dis x y p q
+pullQuantifiers f@(B "|" (Q "V" x p) q) = pullQ True False f fa dis x x p q
+pullQuantifiers f@(B "|" p (Q "V" y q)) = pullQ False True f fa dis y y p q
+pullQuantifiers f@(B "|" (Q "E" x p) q) = pullQ True False f te dis x x p q
+pullQuantifiers f@(B "|" p (Q "E" y q)) = pullQ False True f te dis y y p q
+pullQuantifiers f@(B "&" (Q "V" x p) q) = pullQ True False f fa con x x p q
+pullQuantifiers f@(B "&" p (Q "V" y q)) = pullQ False True f fa con y y p q
+pullQuantifiers f@(B "&" (Q "E" x p) q) = pullQ True False f te con x x p q
+pullQuantifiers f@(B "&" p (Q "E" y q)) = pullQ False True f te con y y p q
+pullQuantifiers f = f
+
+pullQ :: Bool ->
+         Bool ->
+         Formula ->
+         (Term -> Formula -> Formula) ->
+         (Formula -> Formula -> Formula) ->
+         Term ->
+         Term ->
+         Formula ->
+         Formula ->
+         Formula
+pullQ l r f quant op x y p q =
+  let z = variant (freeVars f) x in
+  let ps = if l then subFormula (M.singleton x z) p else p in
+  let qs = if r then subFormula (M.singleton y z) q else q in
+  quant z (pullQuantifiers $ op ps qs)
+
+simplifyFormula (N (N f)) = f
+simplifyFormula (N T) = F
+simplifyFormula (N F) = T
+simplifyFormula (B "|" T f) = T
+simplifyFormula (B "|" f T) = T
+simplifyFormula (B "|" F F) = F
+simplifyFormula (B "&" F f) = F
+simplifyFormula (B "&" f F) = F
+simplifyFormula (B "&" T T) = T
+simplifyFormula f = f
+
+pushNegation (N (B "|" f1 f2)) = B "&" (pushNegation (N f1)) (pushNegation (N f2))
+pushNegation (N (B "&" f1 f2)) = B "|" (pushNegation (N f1)) (pushNegation (N f2))
+pushNegation (N (Q "V" x f)) = Q "E" x (pushNegation (N f))
+pushNegation (N (Q "E" x f)) = Q "V" x (pushNegation (N f))
+pushNegation f = f
+
+elimVacuousQuantifiers (Q n x f) = case S.member x (freeVars f) of
+  True -> Q n x f
+  False -> f
+elimVacuousQuantifiers f = f
+
+replaceImp (B "->" f1 f2) = dis (neg f1) f2
+replaceImp f = f
+
+replaceBic (B "<->" f1 f2) = con (imp f1 f2) (imp f2 f1)
+replaceBic f = f
+
+transformFormula :: (Formula -> Formula) -> Formula -> Formula
+transformFormula tran (B op f1 f2) = tran (B op (transformFormula tran f1) (transformFormula tran f2))
+transformFormula tran (Q q x f) = tran (Q q x (transformFormula tran f))
+transformFormula tran (N f) = tran (N (transformFormula tran f))
+transformFormula tran f = tran f
+
+-- Conversion to Skolem form
+toSkolemForm :: Formula -> Formula
+toSkolemForm = skolemize . toPNF
+
+skolemize :: Formula -> Formula
+skolemize f = (transformFormula removeExistential) $ replaceVarsWithSkolemFuncs f
+
+removeExistential :: Formula -> Formula
+removeExistential (Q "E" v f) = f
+removeExistential f = f
+
+replaceVarsWithSkolemFuncs :: Formula -> Formula
+replaceVarsWithSkolemFuncs f = subFormula varsToSkolemFuncs f
+  where
+    varsToSkolemFuncs = collectSkolemFuncs f 0 []
+    
+collectSkolemFuncs :: Formula -> Int -> [Term] -> Map Term Term
+collectSkolemFuncs (Q "E" v f) n vars = M.insert v (skf n vars) (collectSkolemFuncs f (n+1) vars)
+collectSkolemFuncs (Q "V" v f) n vars = collectSkolemFuncs f n (v:vars)
+collectSkolemFuncs _ _ _ = M.empty
+
+skf :: Int -> [Term] -> Term
+skf n vars = Func ("skl" ++ show n) vars
+
+-- Conversion to clausal form
+type Clause = [Formula]
+
+toClausalForm :: Formula -> [Clause]
+toClausalForm = splitClauses . removeUniversals . toSkolemForm
+
+removeUniversals :: Formula -> Formula
+removeUniversals (Q "V" v f) = removeUniversals f
+removeUniversals f = f
+
+splitClauses :: Formula -> [Clause]
+splitClauses (B "&" l r) = (splitClauses l) ++ (splitClauses r)
+splitClauses f = [splitDis f]
+
+splitDis :: Formula -> Clause
+splitDis (B "|" l r) = (splitDis l) ++ (splitDis r)
+splitDis f = [f]
diff --git a/src/Folly/Resolution.hs b/src/Folly/Resolution.hs
new file mode 100644
--- /dev/null
+++ b/src/Folly/Resolution.hs
@@ -0,0 +1,66 @@
+module Folly.Resolution(
+  isValid) where
+
+import Data.List as L
+import Data.Maybe
+import Data.Set as S
+
+import Folly.Formula
+import Folly.Theorem
+import Folly.Unification
+
+isValid :: Theorem -> Bool
+isValid t = not $ resolve clauseSet
+  where
+    formulas = (neg (conclusion t)) : (hypothesis t)
+    clauses = uniqueVarNames $ L.concat $ L.map toClausalForm formulas
+    clauseSet = S.fromList clauses
+
+resolve :: Set Clause -> Bool
+resolve cls = case S.member [] cls of
+  True -> False
+  False -> resolveIter [cls]
+
+resolveIter :: [Set Clause] -> Bool
+resolveIter [] = error "Empty list of clause sets"
+resolveIter clauseSets = case S.size newClauses == 0 of
+  True -> True
+  False -> case S.member [] newClauses of
+    True -> False
+    False -> resolveIter (newClauses:clauseSets)
+  where
+    newClauses = case L.length clauseSets of
+      1 -> generateNewClauses (head clauseSets) (head clauseSets)
+      _ -> generateNewClauses (head clauseSets) (L.foldl S.union S.empty (tail clauseSets))
+
+generateNewClauses :: Set Clause -> Set Clause -> Set Clause
+generateNewClauses recent old = newClauses
+  where
+    newClauses = S.fold S.union S.empty $ S.map (\ c -> genNewClauses c old) recent
+    genNewClauses c cs = S.fold S.union S.empty $ S.map (\ x -> resolvedClauses c x) cs
+
+resolvedClauses :: Clause -> Clause -> Set Clause
+resolvedClauses left right = S.fromList resClauses
+  where
+    mResClauses = L.map (\ x -> (L.map (\ y -> tryToResolve x left y right) right)) left
+    resClauses = L.map fromJust $ L.filter (/= Nothing) $ L.concat mResClauses 
+
+tryToResolve :: Formula -> Clause -> Formula -> Clause -> Maybe Clause
+tryToResolve leftLiteral leftClause rightLiteral rightClause =
+  case matchingLiterals leftLiteral rightLiteral of
+    True -> unifiedResolvedClause leftLiteral leftClause rightLiteral rightClause
+    False -> Nothing
+
+unifiedResolvedClause :: Formula -> Clause -> Formula -> Clause -> Maybe Clause
+unifiedResolvedClause lLit lc rLit rc = case mostGeneralUnifier $ zip (literalArgs lLit) (literalArgs rLit) of
+  Just mgu -> Just $ L.map (\ lit -> applyToTerms lit (applyUnifier mgu)) ((L.delete lLit lc) ++ (L.delete rLit rc))
+  Nothing -> Nothing
+
+uniqueVarNames :: [Clause] -> [Clause]
+uniqueVarNames cls = zipWith attachSuffix cls (L.map show [1..length cls])
+
+attachSuffix :: Clause -> String -> Clause
+attachSuffix cls suffix = L.map (addSuffixToVarNames suffix) cls
+
+addSuffixToVarNames :: String -> Formula -> Formula
+addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix)
diff --git a/src/Folly/Unification.hs b/src/Folly/Unification.hs
new file mode 100644
--- /dev/null
+++ b/src/Folly/Unification.hs
@@ -0,0 +1,50 @@
+module Folly.Unification(
+  applyUnifier,
+  mostGeneralUnifier,
+  unifier) where
+
+import Control.Monad
+import Data.List as L
+import Data.Map as M
+import Data.Set as S
+
+import Folly.Formula
+
+type Unifier = Map Term Term
+
+unifier :: [(Term, Term)] -> Unifier
+unifier subs = M.fromList subs
+
+applyUnifier :: Unifier -> Term -> Term
+applyUnifier u t = case possibleSubs u t of
+  True -> applyUnifier u (subTerm u t)
+  False -> t
+
+possibleSubs :: Unifier -> Term -> Bool
+possibleSubs u t = (length $ L.intersect (keys u) (S.toList (fvt t))) /= 0
+
+mostGeneralUnifier :: [(Term, Term)] -> Maybe Unifier
+mostGeneralUnifier toUnify = liftM M.fromList $ martelliMontanari toUnify
+
+martelliMontanari :: [(Term, Term)] -> Maybe [(Term, Term)]
+martelliMontanari [] = Just []
+martelliMontanari ((t1, t2):rest) = case t1 == t2 of
+  True -> martelliMontanari rest
+  False -> case isVar t1 of
+    True -> eliminateVar t1 t2 rest 
+    False -> case isVar t2 of
+      True -> martelliMontanari ((t2, t1):rest)
+      False -> case isFunc t1 && isFunc t2 && funcName t1 == funcName t2 of
+        True -> martelliMontanari $ (zip (funcArgs t1) (funcArgs t2)) ++ rest
+        False -> Nothing
+
+eliminateVar :: Term -> Term -> [(Term, Term)] -> Maybe [(Term, Term)]
+eliminateVar var term rest = case S.member var (fvt term) of
+  True -> Nothing
+  False -> liftM ((:) (var, term)) $ martelliMontanari $ applyToAll (var, term) rest
+
+applyToAll :: (Term, Term) -> [(Term, Term)] -> [(Term, Term)]
+applyToAll sub toUnify = L.map applyToPair toUnify
+  where
+    applyToPair (x, y) = (applyUnifier uni x, applyUnifier uni y)
+    uni = unifier [sub]
diff --git a/src/Folly/Utils.hs b/src/Folly/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Folly/Utils.hs
@@ -0,0 +1,23 @@
+module Folly.Utils(
+  Name,
+  Error(..), extractValue) where
+
+type Name = String
+
+data Error a =
+  Succeeded a |
+  Failed String
+  deriving (Show)
+
+instance Monad Error where
+  return a = Succeeded a
+  (Succeeded a) >>= f = f a
+  (Failed errMsg) >>= f = (Failed errMsg)
+
+instance Eq a => Eq (Error a) where
+  (==) (Succeeded v1) (Succeeded v2) = v1 == v2
+  (==) _ _ = False
+
+extractValue :: Error a -> a
+extractValue (Succeeded val) = val
+extractValue (Failed errMsg) = error $ "Computation Failed: " ++ errMsg
diff --git a/src/Main.hs b/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Main.hs
@@ -0,0 +1,25 @@
+module Main(main) where
+
+import System.Environment
+import System.IO
+
+import Folly.Lexer
+import Folly.Parser
+import Folly.Formula
+import Folly.Resolution
+import Folly.Theorem
+import Folly.Utils
+
+main :: IO ()
+main = do
+  (fileName:rest) <- getArgs
+  fHandle <- openFile fileName ReadMode
+  thmString <- hGetContents fHandle
+  let thm = processTheoremFile thmString
+  case thm of
+    Failed errMsg -> putStrLn errMsg
+    Succeeded t -> do
+      putStr $ show t
+      putStrLn $ "\n\nis " ++ (show $ isValid t)
+
+processTheoremFile thmFileContents = (lexer thmFileContents) >>= parseTheorem