diff --git a/FirstOrderTheory.cabal b/FirstOrderTheory.cabal
new file mode 100644
--- /dev/null
+++ b/FirstOrderTheory.cabal
@@ -0,0 +1,21 @@
+-- Initial FirstOrderTheory.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                FirstOrderTheory
+version:             0.1.0.4
+synopsis:            Grammar and typeclass for first order theories
+description:         Grammar and typeclass for first order theories
+license:             BSD3
+license-file:        LICENSE
+author:              Dillon Huff
+maintainer:          dillonhuff@gmail.com
+-- copyright:           
+category:            Math
+build-type:          Simple
+cabal-version:       >=1.8
+
+library
+  exposed-modules:     FirstOrderTheory.Theory, FirstOrderTheory.Utils, FirstOrderTheory.Syntax
+  -- other-modules:       
+  build-depends:       base ==4.6.*, containers
+  hs-source-dirs:      src
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:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the name of Dillon Huff nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND 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 COPYRIGHT
+OWNER 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/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/FirstOrderTheory/Syntax.hs b/src/FirstOrderTheory/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/src/FirstOrderTheory/Syntax.hs
@@ -0,0 +1,79 @@
+module FirstOrderTheory.Syntax(
+  Literal, Atom, Term,
+  atomArgs, predicateName, isFunctionWithName,
+  isNeg, getAtom, varName, intVal, funcArgs,
+  lit, nLit, atom, func, var, intConst) where
+
+import Data.List as L
+
+import FirstOrderTheory.Utils
+
+data Literal
+  = Lit Atom
+  | Neg Atom
+    deriving (Eq, Ord)
+
+lit = Lit
+nLit = Neg
+
+-- |Returns false if the literal is an atomic formula and true if the
+-- literal is the negation of an atomic formula
+isNeg :: Literal -> Bool
+isNeg (Neg _) = True
+isNeg _ = False
+
+-- |Returns the atomic formula of the given literal
+getAtom :: Literal -> Atom
+getAtom (Neg a) = a
+getAtom (Lit a) = a
+
+instance Show Literal where
+  show (Lit p) = show p
+  show (Neg p) = "~" ++ show p
+
+data Atom = Atom Name [Term]
+                 deriving (Eq, Ord)
+
+-- |Returns a new atom
+atom = Atom
+
+-- |Return the terms that are arguments to the predicate of the input atom
+atomArgs (Atom _ args) = args
+
+-- |Return the name of the predicate of the input atom
+predicateName (Atom n _) = n
+
+instance Show Atom where
+  show (Atom name args) = name ++ "[" ++ (L.intercalate ", " $ L.map show args) ++ "]"
+
+data Term
+  = Function Name [Term]
+  | Variable Name
+  | Integer Int
+    deriving (Eq, Ord)
+
+func = Function
+var = Variable
+intConst = Integer
+
+-- |Returns True if the input term is a function with the give name,
+-- and false otherwise
+isFunctionWithName n (Function m _) = n == m
+isFunctionWithName _ _ = False
+
+-- |Return the name of the input variable,
+-- throws error if input term is not a variable
+varName (Variable n) = n
+
+-- |Returns the input function's argument list,
+-- throws error if input term is not a function
+funcArgs (Function _ args) = args
+
+-- |Returns the integer value of an Integer constant or an error
+-- if the input is not an integer
+intVal (Integer i) = i
+
+instance Show Term where
+  show (Integer val) = show val
+  show (Variable name) = name
+  show (Function name args) = name ++ "(" ++ (L.intercalate ", " $ L.map show args) ++ ")"
diff --git a/src/FirstOrderTheory/Theory.hs b/src/FirstOrderTheory/Theory.hs
new file mode 100644
--- /dev/null
+++ b/src/FirstOrderTheory/Theory.hs
@@ -0,0 +1,31 @@
+module FirstOrderTheory.Theory(
+  FirstOrderTheory(..),
+  PredicateDecl,
+  FunctionDecl,
+  predicateDecl,
+  functionDecl) where
+
+import Data.Set as S
+
+import FirstOrderTheory.Syntax
+import FirstOrderTheory.Utils
+
+data PredicateDecl = PredicateDecl Name Arity [Sort]
+                     deriving (Eq, Ord)
+
+-- |Specify a new predicate declaration
+predicateDecl = PredicateDecl
+
+data FunctionDecl = FunctionDecl Name Arity [Sort] Sort
+                    deriving (Eq, Ord)
+
+-- |Specify a new function declaration
+functionDecl = FunctionDecl
+
+-- |Description of a decidable first order theory
+class FirstOrderTheory t where
+  theoryName :: t -> String
+  sorts :: t -> Set Sort
+  predicates :: t -> Set PredicateDecl
+  functions :: t -> Set FunctionDecl
+  decideSat :: t -> Set Literal -> (Bool, Set Literal)
diff --git a/src/FirstOrderTheory/Utils.hs b/src/FirstOrderTheory/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/FirstOrderTheory/Utils.hs
@@ -0,0 +1,12 @@
+module FirstOrderTheory.Utils(
+  Name, Arity, Sort,
+  sort) where
+
+type Name = String
+type Arity = Int
+
+type Sort = String
+
+-- |Make a new sort with the input name
+sort :: String -> Sort
+sort str = str