diff --git a/Proper.cabal b/Proper.cabal
--- a/Proper.cabal
+++ b/Proper.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                Proper
-version:             0.4.2.0
+version:             0.5.2.0
 synopsis:	     An implementation of propositional logic in Haskell            
 description:         Proper is both an executable theorem prover for Propositional logic
 		     and a library for incorporating propositional logic into other Haskell
@@ -21,17 +21,17 @@
 
 library
   hs-source-dirs:	src
-  build-depends:	base==4.5.*, containers
-  exposed-modules:	Proper.Sentence, Proper.CNF, Proper.Clause, Proper.BDD
+  build-depends:	base < 6, containers, syb
+  exposed-modules:	Proper.Formula, Proper.CNF, Proper.Clause, Proper.BDD
 
 executable Proper
   main-is:             Main.hs
   -- other-modules:       
-  build-depends:       base ==4.5.*, containers, parsec
+  build-depends:       base < 6, containers, parsec, syb
   hs-source-dirs:      src
 
 executable Proper-tests
   main-is:             Main.hs
   -- other-modules:       
-  build-depends:       base ==4.5.*, HUnit, containers, parsec
+  build-depends:       base < 6, HUnit, containers, parsec, syb
   hs-source-dirs:      test, src
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -3,7 +3,7 @@
 import System.Environment
 import Proper.Lexer
 import Proper.Parser
-import Proper.Sentence
+import Proper.Formula
 import System.IO
 import Proper.Utils
 
diff --git a/src/Proper/CNF.hs b/src/Proper/CNF.hs
--- a/src/Proper/CNF.hs
+++ b/src/Proper/CNF.hs
@@ -1,13 +1,17 @@
 module Proper.CNF(
-  CNF, cnf, mergeCNFFormulas,
-  naiveSAT)
-       where
+  CNF, SatisfyingAssignment,
+  cnf, mergeCNFFormulas,
+  naiveSAT, naiveSATBool) where
 
+import Control.Monad
+import Data.Generics.Aliases
+import Data.List as L
 import Data.Map as M
 import Data.Set as S
 import Proper.Clause
 import Proper.Utils
 
+type SatisfyingAssignment l = Map l Bool
 type CNF c = Set (Clause c)
   
 cnf :: (Ord c) => [Clause c] -> CNF c
@@ -16,34 +20,55 @@
 mergeCNFFormulas :: (Ord c) => [CNF c] -> CNF c
 mergeCNFFormulas formulas = S.foldl S.union S.empty (S.fromList formulas)
 
-literals :: (Ord c) => CNF c -> Set (Atom c)
-literals formula = S.foldl S.union S.empty (S.map (S.map literal) formula)
+literals :: (Ord c) => CNF c -> Set c
+literals formula = S.map atom $ S.foldl S.union S.empty (S.map (S.map literal) formula)
 
-naiveSAT :: (Ord c) => CNF c -> Bool
-naiveSAT formula = nSat simplifiedFormula allLits
+naiveSATBool :: (Ord c) => CNF c -> Bool
+naiveSATBool formula = case naiveSAT formula of
+  Just asg -> True
+  Nothing -> False
+  
+-- A very naive implementation of DPLL
+naiveSAT :: (Ord c) => CNF c -> Maybe (SatisfyingAssignment c)
+naiveSAT formula = nSat formula allLits
   where
-    simplifiedFormula = unitClauseSimplify formula
-    allLits = literals simplifiedFormula
+    allLits = literals formula
     
-nSat :: (Ord c) => CNF c -> Set (Atom c) -> Bool
+nSat :: (Ord c) => CNF c -> Set c -> Maybe (SatisfyingAssignment c)
 nSat formula lits = case S.member S.empty formula of
-  True -> False
+  True -> Nothing
   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)
+    0 -> Just M.empty
+    _ -> case S.size unitClauses of
+      0 -> pickLitAndSplit formula lits
+      _ -> unitSimplify unitClause formula lits
+      where
+        unitClauses = S.filter (\c -> S.size c == 1) formula
+        unitClause = S.findMin unitClauses
 
-unitClauseSimplify :: (Ord c) => CNF c -> CNF c
-unitClauseSimplify formula = S.foldl removeUnitClause formula unitClauses
+pickLitAndSplit :: (Ord c) => CNF c -> Set c -> Maybe (SatisfyingAssignment c)
+pickLitAndSplit formula lits = orElse trueAsg falseAsg
   where
