diff --git a/Folly.cabal b/Folly.cabal
--- a/Folly.cabal
+++ b/Folly.cabal
@@ -2,7 +2,7 @@
 --  see http://haskell.org/cabal/users-guide/
 
 name:                Folly
-version:             0.1.4.3
+version:             0.1.4.4
 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
@@ -26,12 +26,12 @@
 
 executable Folly
   main-is:             Main.hs
-  -- other-modules:       
+  other-modules:       
   build-depends:       base < 6, containers, parsec
   hs-source-dirs:      src
 
 executable Folly-tests
   main-is:             Main.hs
-  -- other-modules:       
+  other-modules:       Folly.FormulaTests, Folly.LexerTests, Folly.ParserTests, Folly.ResolutionTests, Folly.UnificationTests
   build-depends:       base < 6, HUnit, containers, parsec
   hs-source-dirs:      test, src
diff --git a/test/Folly/FormulaTests.hs b/test/Folly/FormulaTests.hs
new file mode 100644
--- /dev/null
+++ b/test/Folly/FormulaTests.hs
@@ -0,0 +1,201 @@
+module Folly.FormulaTests(allFormulaTests) where
+
+import Data.Map as M
+import Data.Set as S
+import Folly.Formula
+import Folly.TestUtils
+
+allFormulaTests = do
+  testFVT
+  testVars
+  testFreeVars
+  testGeneralize
+  testSubTerm
+  testSubFormula
+  testToPNF
+  testToPNFPullQuants
+  testSkolemize
+  testToClausalForm
+  
+testFVT =
+  testFunction fvt fvtCases
+
+fvtCases :: [(Term, Set Term)]
+fvtCases =
+  [(var "a", S.fromList [var "a"]),
+   (func "+" [(var "x"), (var "y")], S.fromList [(var "x"), (var "y")]),
+   (func "*" [(var "x"), (func "-" [(var "y"), (var "z")])],
+    S.fromList [var "x", var "y", var "z"]),
+   (constant "1", S.empty)]
+  
+testVars =
+  testFunction vars varsCases
+
+varsCases :: [(Formula, Set Term)]
+varsCases =
+  [(t, S.empty),
+   (f, S.empty),
+   (pr "<" [(var "a"), (var "b")], S.fromList [(var "a"), (var "b")]),
+   (imp (pr ">" [(var "c")]) (pr "<" [(var "d"), (var "e")]),
+    S.fromList [(var "c"), (var "d"), (var "e")]),
+   (neg (pr "isReal" [(var "i")]), S.fromList [(var "i")]),
+   (te (var "x") (pr "=" [(var "k"), (var "j")]),
+    S.fromList [(var "x"), (var "k"), (var "j")])]
+  
+testFreeVars =
+  testFunction freeVars freeVarCases
+
+freeVarCases :: [(Formula, Set Term)]
+freeVarCases =
+  [(t, S.empty),
+   (f, S.empty),
+   (pr "<" [(var "a"), (var "b")], S.fromList [(var "a"), (var "b")]),
+   (imp (pr ">" [(var "c")]) (pr "<" [(var "d"), (var "e")]),
+    S.fromList [(var "c"), (var "d"), (var "e")]),
+   (neg (pr "isReal" [(var "i")]), S.fromList [(var "i")]),
+   (te (var "x") (pr "=" [(var "x")]), S.empty)]
+
+testGeneralize =
+  testFunction generalize generalizeCases
+
+generalizeCases :: [(Formula, Formula)]
+generalizeCases =
+  [(t, t),
+   (f, f),
+   (pr "!" [var "x"], (fa (var "x") (pr "!" [var "x"]))),
+   (fa (var "y") (pr "is" [var "x", var "y"]),
+    fa (var "x") (fa (var "y") (pr "is" [var "x", var "y"]))),
+   (te (var "k") (pr "no" [var "l", var "k", var "s"]),
+    (fa (var "s") (fa (var "l") (te (var "k") (pr "no" [var "l", var "k", var "s"])))))]
+  
+testSubTerm =
+  testFunction (subTerm testSub) subTermCases
+
+testSub :: Map Term Term
+testSub = M.fromList
+          [(var "x", func "+" [var "a", var "b"]),
+           (var "k", func "*" [var "c", var "d"])]
+
+subTermCases :: [(Term, Term)]
+subTermCases =
+  [(constant "o", constant "o"),
+   (var "x", func "+" [var "a", var "b"]),
+   (func "su" [var "x", var "l"],
+    func "su" [func "+" [var "a", var "b"], var "l"]),
+   (func "op" [func "op" [var "k", var "x"]],
+    func "op" [func "op"
+               [func "*" [var "c", var "d"],
+                func "+" [var "a", var "b"]]])]
+  
+testSubFormula =
+  testFunction (subFormula testFormSub) subFormulaCases
+
+testFormSub = M.fromList
+              [(var "x", var "a"), (var "y", var "l")]
+
+subFormulaCases :: [(Formula, Formula)]
+subFormulaCases =
+  [(t, t),
+   (f, f),
+   (pr "a" [var "x"], pr "a" [var "a"]),
+   (imp (pr "xo" [var "x"]) (pr "d" [var "y"]),
+    imp (pr "xo" [var "a"]) (pr "d" [var "l"])),
+   (neg (pr "isX" [var "x"]), neg (pr "isX" [var "a"])),
+   (fa (var "q") (pr "isK" [var "x", constant "p"]),
+    fa (var "q") (pr "isK" [var "a", constant "p"])),
+   (te (var "a") (pr "gotcha" [var "x", var "a"]),
+    te (var "a'") (pr "gotcha" [var "a", var "a'"])),
+   (fa (var "a") (te (var "a'") (pr "=" [var "x", var "a'"])),
+    fa (var "a'") (te (var "a''") (pr "=" [var "a", var "a''"])))]
+  
+testToPNF =
+  testFunction toPNF pnfCases
+
+pnfCases :: [(Formula, Formula)]
+pnfCases =
+  [(t, t),
+   (f, f),
+   (imp (pr "a" [var "z"]) (pr "b" [var "z"]),
+    dis (neg (pr "a" [var "z"])) (pr "b" [var "z"])),
+   (bic (pr "d" [var "z"]) (pr "o" [var "k"]),
+    con (dis (neg (pr "d" [var "z"])) (pr "o" [var "k"]))
+        (dis (neg (pr "o" [var "k"])) (pr "d" [var "z"]))),
+   (fa (var "x") (pr "d" [var "k", var "l"]),
+    pr "d" [var "k", var "l"]),
+   (fa (var "x") (te (var "d") (pr "i" [var "x", var "y"])),
+    fa (var "x") (pr "i" [var "x", var "y"])),
+   (neg (con (pr "a" [var "d"]) (pr "k" [var "l"])),
+    dis (neg (pr "a" [var "d"])) (neg (pr "k" [var "l"]))),
+   (neg (neg (dis (pr "a" [var "z"]) (pr "d" [var "k"]))),
+    dis (pr "a" [var "z"]) (pr "d" [var "k"])),
+   (neg (con (dis (pr "d" [var "x"]) (pr "e" [var "p"])) (pr "p" [var "w"])),
+    dis (con (neg (pr "d" [var "x"])) (neg (pr "e" [var "p"]))) (neg (pr "p" [var "w"]))),
+   (neg (fa (var "x") (pr "e" [var "x"])), te (var "x") (neg (pr "e" [var "x"]))),
+   (neg (te (var "i") (pr "ds" [var "i"])), fa (var "i") (neg (pr "ds" [var "i"]))),
+   (neg (con t f), t),
+   (neg (neg (pr "d" [var "k"])), pr "d" [var "k"]),
+   (dis f t, t),
+   (dis f f, f),
+   (con f t, f),
+   (con t f, f),
+   (con t t, t),
+   (neg (neg (neg (pr "d" [var "o"]))), neg (pr "d" [var "o"])),
+   (dis (neg (con (pr "Dog" [var "x"]) (pr "Owns" [var "y", var "x"]))) (pr "LovesAnimals" [var "y"]), (dis (dis (neg (pr "Dog" [var "x"])) (neg (pr "Owns" [var "y", var "x"]))) (pr "LovesAnimals" [var "y"])))]
+  
+testToPNFPullQuants =
+  testFunction toPNF pullQuantsCases
+
+pullQuantsCases :: [(Formula, Formula)]
+pullQuantsCases =
+  [(con (fa (var "x") (pr "d" [var "x"])) (fa (var "y") (pr "k" [var "y"])),
+    fa (var "x") (con (pr "d" [var "x"]) (pr "k" [var "x"]))),
+   (dis (te (var "k") (pr "d" [var "k"])) (te (var "j") (pr "i" [var "j"])),
+    te (var "k") (dis (pr "d" [var "k"]) (pr "i" [var "k"]))),
+   (dis (fa (var "k") (pr "d" [var "k"])) (pr "j" [var "k"]),
+    fa (var "k'") (dis (pr "d" [var "k'"]) (pr "j" [var "k"]))),
+   (dis (pr "d" [var "l"]) (fa (var "k") (pr "lj" [var "k"])),
+    fa (var "k") (dis (pr "d" [var "l"]) (pr "lj" [var "k"]))),
+   (dis (te (var "k") (pr "d" [var "k"])) (pr "j" [var "k"]),
+    te (var "k'") (dis (pr "d" [var "k'"]) (pr "j" [var "k"]))),
+   (dis (pr "d" [var "l"]) (te (var "k") (pr "lj" [var "k"])),
+    te (var "k") (dis (pr "d" [var "l"]) (pr "lj" [var "k"]))),
+   (con (fa (var "k") (pr "d" [var "k"])) (pr "j" [var "k"]),
+    fa (var "k'") (con (pr "d" [var "k'"]) (pr "j" [var "k"]))),
+   (con (pr "d" [var "l"]) (fa (var "k") (pr "lj" [var "k"])),
+    fa (var "k") (con (pr "d" [var "l"]) (pr "lj" [var "k"]))),
+   (con (te (var "k") (pr "d" [var "k"])) (pr "j" [var "k"]),
+    te (var "k'") (con (pr "d" [var "k'"]) (pr "j" [var "k"]))),
+   (con (pr "d" [var "l"]) (te (var "k") (pr "lj" [var "k"])),
+    te (var "k") (con (pr "d" [var "l"]) (pr "lj" [var "k"]))),
+   (con (con (fa (var "x") (pr "d" [var "x"])) (pr "i" [var "x"])) (pr "d" [var "k"]),
+    fa (var "x'") (con (con (pr "d" [var "x'"]) (pr "i" [var "x"])) (pr "d" [var "k"])))]
+  
+testSkolemize =
+  testFunction toSkolemForm skolemizeCases
+
+skolemizeCases :: [(Formula, Formula)]
+skolemizeCases =
+  [(pr "d" [var "a"], pr "d" [var "a"]),
+   (te (var "x") (pr "d" [var "x"]), pr "d" [skf 0 []]),
+   (te (var "x") (fa (var "y") (pr "d" [var "x", var "y"])),
+    fa (var "y") (pr "d" [skf 0 [], var "y"])),
+   (fa (var "k") (te (var "l") (te (var "m") (pr "i" [var "l", var "m", var "k"]))),
+    fa (var "k") (pr "i" [skf 0 [var "k"], skf 1 [var "k"], var "k"])),
+   (fa (var "a") (te (var "b") (fa (var "c") (pr "l" [var "b", var "c", var "a"]))),
+    fa (var "a") (fa (var "c") (pr "l" [skf 0 [var "a"], var "c", var "a"]))),
+   (fa (var "a") (fa (var "b") (te (var "c") (pr "l" [var "a", var "c", var "b"]))),
+    fa (var "a") (fa (var "b") (pr "l" [var "a", skf 0 [var "b", var "a"], var "b"])))]
+
+testToClausalForm =
+  testFunction toClausalForm clausalFormCases
+
+clausalFormCases :: [(Formula, [[Formula]])]
+clausalFormCases =
+  [(pr "d" [var "no"], [[pr "d" [var "no"]]]),
+   (fa (var "x") (con (pr "a" [var "x"]) (pr "d" [constant "P"])),
+    [[pr "a" [var "x"]], [pr "d" [constant "P"]]]),
+   (dis (pr "a" [var "x"]) (pr "d" [var "c"]), [[pr "a" [var "x"], pr "d" [var "c"]]]),
+   (bic (pr "P" [var "x"]) (con (pr "Q" [var "y"]) (pr "R" [var "z"])),
+    [[neg (pr "P" [var "x"]), pr "Q" [var "y"]],
+     [neg (pr "P" [var "x"]), pr "R" [var "z"]],
+     [neg (pr "Q" [var "y"]), neg (pr "R" [var "z"]), pr "P" [var "x"]]])]
diff --git a/test/Folly/LexerTests.hs b/test/Folly/LexerTests.hs
new file mode 100644
--- /dev/null
+++ b/test/Folly/LexerTests.hs
@@ -0,0 +1,30 @@
+module Folly.LexerTests(allLexerTests) where
+
+import Folly.Lexer
+import Folly.TestUtils
+import Folly.Utils
+
+allLexerTests = do
+  testFunction lexer lexerCases
+
+lexerCases =
+  [("nooo", Succeeded $ [testVar "nooo"]),
+   ("(", Succeeded $ [testSep "("]),
+   (")", Succeeded $ [testSep ")"]),
+   ("[", Succeeded $ [testSep "["]),
+   ("]", Succeeded $ [testSep "]"]),
+   (",", Succeeded $ [testSep ","]),
+   (".", Succeeded $ [testSep "."]),
+   ("|", Succeeded $ [testOp "|"]),
+   ("&", Succeeded $ [testOp "&"]),
+   ("~", Succeeded $ [testOp "~"]),
+   ("->", Succeeded $ [testOp "->"]),
+   ("<->", Succeeded $ [testOp "<->"]),
+   ("E", Succeeded $ [testQuant "E"]),
+   ("Q", Succeeded $ [testQuant "Q"]),
+   ("=", Succeeded $ [testPred "="]),
+   ("Ever", Succeeded $ [testPred "Ever"]),
+   ("Quacks", Succeeded $ [testPred "Quacks"]),
+   ("N#%_Man", Succeeded $ [testPred "N#%_Man"]),
+   ("n#2@", Succeeded $ [testVar "n#2@"]),
+   ("V z . E k. F[z] -> G[k]", Succeeded $ [testPred "V", testVar "z", testSep ".", testPred "E", testVar "k", testSep ".", testPred "F", testSep "[", testVar "z", testSep "]", testOp "->", testPred "G", testSep "[", testVar "k", testSep "]"])]
diff --git a/test/Folly/ParserTests.hs b/test/Folly/ParserTests.hs
new file mode 100644
--- /dev/null
+++ b/test/Folly/ParserTests.hs
@@ -0,0 +1,25 @@
+module Folly.ParserTests(allParserTests) where
+
+import Folly.Formula
+import Folly.Lexer
+import Folly.Parser
+import Folly.TestUtils
+import Folly.Utils
+
+allParserTests = do
+  testFunction (\x -> ((>>=) x parseFormula)) (map (\ (x, y) -> (lexer x, y)) parseFormulaCases)
+
+parseFormulaCases :: [(String, Error Formula)]
+parseFormulaCases =
+  [("Dog[ a ]", Succeeded $ pr "Dog" [var "a"]),
+   ("~Super[ k, kill(a, b)]", Succeeded $ neg (pr "Super" [var "k", func "kill" [var "a", var "b"]])),
+   ("Dog[x] & Owns[John, x]", Succeeded $ con (pr "Dog" [var "x"]) (pr "Owns" [constant "John", var "x"])),
+   ("Dog [x] & (Owns[John, x] | Not[Cat, John])", Succeeded $ con (pr "Dog" [var "x"]) (dis (pr "Owns" [constant "John", var "x"]) (pr "Not" [constant "Cat", constant "John"]))),
+   ("Ex[p] | ~Ex[x]", Succeeded $ dis (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),
+   ("Ex[p] -> ~Ex[x]", Succeeded $ imp (pr "Ex" [var "p"]) (neg (pr "Ex" [var "x"]))),
+   ("Ex[p] <-> ~Vx[x]", Succeeded $ bic (pr "Ex" [var "p"]) (neg (pr "Vx" [var "x"]))),
+   ("V x . U#12[x]", Succeeded $ fa (var "x") (pr "U#12" [var "x"])),
+   ("E y . K[f(l, y, No)]", Succeeded $ te (var "y") (pr "K" [func "f" [var "l", var "y", constant "No"]])),
+   ("V z . E k. F[z] -> G[k]", Succeeded $ fa (var "z") (te (var "k") (imp (pr "F" [var "z"]) (pr "G" [var "k"])))),
+   ("E y. K[y] -> V x. Z[x, y]", Succeeded $ te (var "y") (imp (pr "K" [var "y"]) (fa (var "x") (pr "Z" [var "x", var "y"])))),
+   ("E y. K[y] -> Z[x, y]", Succeeded $ te (var "y") (imp (pr "K" [var "y"]) (pr "Z" [var "x", var "y"])))]
diff --git a/test/Folly/ResolutionTests.hs b/test/Folly/ResolutionTests.hs
new file mode 100644
--- /dev/null
+++ b/test/Folly/ResolutionTests.hs
@@ -0,0 +1,41 @@
+module Folly.ResolutionTests(allResolutionTests) where
+
+import Folly.Formula
+import Folly.Resolution
+import Folly.Theorem
+import Folly.TestUtils
+
+allResolutionTests = do
+  testIsValid
+
+testIsValid =
+  testFunction isValid isValidTestCases
+
+isValidTestCases :: [(Theorem, Bool)]
+isValidTestCases =
+  [(theorem [] (fa (var "a") (dis (pr "d" [var "a"]) (neg (pr "d" [var "a"])))), True),
+   (theorem [] (pr "d" [var "k"]), False),
+   (theorem [pr "Dog" [var "x"]] (pr "Dog" [var "x"]), True),
+   (theorem
+    [(fa (var "d") (imp (pr "Dog" [var "d"]) (pr "Loves" [constant "John", var "d"]))),
+     (pr "Dog" [constant "Fido"])]
+    (pr "Loves" [constant "John", constant "Fido"]), True),
+   (theorem
+    [(fa (var "p") (imp (te (var "d") (con (pr "Dog" [var "d"]) (pr "Owns" [var "p", var "d"]))) (pr "LovesAnimals" [var "p"]))),
+     (imp (pr "LovesAnimals" [var "x"]) (fa (var "a") (neg (pr "Kills" [var "x", var "a"])))),
+     (pr "Owns" [constant "John", constant "Fido"]),
+     (pr "Dog" [constant "Fido"])]
+    (fa (var "a") (neg (pr "Kills" [constant "John", var "a"]))), True),
+   (theorem groupWithEquals (imp (con (con (con (pr "=" [func "*" [var "x", var "y"], constant "1"]) (pr "=" [func "*" [var "y", var "x"], constant "1"])) (pr "=" [func "*" [var "x", var "z"], constant "1"])) (pr "=" [func "*" [var "z", var "x"], constant "1"])) (pr "=" [var "y", var "z"])), True),
+   (theorem groupWithEquals (imp (fa (var "x") (con (pr "=" [func "*" [var "x", var "z"], constant "1"]) (pr "=" [func "*" [var "z", var "x"], constant "1"]))) (pr "=" [var "z", constant "1"])), True)]
+
+equalityAxioms :: [Formula]
+equalityAxioms =
+  [(fa (var "x") (pr "=" [var "x", var "x"])),
+   (fa (var "x") (fa (var "y") (imp (pr "=" [var "x", var "y"]) (pr "=" [var "y", var "x"])))),
+   (fa (var "x") (fa (var "y") (fa (var "z") (imp (con (pr "=" [var "x", var "y"]) (pr "=" [var "y", var "z"])) (pr "=" [var "x", var "z"])))))]
+
+groupWithEquals =
+  [(fa (var "x") (te (var "y") (con (pr "=" [func "*" [var "x", var "y"], constant "1"]) (pr "=" [func "*" [var "y", var "x"], constant "1"])))),
+   (fa (var "x") (fa (var "y") (fa (var "z") (pr "=" [func "*" [var "x", func "*" [var "y", var "z"]], func "*" [func "*" [var "x", var "y"], var "z"]])))),
+   (fa (var "x") (con (pr "=" [func "*" [var "x", constant "1"], var "x"]) (pr "=" [func "*" [constant "1", var "x"], constant "x"])))] ++ equalityAxioms
diff --git a/test/Folly/UnificationTests.hs b/test/Folly/UnificationTests.hs
new file mode 100644
--- /dev/null
+++ b/test/Folly/UnificationTests.hs
@@ -0,0 +1,42 @@
+module Folly.UnificationTests(allUnificationTests) where
+
+import Folly.Formula
+import Folly.TestUtils
+import Folly.Unification
+
+allUnificationTests = do
+  testApplyUnifier
+  testMostGeneralUnifier
+
+simpleUnifier = unifier [(var "d", constant "Fido"),
+                         (var "n", constant "OOH-KILLEM"),
+                         (var "k", func "x" [(var "y")]),
+                         (var "y", var "n"),
+                         (var "q", var "uio")]
+
+testApplyUnifier =
+  testFunction (applyUnifier simpleUnifier) applyUnifierCases
+
+applyUnifierCases =
+  [(var "should-not-change", var "should-not-change"),
+   (var "q", var "uio"),
+   (var "d", constant "Fido"),
+   (var "k", func "x" [constant "OOH-KILLEM"]),
+   (func "nest" [var "k"], func "nest" [func "x" [constant "OOH-KILLEM"]])]
+
+testMostGeneralUnifier =
+  testFunction mostGeneralUnifier mguTestCases
+
+mguTestCases =
+  [([(var "x", var "x")], Just $ unifier []),
+   ([(var "x", var "y")], Just $ unifier [(var "x", var "y")]),
+   ([(var "x", var "z"), (constant "p", constant "dsf")], Nothing),
+   ([(var "x", func "d" [constant "x", func "k" [var "x"]])], Nothing),
+   ([(var "x", var "y"), (var "x", var "x"), (var "x", constant "K")],
+    Just $ unifier [(var "x", var "y"), (var "y", constant "K")]),
+   ([(func "g" [var "x2"], var "x1"),
+     (func "f" [var "x1", func "h" [var "x1"], var "x2"],
+      func "f" [func "g" [var "x3"], var "x4", var "x3"])],
+    Just $ unifier [(var "x2", var "x3"),
+                    (var "x1", func "g" [var "x2"]),
+                    (var "x4", func "h" [func "g" [var "x3"]])])]