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.1
+version:             0.1.4.2
 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
@@ -20,8 +20,7 @@
 cabal-version:       >=1.8
 
 library
-  exposed-modules:     Folly.Formula, Folly.Unification, Folly.Resolution, Folly.Utils
-  -- other-modules:       
+  exposed-modules:     Folly.Formula, Folly.Unification, Folly.Resolution, Folly.Utils, Folly.Theorem, Folly.Lexer, Folly.Parser
   build-depends:       base < 6, containers
   hs-source-dirs:      src
 
diff --git a/src/Folly/Lexer.hs b/src/Folly/Lexer.hs
new file mode 100644
--- /dev/null
+++ b/src/Folly/Lexer.hs
@@ -0,0 +1,116 @@
+module Folly.Lexer(
+  Token, name, isVar, isPred, pos,
+  testOp, testVar, testQuant,
+  testPred, testSep,
+  lexer) where
+
+import Text.Parsec.Pos
+import Text.ParserCombinators.Parsec
+import Folly.Utils
+
+data Token = 
+  Var String SourcePos   |
+  Pred String SourcePos  |
+  Sep String SourcePos   |
+  Op String SourcePos    |
+  Quant String SourcePos |
+  Res String SourcePos
+
+instance Show Token where
+  show = showTok
+                      
+instance Eq Token where
+  (==) = tokEqual
+  
+isVar (Var _ _) = True
+isVar _ = False
+
+isPred (Pred _ _) = True
+isPred _ = False
+
+name (Var n _) = n
+name (Pred n _) = n
+name (Sep n _) = n
+name (Op n _) = n
+name (Res n _) = n
+name (Quant n _) = n
+
+pos (Var _ p) = p
+pos (Pred _ p) = p
+pos (Sep _ p) = p
+pos (Op _ p) = p
+pos (Res _ p) = p
+pos (Quant _ p) = p
+
+testVar s = Var s (newPos "DUMMY" 0 0)
+testPred s = Pred s (newPos "DUMMY" 0 0)
+testSep s = Sep s (newPos "DUMMY" 0 0)
+testOp s = Sep s (newPos "DUMMY" 0 0)
+testRes s = Res s (newPos "DUMMY" 0 0)
+testQuant s = Quant s (newPos "DUMMY" 0 0)
+
+showTok :: Token -> String
+showTok t = name t
+
+tokEqual :: Token -> Token -> Bool
+tokEqual t1 t2 = name t1 == name t2
+
+lexer :: String -> Error [Token]
+lexer str = case parse parseToks "LEXER" str of
+  Left err -> Failed $ show err
+  Right toks -> Succeeded $ toks
+
+parseToks = endBy parseTok spaces
+
+parseTok = try atomicLit
+         <|> try reservedWord
+         <|> try predicate
+         <|> try separator
+         <|> try quantifier
+         <|> operator
+
+predicate = do
+  pos <- getPosition
+  firstChar <- upper <|> specialChar
+  case firstChar of
+    'E' -> eOrQPred 'E' pos
+    'Q' -> eOrQPred 'Q' pos
+    _ -> nonEQPred firstChar pos
+
+eOrQPred firstChar pos = do
+  rest <- many1 bodyChar
+  return $ Pred (firstChar:rest) pos
+
+nonEQPred firstChar pos = do
+  rest <- many bodyChar
+  return $ Pred (firstChar:rest) pos
+  
+atomicLit = do
+  pos <- getPosition
+  firstChar <- lower
+  rest <- many bodyChar
+  return $ Var (firstChar:rest) pos
+  
+reservedWord = do
+  pos <- getPosition
+  name <- try (string "HYPOTHESIS:") <|> (string "CONCLUSION:")
+  return $ Res name pos
+
+separator = do
+  pos <- getPosition
+  name <- choice $ map string ["(", ")", "]", "[", ",", "."]
+  return $ Sep name pos
+
+operator = do
+  pos <- getPosition
+  name <- choice $ map string ["~", "|", "&", "<->", "->"]
+  return $ Op name pos
+
+quantifier = do
+  pos <- getPosition
+  name <- choice $ map string ["E", "Q"]
+  return $ Quant name pos
+
+bodyChar = alphaNum <|> specialChar
+
+specialChar = oneOf "!@#$%*<>?+=-_"
diff --git a/src/Folly/Parser.hs b/src/Folly/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Folly/Parser.hs
@@ -0,0 +1,156 @@
+module Folly.Parser(
+  parseFormula,
+  parseTheorem) where
+
+import Text.Parsec.Combinator
+import Text.Parsec.Expr
+import Text.Parsec.Pos
+import Text.Parsec.Prim
+
+import Folly.Formula
+import Folly.Lexer as Lex
+import Folly.Theorem
+import Folly.Utils
+
+parseTheorem :: [Token] -> Error Theorem
+parseTheorem toks = case parse parseTheoremToks "PARSER" toks of
+  Left err -> Failed $ show err
+  Right thm -> Succeeded thm
+
+parseTheoremToks = do
+  axioms <- parseHypothesis
+  hypothesis <- parseConclusion
+  return $ theorem axioms hypothesis
+  
+parseConclusion = do
+  propTok "CONCLUSION:"
+  axioms <- parseForm
+  return axioms
+  
+parseHypothesis = do
+  propTok "HYPOTHESIS:"
+  hypothesis <- many parseForm
+  return hypothesis
+
+parseFormula :: [Token] -> Error (Formula)
+parseFormula toks = case parse parseForm "PARSER" toks of
+  Left err -> Failed $ show err
+  Right formula -> Succeeded formula
+
+parseForm = buildExpressionParser table parseFactor
+
+parseFactor = try (parseParens parseForm)
+             <|> try parsePredicate
+             <|> parseQuantification
+
+table =
+  [[negation],
+   [conjunction],
+   [disjunction],
+   [implication],
+   [bicondition]]
+
+negation = Prefix parseNeg
+conjunction = Infix parseCon AssocRight
+disjunction = Infix parseDis AssocRight
+implication = Infix parseImp AssocRight
+bicondition = Infix parseBic AssocRight
+--quantification = Prefix parseQuant
+
+parseParens e = do
+  propTok "("
+  expr <- e
+  propTok ")"
+  return expr
+
+parseQuantification = do
+  quantType <- propTok "V" <|> propTok "E"
+  varName <- varTok
+  propTok "."
+  form <- parseForm
+  case (name quantType) of
+    "V" -> return $ fa (var (name varName)) form
+    "E" -> return $ te (var (name varName)) form
+    _ -> error $ show quantType ++ " is not a quantifier"
+
+parseNeg :: (Monad m) => ParsecT [Token] u m (Formula -> Formula)
+parseNeg = do
+  propTok "~"
+  return $ neg
+  
+parseCon = do
+  propTok "&"
+  return $ con
+  
+parseDis = do
+  propTok "|"
+  return $ dis
+  
+parseImp = do
+  propTok "->"
+  return $ imp
+  
+parseBic = do
+  propTok "<->"
+  return $ bic
+
+parsePredicate :: (Monad m) => ParsecT [Token] u m (Formula)
+parsePredicate = do
+  nameTok <- predicateTok
+  propTok "["
+  terms <- sepBy parseTerm (propTok ",")
+  propTok "]"
+  return $ pr (name nameTok) terms
+
+parseTerm :: (Monad m) => ParsecT [Token] u m Term
+parseTerm = try parseConstant <|> try parseFunc <|> parseVar
+
+parseConstant :: (Monad m) => ParsecT [Token] u m Term
+parseConstant = do
+  nameTok <- predicateTok
+  return $ constant (name nameTok)
+
+parseVar :: (Monad m) => ParsecT [Token] u m Term
+parseVar = do
+  nameTok <- varTok
+  return $ var (name nameTok)
+
+parseFunc :: (Monad m) => ParsecT [Token] u m Term
+parseFunc = do
+  nameTok <- varTok
+  propTok "("
+  args <- sepBy parseTerm (propTok ",")
+  propTok ")"
+  return $ func (name nameTok) args
+
+propTok :: (Monad m) => String -> ParsecT [Token] u m Token
+propTok str = tokenPrim show updatePos hasNameStr
+  where
+    hasNameStr t = if (name t) == str then Just t else Nothing
+
+predicateTok :: (Monad m) => ParsecT [Token] u m Token
+predicateTok = tokenPrim show updatePos isPred
+  where
+    isPred t = if (Lex.isPred t) then Just t else Nothing
+
+varTok :: (Monad m) => ParsecT [Token] u m Token
+varTok = tokenPrim show updatePos isPred
+  where
+    isPred t = if (Lex.isVar t) then Just t else Nothing
+
+literalTok :: (Monad m) => ParsecT [Token] u m Token
+literalTok = tokenPrim show updatePos isLit
+  where
+    isLit t = if (Lex.isVar t) then Just t else Nothing
+
+axiomsTok c = tokenPrim show updatePos isAxiom
+  where
+    isAxiom t = if (name t) == "AXIOMS:" then Just t else Nothing
+
+hypothesisTok c = tokenPrim show updatePos isAxiom
+  where
+    isAxiom t = if (name t) == "HYPOTHESIS:" then Just t else Nothing
+
+updatePos :: SourcePos -> Token -> [Token] -> SourcePos
+updatePos _ _ (pt:_) = pos pt
+updatePos position _ [] = position
diff --git a/src/Folly/Theorem.hs b/src/Folly/Theorem.hs
new file mode 100644
--- /dev/null
+++ b/src/Folly/Theorem.hs
@@ -0,0 +1,29 @@
+module Folly.Theorem(
+  Theorem,
+  theorem,
+  hypothesis,
+  conclusion) where
+
+import Data.List as L
+
+import Folly.Formula
+
+data Theorem = Theorem [Formula] (Formula)
+               deriving (Eq, Ord)
+
+instance Show Theorem where
+  show = showThm
+
+showThm :: Theorem -> String
+showThm (Theorem h c) = "Hypothesis:\n" ++ hypStr ++ "\n\n|=\n\n" ++ conclStr
+  where
+    hypStr = (L.concat $ L.intersperse "\n" $ L.map show h)
+    conclStr = "Conclusion:\n" ++ show c
+
+theorem = Theorem
+
+hypothesis :: Theorem -> [Formula]
+hypothesis (Theorem hp _) = hp
+
+conclusion :: Theorem -> Formula
+conclusion (Theorem _ c) = c