diff --git a/FirstOrderTheory.cabal b/FirstOrderTheory.cabal
--- a/FirstOrderTheory.cabal
+++ b/FirstOrderTheory.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                FirstOrderTheory
-version:             0.1.0.4
+version:             0.1.0.6
 synopsis:            Grammar and typeclass for first order theories
 description:         Grammar and typeclass for first order theories
 license:             BSD3
@@ -17,5 +17,5 @@
 library
   exposed-modules:     FirstOrderTheory.Theory, FirstOrderTheory.Utils, FirstOrderTheory.Syntax
   -- other-modules:       
-  build-depends:       base ==4.6.*, containers
+  build-depends:       base ==4.6.*, containers, Proper
   hs-source-dirs:      src
diff --git a/src/FirstOrderTheory/Syntax.hs b/src/FirstOrderTheory/Syntax.hs
--- a/src/FirstOrderTheory/Syntax.hs
+++ b/src/FirstOrderTheory/Syntax.hs
@@ -1,13 +1,46 @@
 module FirstOrderTheory.Syntax(
   Literal, Atom, Term,
+  NNFFormula, nnfLit, nnfCon, nnfDis,
+  toPropositionalCNF,
+  negateLit,
   atomArgs, predicateName, isFunctionWithName,
   isNeg, getAtom, varName, intVal, funcArgs,
   lit, nLit, atom, func, var, intConst) where
 
 import Data.List as L
 
+import Proper.CNF
+import Proper.Formula
+
 import FirstOrderTheory.Utils
 
+-- |A quantifier free formla in negation normal form
+data NNFFormula
+  = Con NNFFormula NNFFormula
+  | Dis NNFFormula NNFFormula
+  | LF Literal
+    deriving (Eq, Ord, Show)
+
+-- |Returns a NNF Formula consisting of only the input literal
+nnfLit :: Literal -> NNFFormula
+nnfLit l = LF l
+
+-- |Returns the conjunction of two NNF formulas
+nnfCon l r = Con l r
+
+-- |Return the disjunction of two NNF formulas
+nnfDis l r = Dis l r
+
+-- | Convert NNFFormula to propositional formula in
+-- conjunctive normal form
+toPropositionalCNF :: NNFFormula -> CNF Literal
+toPropositionalCNF formula = toCNF $ toProperFormula formula
+
+toProperFormula :: NNFFormula -> Formula Literal
+toProperFormula (LF l) = val l
+toProperFormula (Con l r) = con (toProperFormula l) (toProperFormula r)
+toProperFormula (Dis l r) = dis (toProperFormula l) (toProperFormula l)
+
 data Literal
   = Lit Atom
   | Neg Atom
@@ -21,6 +54,10 @@
 isNeg :: Literal -> Bool
 isNeg (Neg _) = True
 isNeg _ = False
+
+-- |Return the negation of the input literal
+negateLit (Lit a) = Neg a
+negateLit (Neg a) = Lit a
 
 -- |Returns the atomic formula of the given literal
 getAtom :: Literal -> Atom
diff --git a/src/FirstOrderTheory/Theory.hs b/src/FirstOrderTheory/Theory.hs
--- a/src/FirstOrderTheory/Theory.hs
+++ b/src/FirstOrderTheory/Theory.hs
@@ -2,6 +2,7 @@
   FirstOrderTheory(..),
   PredicateDecl,
   FunctionDecl,
+  nnfLit, nnfCon, nnfDis,
   predicateDecl,
   functionDecl) where