-    unitClauses = S.filter (\s -> S.size s == 1) formula
+    nextLit = S.findMin lits
+    nextLits = S.delete nextLit lits
+    trueRes = nSat (S.insert (clause [lit nextLit]) formula) nextLits
+    falseRes = nSat (S.insert (clause [negation $ lit nextLit]) formula) nextLits
+    trueAsg = liftM (M.insert nextLit True) trueRes
+    falseAsg = liftM (M.insert nextLit False) falseRes
 
+unitSimplify :: (Ord c) =>
+                Clause c ->
+                CNF c ->
+                Set c ->
+                Maybe (SatisfyingAssignment c)
+unitSimplify unitClause formula lits = satResWithUnitAsg
+  where
+    simplifiedFormula = removeUnitClause formula unitClause
+    litToSimplify = S.findMin unitClause
+    tVal = assignTruthVal litToSimplify
+    satRes = nSat simplifiedFormula lits
+    satResWithUnitAsg = liftM (M.insert (atom litToSimplify) tVal) satRes
+    
 removeUnitClause :: (Ord c) => CNF c -> Clause c -> CNF c
 removeUnitClause formula c = remainingClauses
   where
diff --git a/src/Proper/Clause.hs b/src/Proper/Clause.hs
--- a/src/Proper/Clause.hs
+++ b/src/Proper/Clause.hs
@@ -1,6 +1,7 @@
 module Proper.Clause(
-  Atom, negation, lit, nLit, literal,
-  Clause, clause, concatClause) where
+  Atom, atom, negation, lit, nLit, literal,
+  Clause, clause, concatClause,
+  assignTruthVal) where
 
 import Data.Set as S
 
@@ -10,7 +11,11 @@
   Lit a |
   NLit a
   deriving (Eq, Ord, Show)
-  
+
+assignTruthVal :: Atom l -> Bool
+assignTruthVal (Lit _) = True
+assignTruthVal (NLit _) = False
+
 negation :: Atom a -> Atom a
 negation (Lit n) = NLit n
 negation (NLit n) = Lit n
@@ -18,6 +23,9 @@
 literal :: Atom a -> Atom a
 literal (Lit n) = Lit n
 literal (NLit n) = Lit n
+
+atom (Lit n) = n
+atom (NLit n) = n
 
 lit name = Lit name
 nLit name = NLit name
