diff --git a/Proper.cabal b/Proper.cabal
--- a/Proper.cabal
+++ b/Proper.cabal
@@ -2,13 +2,13 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                Proper
-version:             0.1.0.0
+version:             0.2.0.0
 synopsis:	     An implementation of propositional logic in Haskell            
 -- description:         
 license:  		BSD3           
 license-file:        LICENSE
--- author:              
--- maintainer:          
+author:		     Dillon Huff              
+maintainer:	     Dillon Huff          
 -- copyright:           
 -- category:            
 build-type:          Simple
diff --git a/src/Proper/CNF.hs b/src/Proper/CNF.hs
--- a/src/Proper/CNF.hs
+++ b/src/Proper/CNF.hs
@@ -8,24 +8,24 @@
 import Proper.Clause
 import Proper.Utils
 
-type CNF = Set Clause
+type CNF c = Set (Clause c)
   
-cnf :: [Clause] -> CNF
+cnf :: (Ord c) => [Clause c] -> CNF c
 cnf clauses = S.fromList clauses
 
-mergeCNFFormulas :: [CNF] -> CNF
+mergeCNFFormulas :: (Ord c) => [CNF c] -> CNF c
 mergeCNFFormulas formulas = S.foldl S.union S.empty (S.fromList formulas)
 
-literals :: CNF -> Set Atom
+literals :: (Ord c) => CNF c -> Set (Atom c)
 literals formula = S.foldl S.union S.empty (S.map (S.map literal) formula)
 
-naiveSAT :: CNF -> Bool
+naiveSAT :: (Ord c) => CNF c -> Bool
 naiveSAT formula = nSat simplifiedFormula allLits
   where
     simplifiedFormula = unitClauseSimplify formula
     allLits = literals simplifiedFormula
     
-nSat :: CNF -> Set Atom -> Bool
+nSat :: (Ord c) => CNF c -> Set (Atom c) -> Bool
 nSat formula lits = case S.member S.empty formula of
   True -> False
   False -> case S.size formula of
@@ -39,12 +39,12 @@
       nextFormula = unitClauseSimplify (S.insert unitClause formula)
       nextFormulaNeg = unitClauseSimplify (S.insert unitNegClause formula)
 
-unitClauseSimplify :: CNF -> CNF
+unitClauseSimplify :: (Ord c) => CNF c -> CNF c
 unitClauseSimplify formula = S.foldl removeUnitClause formula unitClauses
   where
     unitClauses = S.filter (\s -> S.size s == 1) formula
 
-removeUnitClause :: CNF -> Clause -> CNF
+removeUnitClause :: (Ord c) => CNF c -> Clause c -> CNF c
 removeUnitClause formula c = remainingClauses
   where
     elemC = S.findMin c
diff --git a/src/Proper/Clause.hs b/src/Proper/Clause.hs
--- a/src/Proper/Clause.hs
+++ b/src/Proper/Clause.hs
@@ -6,26 +6,26 @@
 
 import Proper.Utils
 
-data Atom =
-  Lit Name |
-  NLit Name
+data Atom a =
+  Lit a |
+  NLit a
   deriving (Eq, Ord, Show)
   
-negation :: Atom -> Atom
+negation :: Atom a -> Atom a
 negation (Lit n) = NLit n
 negation (NLit n) = Lit n
 
-literal :: Atom -> Atom
+literal :: Atom a -> Atom a
 literal (Lit n) = Lit n
 literal (NLit n) = Lit n
 
 lit name = Lit name
 nLit name = NLit name
 
-type Clause = Set Atom
+type Clause c = Set (Atom c)
 
-concatClause :: Clause -> Clause -> Clause
+concatClause :: (Ord c) => Clause c -> Clause c -> Clause c
 concatClause c1 c2 = S.union c1 c2
 
-clause :: [Atom] -> Clause
+clause :: (Ord a) => [Atom a] -> Clause a
 clause atoms = S.fromList atoms
diff --git a/src/Proper/Sentence.hs b/src/Proper/Sentence.hs
--- a/src/Proper/Sentence.hs
+++ b/src/Proper/Sentence.hs
@@ -12,20 +12,20 @@
 import Proper.CNF
 import Proper.Utils
 
-data Sentence =
-  Val Name              |
-  Neg Sentence          |
-  Con Sentence Sentence |
-  Dis Sentence Sentence |
-  Bic Sentence Sentence |
-  Imp Sentence Sentence
+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 Show Sentence where
+instance Show s => Show (Sentence s) where
   show = showSent
   
-showSent :: Sentence -> String
-showSent (Val name) = name
+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 ++ ")"
@@ -39,7 +39,7 @@
 imp s1 s2 = Imp s1 s2
 val name = Val name
 
-constants :: Sentence -> [Sentence]
+constants :: Sentence s -> [Sentence s]
 constants (Val n) = [(Val n)]
 constants (Neg s) = constants s
 constants (Con s1 s2) = constants s1 ++ constants s2
