diff --git a/Proper.cabal b/Proper.cabal
--- a/Proper.cabal
+++ b/Proper.cabal
@@ -2,10 +2,14 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                Proper
-version:             0.3.0.0
+version:             0.4.0.0
 synopsis:	     An implementation of propositional logic in Haskell            
--- description:         
-license:  		BSD3           
+description:         Proper is both an executable theorem prover for Propositional logic
+		     and a library for incorporating propositional logic into other Haskell
+		     programs. See the github repo for examples of theorem files for the
+		     executable.
+
+license:  	     BSD3           
 license-file:        LICENSE
 author:		     Dillon Huff              
 maintainer:	     Dillon Huff
@@ -18,7 +22,7 @@
 library
   hs-source-dirs:	src
   build-depends:	base==4.5.*, containers
-  exposed-modules:	Proper.Sentence, Proper.CNF, Proper.Clause
+  exposed-modules:	Proper.Sentence, Proper.CNF, Proper.Clause, Proper.BDD
 
 executable Proper
   main-is:             Main.hs
diff --git a/src/Proper/BDD.hs b/src/Proper/BDD.hs
new file mode 100644
--- /dev/null
+++ b/src/Proper/BDD.hs
@@ -0,0 +1,131 @@
+module Proper.BDD(
+  BDD, trueBDD, falseBDD, singletonBDD, negBDD,
+  disBDD, conBDD, impBDD, bicBDD,
+  isTaut) where
+
+import Data.Map as M
+import Data.List as L
+import Data.Tuple as T
+
+data BDD p =
+  TrueNode            |
+  FalseNode           |
+  N p (BDD p) (BDD p)
+  deriving (Eq, Show)
+  
+node :: (Eq p) => p -> BDD p -> BDD p -> BDD p
+node v l r = case l == r of
+  True -> l
+  False -> N v l r
+  
+trueBDD = TrueNode
+falseBDD = FalseNode
+singletonBDD v = N v TrueNode FalseNode
+
+negBDD :: (Eq p) => BDD p -> BDD p
+negBDD TrueNode = FalseNode
+negBDD FalseNode = TrueNode
+negBDD (N p l r) = node p (negBDD l) (negBDD r)
+
+disBDD :: (Ord p) => BDD p -> BDD p -> BDD p
+disBDD TrueNode _ = TrueNode
+disBDD _ TrueNode = TrueNode
+disBDD FalseNode n = n
+disBDD n FalseNode = n
+disBDD l@(N p ll lr) r@(N q rl rr) = case compare p q of
+  LT -> node q (disBDD l rl) (disBDD l rr)
+  GT -> node p (disBDD ll r) (disBDD lr r)
+  EQ -> node p (disBDD ll rl) (disBDD lr rr)
+  
+conBDD :: (Ord p) => BDD p -> BDD p -> BDD p
+conBDD l r = negBDD (disBDD (negBDD l) (negBDD r))
+
+impBDD :: (Ord p) => BDD p -> BDD p -> BDD p
+impBDD l r = (disBDD (negBDD l) r)
+
+bicBDD :: (Ord p) => BDD p -> BDD p -> BDD p
+bicBDD l r = (conBDD (impBDD l r) (impBDD r l))
+
+isTaut TrueNode = True
+isTaut _ = False
+{-
+data BDD p = BDD (Map (BDDNode p) Int) (Map Int (BDDNode p)) Int
+             deriving (Eq, Show)
+                      
+data BDDNode p =
+  TrueNode  |
+  FalseNode |
+  N p Int Int
+  deriving (Eq, Ord, Show)
+           
+negateNode :: BDDNode p -> BDDNode p
+negateNode (N p l r) = N p r l
+negateNode n = n
+
+root :: (Ord p) => BDD p -> BDDNode
+root (BDD nToInt _ _) = fst $ M.findMax nToInd
+
+leftChild :: (Ord p) => BDD p -> BDD p
+leftChild bdd@(BDD nToInt intToN n) = deleteTreeFrom (rightNode r) (deleteNode r bdd)
+ where
+   r = root bdd
+   
+deleteTreeFrom :: (Ord p) => BDDNode p -> BDD p -> BDD p
+deleteTreeFrom (N p l r) bdd = deleteTreeFrom 
+   
+deleteNode :: (Ord p) => BDDNode p -> BDD p -> BDD p
+deleteNode n bdd@(BDD nToInt intToN m) = BDD (M.delete n nToInt) (M.delete nInd intToN) m
+  where
+    nInd = case M.lookup n nToInt of
+      Just ind -> ind
+      Nothing -> m+1
+
+trueBDD :: (Ord p) => BDD p
+trueBDD = BDD (M.fromList [(TrueNode, 1)]) (M.fromList [(1, TrueNode)]) 2
+
+falseBDD :: (Ord p) => BDD p
+falseBDD = BDD (M.fromList [(FalseNode, 0)]) (M.fromList [(0, FalseNode)]) 2
+
+singletonBDD :: (Ord p) => p -> BDD p
+singletonBDD val = BDD (M.fromList sl) (M.fromList (L.map swap sl)) 3
+  where
+    sl = [(TrueNode, 1), (FalseNode, 0), (N val 1 0, 2)]
+    
+negBDD :: (Ord p) => BDD p -> BDD p
+negBDD (BDD nToInt intToN n) = BDD negNToInt negIntToN n
+  where
+    negNToInt = mapKeys negateNode nToInt
+    negIntToN = M.fromList $  L.map swap $ M.toList negNToInt
+    
+disBDD :: (Ord p) => BDD p -> BDD p -> BDD p
+disBDD left right = case left == trueBDD || right == trueBDD of
+  True -> trueBDD
+  False -> case left == falseBDD && right == falseBDD of
+    True -> falseBDD
+    False -> disMerge left right
+    
+disMerge :: (Ord p) => BDD p -> BDD p -> BDD p
+disMerge left right = case leftRoot == rightRoot of
+  True -> makeBDD leftRoot (disBDD lrlc rrlc) (disBDD lrrc rrrc)
+  False -> case leftRoot > rightRoot of
+    True -> makeBDD leftRoot (disBDD lrlc rightRoot) (disBDD lrrc rightRoot)
+    False -> makeBDD rightRoot (disBDD leftRoot rrlc) (disBDD leftRoot rrrc)
+  where
+    leftRoot = root left
+    rightRoot = root right
+    lrlc = leftChild leftRoot
+    lrrc = rightChild leftRoot
+    rrlc = leftChild rightRoot
+    rrrc = rightChild rightRoot
+
+isTaut :: (Ord p) => BDD p -> Bool
+isTaut b = b == trueBDD
+
+newBDD :: (Ord p) => BDD p
+newBDD = BDD M.empty M.empty 2
+
+addNode :: (Ord p) => BDD p -> BDDNode p -> (BDD p, Int)
+addNode bdd@(BDD nToInt intToN n) newNode = case M.lookup newNode nToInt of
+  Just nodeInd -> (bdd, nodeInd)
+  Nothing -> (BDD (M.insert newNode (n+1) nToInt) (M.insert (n+1) newNode intToN) (n+1), n)
+-}
diff --git a/src/Proper/Sentence.hs b/src/Proper/Sentence.hs
--- a/src/Proper/Sentence.hs
+++ b/src/Proper/Sentence.hs
@@ -4,12 +4,13 @@
   truthAssignment,
   evalSentence,
   isValidByTruthTable,
-  toCNF, theorem) where
+  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
@@ -217,3 +218,16 @@
     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
@@ -1,5 +1,6 @@
 module Main(main) where
 
+import Proper.BDDTests
 import Proper.CNFTests
 import Proper.LexerTests
 import Proper.ParserTests
@@ -10,3 +11,4 @@
   allCNFTests
   allLexerTests
   allParserTests
+  allBDDTests