diff --git a/src/Proper/Formula.hs b/src/Proper/Formula.hs
new file mode 100644
--- /dev/null
+++ b/src/Proper/Formula.hs
@@ -0,0 +1,235 @@
+module Proper.Formula(
+  Formula, checkTheorem,
+  neg, con, dis, val, bic, imp,
+  truthAssignment,
+  evalFormula,
+  isValidByTruthTable,
+  toCNF, theorem,
+  bddCheckTaut) where
+
+import Data.Foldable
+import Data.Monoid
+import Data.Map as M
+import Proper.BDD
+import Proper.Clause
+import Proper.CNF
+import Proper.Utils
+
+data Formula s =
+  Val s                         |
+  Neg (Formula s)              |
+  Con (Formula s) (Formula s) |
+  Dis (Formula s) (Formula s) |
+  Bic (Formula s) (Formula s) |
+  Imp (Formula s) (Formula s)
+  deriving (Eq, Ord)
+
+instance Functor Formula where
+  fmap f (Val v) = Val (f v)
+  fmap f (Neg s) = Neg (fmap f s)
+  fmap f (Con s1 s2) = Con (fmap f s1) (fmap f s2)
+  fmap f (Dis s1 s2) = Dis (fmap f s1) (fmap f s2)
+  fmap f (Bic s1 s2) = Bic (fmap f s1) (fmap f s2)
+  fmap f (Imp s1 s2) = Imp (fmap f s1) (fmap f s2)
+
+instance Foldable Formula where
+  foldMap f (Val v) = f v
+  foldMap f (Neg s) = foldMap f s
+  foldMap f (Con s1 s2) = mappend (foldMap f s1) (foldMap f s2)
+  foldMap f (Dis s1 s2) = mappend (foldMap f s1) (foldMap f s2)
+  foldMap f (Imp s1 s2) = mappend (foldMap f s1) (foldMap f s2)
+  foldMap f (Bic s1 s2) = mappend (foldMap f s1) (foldMap f s2)
+  
+instance Show s => Show (Formula s) where
+  show = showSent
+  
+showSent :: (Show s) => (Formula s) -> String
+showSent (Val name) = show 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
+
+constantsF :: Formula s -> [Formula s]
+constantsF s = foldMap (\n -> [Val n]) s
+
+constants :: Formula s -> [Formula s]
+constants s = foldMap (\n -> [Val n]) s
+
+type TruthAssignment s = Map (Formula s) Bool
+
+truthVal :: (Ord s, Show s) => Formula s -> TruthAssignment s -> Bool
+truthVal s tt = case M.lookup s tt of
+  Just val -> val
+  Nothing -> error $ "Formula not in truth table " ++ show s
+
+truthAssignment :: (Ord s) => [s] -> [Bool] -> TruthAssignment s
+truthAssignment constNames constVals = M.fromList $ zip consts constVals
+  where
+    consts = Prelude.map val constNames
+
+evalFormula :: (Ord s, Show s) => TruthAssignment s -> Formula s -> Bool
+evalFormula a (Neg s) = not $ evalFormula a s
+evalFormula a (Con s1 s2) = (evalFormula a s1) && (evalFormula a s2)
+evalFormula a (Dis s1 s2) = (evalFormula a s1) || (evalFormula a s2)
+evalFormula a (Imp s1 s2) = (not s1Eval) || s2Eval
+  where
+    s1Eval = evalFormula a s1
+    s2Eval = evalFormula a s2
+evalFormula a (Bic s1 s2) = (s1Eval && s2Eval) || ((not s1Eval) && (not s2Eval))
+  where
+    s1Eval = evalFormula a s1
+    s2Eval = evalFormula a s2
+evalFormula a constant = truthVal constant a
+  
+type TruthTable s = [TruthAssignment s]
+
+containsFormula :: (Ord s) => Formula s -> TruthTable s -> Bool
+containsFormula s [] = False
+containsFormula s tt = M.member s (head tt)
+
+truthTable :: (Ord s, Show s) => [Formula s] -> TruthTable s
+truthTable sents = Prelude.foldl addFormula [] sents
+
+addFormula :: (Ord s, Show s) => TruthTable s -> Formula s -> TruthTable s
+addFormula tt s = if (containsFormula s tt)
+  then tt
+  else addNewFormula tt s
+
+addNewFormula :: (Ord s, Show s) => TruthTable s -> Formula s -> TruthTable s
+addNewFormula [] c@(Val n) = [truthAssignment [n] [True], truthAssignment [n] [False]]
+addNewFormula 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
+addNewFormula tt s = Prelude.map (addCompoundFormula s) tt
+
+addCompoundFormula ::(Ord s, Show s) => Formula s -> TruthAssignment s -> TruthAssignment s
+addCompoundFormula s ta = insert s sval ta
+  where
+    sval = evalFormula ta s
+
+truthTableForFormula :: (Ord s, Show s) => Formula s -> TruthTable s
+truthTableForFormula s = truthTable $ (constants s) ++ [s]
+                          
+isValidByTruthTable :: (Ord s, Show s) => Formula s -> Bool
+isValidByTruthTable s = Prelude.and sTruthVals
+  where
+    sTruthTable = truthTableForFormula s
+    sTruthVals = Prelude.map (truthVal s) sTruthTable
+    
+-- Format conversion functions
+toCNF :: (Ord s, Show s) => Formula s -> CNF s
+toCNF = cnf .
+        cnfClauses .
+        distributeDisjunction .
+        pushNegation .
+        removeImplication .
+        removeBiconditional
+
+cnfClauses :: (Ord s, Show s) => Formula s -> [Clause s]
+cnfClauses (Con s1 s2) = cnfClauses s1 ++ cnfClauses s2
+cnfClauses s = [disjunctiveClause s]
+
+disjunctiveClause :: (Ord s, Show s) => Formula s -> Clause s
+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 :: Formula s -> Formula s
+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 :: Formula s -> Formula s
+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 :: Formula s -> Formula s
+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 :: Formula s -> Formula s
+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 s = Thm [Formula s] (Formula s)
+               deriving (Eq)
+                        
+instance Show s => Show (Theorem s) where
+  show = showThm
+  
+showThm :: (Show s) => Theorem s -> 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 :: [Formula s] -> Formula s -> Theorem s
+theorem axioms hypothesis = Thm axioms hypothesis
+
+checkTheorem :: (Ord s, Show s) => Theorem s -> Bool
+checkTheorem (Thm axioms hypothesis) = case naiveSAT cnfFormNegThm of
+  Just asg -> False
+  Nothing -> True
+  where
+    cnfAxioms = Prelude.map toCNF axioms
+    cnfNotHypothesis = toCNF (neg hypothesis)
+    cnfFormNegThm = mergeCNFFormulas (cnfNotHypothesis:cnfAxioms)
+    
+-- BDD conversion code
+    
+bddCheckTaut :: (Ord s) => Formula s -> Bool
+bddCheckTaut sent = isTaut (toBDD sent)
+
+toBDD :: (Ord s) => Formula s -> BDD s
+toBDD (Val n) = singletonBDD n
+toBDD (Neg sent) = negBDD (toBDD sent)
+toBDD (Dis f1 f2) = disBDD (toBDD f1) (toBDD f2)
+toBDD (Con f1 f2) = conBDD (toBDD f1) (toBDD f2)
+toBDD (Imp f1 f2) = impBDD (toBDD f1) (toBDD f2)
+toBDD (Bic f1 f2) = bicBDD (toBDD f1) (toBDD f2)
diff --git a/src/Proper/Sentence.hs b/src/Proper/Sentence.hs
deleted file mode 100644
--- a/src/Proper/Sentence.hs
+++ /dev/null
@@ -1,233 +0,0 @@
-module Proper.Sentence(
-  Sentence, checkTheorem,
-  neg, con, dis, val, bic, imp,
-  truthAssignment,
-  evalSentence,
-  isValidByTruthTable,
-  toCNF, theorem,
-  bddCheckTaut) where
-
-import Data.Foldable
-import Data.Monoid
-import Data.Map as M
-import Proper.BDD
-import Proper.Clause
-import Proper.CNF
-import Proper.Utils
-
-data Sentence s =
-  Val s                         |
-  Neg (Sentence s)              |
-  Con (Sentence s) (Sentence s) |
-  Dis (Sentence s) (Sentence s) |
-  Bic (Sentence s) (Sentence s) |
-  Imp (Sentence s) (Sentence s)
-  deriving (Eq, Ord)
-
-instance Functor Sentence where
-  fmap f (Val v) = Val (f v)
-  fmap f (Neg s) = Neg (fmap f s)
-  fmap f (Con s1 s2) = Con (fmap f s1) (fmap f s2)
-  fmap f (Dis s1 s2) = Dis (fmap f s1) (fmap f s2)
-  fmap f (Bic s1 s2) = Bic (fmap f s1) (fmap f s2)
-  fmap f (Imp s1 s2) = Imp (fmap f s1) (fmap f s2)
-
-instance Foldable Sentence where
-  foldMap f (Val v) = f v
-  foldMap f (Neg s) = foldMap f s
-  foldMap f (Con s1 s2) = mappend (foldMap f s1) (foldMap f s2)
-  foldMap f (Dis s1 s2) = mappend (foldMap f s1) (foldMap f s2)
-  foldMap f (Imp s1 s2) = mappend (foldMap f s1) (foldMap f s2)
-  foldMap f (Bic s1 s2) = mappend (foldMap f s1) (foldMap f s2)
-  
-instance Show s => Show (Sentence s) where
-  show = showSent
-  
-showSent :: (Show s) => (Sentence s) -> String
-showSent (Val name) = show 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
-
-constantsF :: Sentence s -> [Sentence s]
-constantsF s = foldMap (\n -> [Val n]) s
-
-constants :: Sentence s -> [Sentence s]
-constants s = foldMap (\n -> [Val n]) s
-
-type TruthAssignment s = Map (Sentence s) Bool
-
-truthVal :: (Ord s, Show s) => Sentence s -> TruthAssignment s -> Bool
-truthVal s tt = case M.lookup s tt of
-  Just val -> val
-  Nothing -> error $ "Sentence not in truth table " ++ show s
-
-truthAssignment :: (Ord s) => [s] -> [Bool] -> TruthAssignment s
-truthAssignment constNames constVals = M.fromList $ zip consts constVals
-  where
-    consts = Prelude.map val constNames
-
-evalSentence :: (Ord s, Show s) => TruthAssignment s -> Sentence s -> 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 s = [TruthAssignment s]
-
-containsSentence :: (Ord s) => Sentence s -> TruthTable s -> Bool
-containsSentence s [] = False
-containsSentence s tt = M.member s (head tt)
-
-truthTable :: (Ord s, Show s) => [Sentence s] -> TruthTable s
-truthTable sents = Prelude.foldl addSentence [] sents
-
-addSentence :: (Ord s, Show s) => TruthTable s -> Sentence s -> TruthTable s
-addSentence tt s = if (containsSentence s tt)
-  then tt
-  else addNewSentence tt s
-
-addNewSentence :: (Ord s, Show s) => TruthTable s -> Sentence s -> TruthTable s
-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 ::(Ord s, Show s) => Sentence s -> TruthAssignment s -> TruthAssignment s
-addCompoundSentence s ta = insert s sval ta
-  where
-    sval = evalSentence ta s
-
-truthTableForSentence :: (Ord s, Show s) => Sentence s -> TruthTable s
-truthTableForSentence s = truthTable $ (constants s) ++ [s]
-                          
-isValidByTruthTable :: (Ord s, Show s) => Sentence s -> Bool
-isValidByTruthTable s = Prelude.and sTruthVals
-  where
-    sTruthTable = truthTableForSentence s
-    sTruthVals = Prelude.map (truthVal s) sTruthTable
-    
--- Format conversion functions
-toCNF :: (Ord s, Show s) => Sentence s -> CNF s
-toCNF = cnf .
-        cnfClauses .
-        distributeDisjunction .
-        pushNegation .
-        removeImplication .
-        removeBiconditional
-
-cnfClauses :: (Ord s, Show s) => Sentence s -> [Clause s]
-cnfClauses (Con s1 s2) = cnfClauses s1 ++ cnfClauses s2
-cnfClauses s = [disjunctiveClause s]
-
-disjunctiveClause :: (Ord s, Show s) => Sentence s -> Clause s
-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 s -> Sentence s
-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 s -> Sentence s
-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 s -> Sentence s
-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 s -> Sentence s
-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 s = Thm [Sentence s] (Sentence s)
-               deriving (Eq)
-                        
-instance Show s => Show (Theorem s) where
-  show = showThm
-  
-showThm :: (Show s) => Theorem s -> 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 s] -> Sentence s -> Theorem s
-theorem axioms hypothesis = Thm axioms hypothesis
-
-checkTheorem :: (Ord s, Show s) => Theorem s -> Bool
-checkTheorem (Thm axioms hypothesis) = not $ naiveSAT cnfFormNegThm
-  where
-    cnfAxioms = Prelude.map toCNF axioms
-    cnfNotHypothesis = toCNF (neg hypothesis)
-    cnfFormNegThm = mergeCNFFormulas (cnfNotHypothesis:cnfAxioms)
-    
--- BDD conversion code
-    
-bddCheckTaut :: (Ord s) => Sentence s -> Bool
-bddCheckTaut sent = isTaut (toBDD sent)
-
-toBDD :: (Ord s) => Sentence s -> BDD s
-toBDD (Val n) = singletonBDD n
-toBDD (Neg sent) = negBDD (toBDD sent)
-toBDD (Dis f1 f2) = disBDD (toBDD f1) (toBDD f2)
-toBDD (Con f1 f2) = conBDD (toBDD f1) (toBDD f2)
-toBDD (Imp f1 f2) = impBDD (toBDD f1) (toBDD f2)
-toBDD (Bic f1 f2) = bicBDD (toBDD f1) (toBDD f2)
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -4,10 +4,10 @@
 import Proper.CNFTests
 import Proper.LexerTests
 import Proper.ParserTests
-import Proper.SentenceTests
+import Proper.FormulaTests
 
 main = do
-  allSentenceTests
+  allFormulaTests
   allCNFTests
   allLexerTests
   allParserTests