@@ -47,19 +47,19 @@
 constants (Bic s1 s2) = constants s1 ++ constants s2
 constants (Imp s1 s2) = constants s1 ++ constants s2
 
-type TruthAssignment = Map Sentence Bool
+type TruthAssignment s = Map (Sentence s) Bool
 
-truthVal :: Sentence -> TruthAssignment -> 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 :: [Name] -> [Bool] -> TruthAssignment
+truthAssignment :: (Ord s) => [s] -> [Bool] -> TruthAssignment s
 truthAssignment constNames constVals = M.fromList $ zip consts constVals
   where
     consts = Prelude.map val constNames
 
-evalSentence :: TruthAssignment -> Sentence -> Bool
+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)
@@ -73,21 +73,21 @@
     s2Eval = evalSentence a s2
 evalSentence a constant = truthVal constant a
   
-type TruthTable = [TruthAssignment]
+type TruthTable s = [TruthAssignment s]
 
-containsSentence :: Sentence -> TruthTable -> Bool
+containsSentence :: (Ord s) => Sentence s -> TruthTable s -> Bool
 containsSentence s [] = False
 containsSentence s tt = M.member s (head tt)
 
-truthTable :: [Sentence] -> TruthTable
+truthTable :: (Ord s, Show s) => [Sentence s] -> TruthTable s
 truthTable sents = Prelude.foldl addSentence [] sents
 
-addSentence :: TruthTable -> Sentence -> TruthTable
+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 :: TruthTable -> Sentence -> TruthTable
+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
@@ -95,22 +95,22 @@
    ttTrue = Prelude.map (\ta -> M.insert c True ta) tt
 addNewSentence tt s = Prelude.map (addCompoundSentence s) tt
 
-addCompoundSentence :: Sentence -> TruthAssignment -> TruthAssignment
+addCompoundSentence ::(Ord s, Show s) => Sentence s -> TruthAssignment s -> TruthAssignment s
 addCompoundSentence s ta = insert s sval ta
   where
     sval = evalSentence ta s
 
-truthTableForSentence :: Sentence -> TruthTable
+truthTableForSentence :: (Ord s, Show s) => Sentence s -> TruthTable s
 truthTableForSentence s = truthTable $ (constants s) ++ [s]
                           
-isValidByTruthTable :: Sentence -> Bool
+isValidByTruthTable :: (Ord s, Show s) => Sentence s -> Bool
 isValidByTruthTable s = and sTruthVals
   where
     sTruthTable = truthTableForSentence s
     sTruthVals = Prelude.map (truthVal s) sTruthTable
     
 -- Format conversion functions
-toCNF :: Sentence -> CNF
+toCNF :: (Ord s, Show s) => Sentence s -> CNF s
 toCNF = cnf .
         cnfClauses .
         distributeDisjunction .
@@ -118,17 +118,17 @@
         removeImplication .
         removeBiconditional
 
-cnfClauses :: Sentence -> [Clause]
+cnfClauses :: (Ord s, Show s) => Sentence s -> [Clause s]
 cnfClauses (Con s1 s2) = cnfClauses s1 ++ cnfClauses s2
 cnfClauses s = [disjunctiveClause s]
 
-disjunctiveClause :: Sentence -> Clause
+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 -> Sentence
+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)
@@ -138,7 +138,7 @@
     q = removeImplication s2
 removeImplication s = s
 
-removeBiconditional :: Sentence -> Sentence
+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)
@@ -151,7 +151,7 @@
     q = removeBiconditional s2
 removeBiconditional (Val name) = (Val name)
 
-pushNegation :: Sentence -> Sentence
+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))
@@ -159,7 +159,7 @@
 pushNegation (Dis s1 s2) = Dis (pushNegation s1) (pushNegation s2)
 pushNegation s = s
 
-distributeDisjunction :: Sentence -> Sentence
+distributeDisjunction :: Sentence s -> Sentence s
 distributeDisjunction (Con p q) = Con (distributeDisjunction p) (distributeDisjunction q)
 distributeDisjunction (Dis p (Con q r)) = Con pdq pdr
  where
@@ -180,22 +180,22 @@
 distributeDisjunction s = s
 
 -- Theorem code
-data Theorem = Thm [Sentence] Sentence
+data Theorem s = Thm [Sentence s] (Sentence s)
                deriving (Eq)
                         
-instance Show Theorem where
+instance Show s => Show (Theorem s) where
   show = showThm
   
-showThm :: Theorem -> String
+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] -> Sentence -> Theorem
+theorem :: [Sentence s] -> Sentence s -> Theorem s
 theorem axioms hypothesis = Thm axioms hypothesis
 
-checkTheorem :: Theorem -> Bool
+checkTheorem :: (Ord s, Show s) => Theorem s -> Bool
 checkTheorem (Thm axioms hypothesis) = not $ naiveSAT cnfFormNegThm
   where
     cnfAxioms = Prelude.map toCNF axioms