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:
+
+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 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 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/Proper.cabal b/Proper.cabal
new file mode 100644
--- /dev/null
+++ b/Proper.cabal
@@ -0,0 +1,32 @@
+-- Initial Proper.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                Proper
+version:             0.1.0.0
+synopsis:	     An implementation of propositional logic in Haskell            
+-- description:         
+license:  		BSD3           
+license-file:        LICENSE
+-- author:              
+-- maintainer:          
+-- copyright:           
+-- category:            
+build-type:          Simple
+cabal-version:       >=1.8
+
+library
+  hs-source-dirs:	src
+  build-depends:	base==4.5.*, containers
+  exposed-modules:	Proper.Sentence, Proper.CNF, Proper.Clause
+
+executable Proper
+  main-is:             Main.hs
+  -- other-modules:       
+  build-depends:       base ==4.5.*, containers, parsec
+  hs-source-dirs:      src
+
+executable Proper-tests
+  main-is:             Main.hs
+  -- other-modules:       
+  build-depends:       base ==4.5.*, HUnit, containers, parsec
+  hs-source-dirs:      test, src
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/Main.hs b/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Main.hs
@@ -0,0 +1,23 @@
+module Main(main) where
+
+import System.Environment
+import Proper.Lexer
+import Proper.Parser
+import Proper.Sentence
+import System.IO
+import Proper.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 $ checkTheorem t)
+  
+processTheoremFile thmFileContents =
+  (toTokens thmFileContents >>= parseTheoremToks)
diff --git a/src/Proper/CNF.hs b/src/Proper/CNF.hs
new file mode 100644
--- /dev/null
+++ b/src/Proper/CNF.hs
@@ -0,0 +1,52 @@
+module Proper.CNF(
+  CNF, cnf, mergeCNFFormulas,
+  naiveSAT)
+       where
+
+import Data.Map as M
+import Data.Set as S
+import Proper.Clause
+import Proper.Utils
+
+type CNF = Set Clause
+  
+cnf :: [Clause] -> CNF
+cnf clauses = S.fromList clauses
+
+mergeCNFFormulas :: [CNF] -> CNF
+mergeCNFFormulas formulas = S.foldl S.union S.empty (S.fromList formulas)
+
+literals :: CNF -> Set Atom
+literals formula = S.foldl S.union S.empty (S.map (S.map literal) formula)
+
+naiveSAT :: CNF -> Bool
+naiveSAT formula = nSat simplifiedFormula allLits
+  where
+    simplifiedFormula = unitClauseSimplify formula
+    allLits = literals simplifiedFormula
+    
+nSat :: CNF -> Set Atom -> Bool
+nSat formula lits = case S.member S.empty formula of
+  True -> False
+  False -> case S.size formula of
+    0 -> True
+    _ -> (nSat nextFormula nextLits) || (nSat nextFormulaNeg nextLits)
+    where
+      nextLit = S.findMin lits
+      nextLits = S.delete nextLit lits
+      unitClause = clause [nextLit]
+      unitNegClause = clause [negation nextLit]
+      nextFormula = unitClauseSimplify (S.insert unitClause formula)
+      nextFormulaNeg = unitClauseSimplify (S.insert unitNegClause formula)
+
+unitClauseSimplify :: CNF -> CNF
+unitClauseSimplify formula = S.foldl removeUnitClause formula unitClauses
+  where
+    unitClauses = S.filter (\s -> S.size s == 1) formula
+
+removeUnitClause :: CNF -> Clause -> CNF
+removeUnitClause formula c = remainingClauses
+  where
+    elemC = S.findMin c
+    removeNegC = S.map (S.delete (negation elemC)) formula
+    remainingClauses = S.filter (\s -> (not $ S.member elemC s)) removeNegC
diff --git a/src/Proper/Clause.hs b/src/Proper/Clause.hs
new file mode 100644
--- /dev/null
+++ b/src/Proper/Clause.hs
@@ -0,0 +1,31 @@
+module Proper.Clause(
+  Atom, negation, lit, nLit, literal,
+  Clause, clause, concatClause) where
+
+import Data.Set as S
+
+import Proper.Utils
+
+data Atom =
+  Lit Name |
+  NLit Name
+  deriving (Eq, Ord, Show)
+  
+negation :: Atom -> Atom
+negation (Lit n) = NLit n
+negation (NLit n) = Lit n
+
+literal :: Atom -> Atom
+literal (Lit n) = Lit n
+literal (NLit n) = Lit n
+
+lit name = Lit name
+nLit name = NLit name
+
+type Clause = Set Atom
+
+concatClause :: Clause -> Clause -> Clause
+concatClause c1 c2 = S.union c1 c2
+
+clause :: [Atom] -> Clause
+clause atoms = S.fromList atoms
diff --git a/src/Proper/Sentence.hs b/src/Proper/Sentence.hs
new file mode 100644
--- /dev/null
+++ b/src/Proper/Sentence.hs
@@ -0,0 +1,203 @@
+module Proper.Sentence(
+  Sentence, checkTheorem,
+  neg, con, dis, val, bic, imp,
+  truthAssignment,
+  evalSentence,
+  isValidByTruthTable,
+  toCNF, theorem) where
+
+import Data.Map as M
+
+import Proper.Clause
+import Proper.CNF
+import Proper.Utils
+
+data Sentence =
+  Val Name              |
+  Neg Sentence          |
+  Con Sentence Sentence |
+  Dis Sentence Sentence |
+  Bic Sentence Sentence |
+  Imp Sentence Sentence
+  deriving (Eq, Ord)
+
+instance Show Sentence where
+  show = showSent
+  
+showSent :: Sentence -> String
+showSent (Val name) = name
+showSent (Neg s) = "~(" ++ show s ++ ")"
+showSent (Con s1 s2) = "(" ++ show s1 ++ " & " ++ show s2 ++ ")"
+showSent (Dis s1 s2) = "(" ++ show s1 ++ " | " ++ show s2 ++ ")"
+showSent (Bic s1 s2) = "(" ++ show s1 ++ " <-> " ++ show s2 ++ ")"
+showSent (Imp s1 s2) = "(" ++ show s1 ++ " -> " ++ show s2 ++ ")"
+           
+neg sent = Neg sent
+con s1 s2 = Con s1 s2
+dis s1 s2 = Dis s1 s2
+bic s1 s2 = Bic s1 s2
+imp s1 s2 = Imp s1 s2
+val name = Val name
+
+constants :: Sentence -> [Sentence]
+constants (Val n) = [(Val n)]
+constants (Neg s) = constants s
+constants (Con s1 s2) = constants s1 ++ constants s2
+constants (Dis s1 s2) = constants s1 ++ constants s2
+constants (Bic s1 s2) = constants s1 ++ constants s2
+constants (Imp s1 s2) = constants s1 ++ constants s2
+
+type TruthAssignment = Map Sentence Bool
+
+truthVal :: Sentence -> TruthAssignment -> Bool
+truthVal s tt = case M.lookup s tt of
+  Just val -> val
+  Nothing -> error $ "Sentence not in truth table " ++ show s
+
+truthAssignment :: [Name] -> [Bool] -> TruthAssignment
+truthAssignment constNames constVals = M.fromList $ zip consts constVals
+  where
+    consts = Prelude.map val constNames
+
+evalSentence :: TruthAssignment -> Sentence -> Bool
+evalSentence a (Neg s) = not $ evalSentence a s
+evalSentence a (Con s1 s2) = (evalSentence a s1) && (evalSentence a s2)
+evalSentence a (Dis s1 s2) = (evalSentence a s1) || (evalSentence a s2)
+evalSentence a (Imp s1 s2) = (not s1Eval) || s2Eval
+  where
+    s1Eval = evalSentence a s1
+    s2Eval = evalSentence a s2
+evalSentence a (Bic s1 s2) = (s1Eval && s2Eval) || ((not s1Eval) && (not s2Eval))
+  where
+    s1Eval = evalSentence a s1
+    s2Eval = evalSentence a s2
+evalSentence a constant = truthVal constant a
+  
+type TruthTable = [TruthAssignment]
+
+containsSentence :: Sentence -> TruthTable -> Bool
+containsSentence s [] = False
+containsSentence s tt = M.member s (head tt)
+
+truthTable :: [Sentence] -> TruthTable
+truthTable sents = Prelude.foldl addSentence [] sents
+
+addSentence :: TruthTable -> Sentence -> TruthTable
+addSentence tt s = if (containsSentence s tt)
+  then tt
+  else addNewSentence tt s
+
+addNewSentence :: TruthTable -> Sentence -> TruthTable
+addNewSentence [] c@(Val n) = [truthAssignment [n] [True], truthAssignment [n] [False]]
+addNewSentence tt c@(Val n) = ttFalse ++ ttTrue
+ where
+   ttFalse = Prelude.map (\ta -> M.insert c False ta) tt
+   ttTrue = Prelude.map (\ta -> M.insert c True ta) tt
+addNewSentence tt s = Prelude.map (addCompoundSentence s) tt
+
+addCompoundSentence :: Sentence -> TruthAssignment -> TruthAssignment
+addCompoundSentence s ta = insert s sval ta
+  where
+    sval = evalSentence ta s
+
+truthTableForSentence :: Sentence -> TruthTable
+truthTableForSentence s = truthTable $ (constants s) ++ [s]
+                          
+isValidByTruthTable :: Sentence -> Bool
+isValidByTruthTable s = and sTruthVals
+  where
+    sTruthTable = truthTableForSentence s
+    sTruthVals = Prelude.map (truthVal s) sTruthTable
+    
+-- Format conversion functions
+toCNF :: Sentence -> CNF
+toCNF = cnf .
+        cnfClauses .
+        distributeDisjunction .
+        pushNegation .
+        removeImplication .
+        removeBiconditional
+
+cnfClauses :: Sentence -> [Clause]
+cnfClauses (Con s1 s2) = cnfClauses s1 ++ cnfClauses s2
+cnfClauses s = [disjunctiveClause s]
+
+disjunctiveClause :: Sentence -> Clause
+disjunctiveClause (Dis s1 s2) = concatClause (disjunctiveClause s1) (disjunctiveClause s2)
+disjunctiveClause (Val name) = clause [lit name]
+disjunctiveClause (Neg (Val name)) = clause [nLit name]
+disjunctiveClause s = error $ "Disjunctive clause contains " ++ show s
+
+removeImplication :: Sentence -> Sentence
+removeImplication (Neg s) = Neg $ removeImplication s
+removeImplication (Con s1 s2) = Con (removeImplication s1) (removeImplication s2)
+removeImplication (Dis s1 s2) = Dis (removeImplication s1) (removeImplication s2)
+removeImplication (Imp s1 s2) = Dis (Neg p) q
+  where
+    p = removeImplication s1
+    q = removeImplication s2
+removeImplication s = s
+
+removeBiconditional :: Sentence -> Sentence
+removeBiconditional (Neg s) = Neg $ removeBiconditional s
+removeBiconditional (Con s1 s2) = Con (removeBiconditional s1) (removeBiconditional s2)
+removeBiconditional (Dis s1 s2) = Dis (removeBiconditional s1) (removeBiconditional s2)
+removeBiconditional (Imp s1 s2) = Imp (removeBiconditional s1) (removeBiconditional s2)
+removeBiconditional (Bic s1 s2) = Con noBic1 noBic2
+  where
+    noBic1 = Imp p q
+    noBic2 = Imp q p
+    p = removeBiconditional s1
+    q = removeBiconditional s2
+removeBiconditional (Val name) = (Val name)
+
+pushNegation :: Sentence -> Sentence
+pushNegation (Neg (Neg s)) = pushNegation s
+pushNegation (Neg (Con s1 s2)) = Dis (pushNegation (Neg s1)) (pushNegation (Neg s2))
+pushNegation (Neg (Dis s1 s2)) = Con (pushNegation (Neg s1)) (pushNegation (Neg s2))
+pushNegation (Con s1 s2) = Con (pushNegation s1) (pushNegation s2)
+pushNegation (Dis s1 s2) = Dis (pushNegation s1) (pushNegation s2)
+pushNegation s = s
+
+distributeDisjunction :: Sentence -> Sentence
+distributeDisjunction (Con p q) = Con (distributeDisjunction p) (distributeDisjunction q)
+distributeDisjunction (Dis p (Con q r)) = Con pdq pdr
+ where
+   pdq = distributeDisjunction $ Dis p q
+   pdr = distributeDisjunction $ Dis p r
+distributeDisjunction (Dis (Con p q) r) = Con pdr qdr
+ where
+   pdr = distributeDisjunction $ Dis p r
+   qdr = distributeDisjunction $ Dis q r
+distributeDisjunction (Dis p q) = case pd of
+  (Con r s) -> distributeDisjunction (Dis pd qd)
+  other -> case qd of
+    (Con r s) -> distributeDisjunction (Dis pd qd)
+    other -> Dis pd qd
+  where
+    pd = distributeDisjunction p
+    qd = distributeDisjunction q
+distributeDisjunction s = s
+
+-- Theorem code
+data Theorem = Thm [Sentence] Sentence
+               deriving (Eq)
+                        
+instance Show Theorem where
+  show = showThm
+  
+showThm :: Theorem -> String
+showThm (Thm axioms hyp) = "THEOREM\n" ++ axiomStr ++ "\n|=\n\n" ++ hypString
+  where
+    axiomStr = Prelude.concat $ Prelude.map (\a -> (show a) ++ "\n") axioms
+    hypString = show hyp
+
+theorem :: [Sentence] -> Sentence -> Theorem
+theorem axioms hypothesis = Thm axioms hypothesis
+
+checkTheorem :: Theorem -> Bool
+checkTheorem (Thm axioms hypothesis) = not $ naiveSAT cnfFormNegThm
+  where
+    cnfAxioms = Prelude.map toCNF axioms
+    cnfNotHypothesis = toCNF (neg hypothesis)
+    cnfFormNegThm = mergeCNFFormulas (cnfNotHypothesis:cnfAxioms)
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,12 @@
+module Main(main) where
+
+import Proper.CNFTests
+import Proper.LexerTests
+import Proper.ParserTests
+import Proper.SentenceTests
+
+main = do
+  allSentenceTests
+  allCNFTests
+  allLexerTests
+  allParserTests