diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,4 @@
+# Revision history for stp
+
+## 0.1.0.0 -- 2018-11-20
+* First version.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2018, Boro Sitnikovski
+
+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 Boro Sitnikovski 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,17 @@
+# Simple Theorem Prover
+
+Simple Theorem Prover is a proof tree generator. It allows for specifying axioms and inference rules, and then by quering the program it will produce all valid combinations of inference in attempt to reach a target result.
+
+This project is based on [Simple theorem prover in Racket](https://bor0.wordpress.com/2018/08/07/simple-theorem-prover-in-racket/).
+
+## Prerequisites
+
+Make sure you have `ghc` and `cabal` installed. Also, make sure that `cabal update` is ran to ensure latest version of packages is used.
+
+## Installation
+
+1. Run `cabal sandbox init`
+1. Run `cabal install` to install dependencies and build this project
+1. Run `cabal run` to run the example
+
+Copyright 2018, Boro Sitnikovski. All rights reserved.
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/example/MU.hs b/example/MU.hs
new file mode 100644
--- /dev/null
+++ b/example/MU.hs
@@ -0,0 +1,21 @@
+module Main where
+
+import SimpleTheoremProver
+
+import Text.Regex (subRegex, matchRegex, mkRegex)
+import Data.List (isSuffixOf)
+
+muRules :: [Rule String]
+muRules = [
+    Rule   "One"   (\thm -> if (isSuffixOf "I" thm) then (thm ++ "U") else thm)
+    , Rule "Two"   (\thm -> case (matchRegex (mkRegex "M(.*)") thm) of
+                                Just [x] -> thm ++ x
+                                _        -> thm)
+    , Rule "Three" (\thm -> subRegex (mkRegex "III") thm "U")
+    , Rule "Four"  (\thm -> subRegex (mkRegex "UU") thm "")
+    ]
+
+testProver = TheoremProver (map mkAxiom ["MI"]) muRules
+
+main :: IO ()
+main = print $ findProof testProver "MIUIU" 5
diff --git a/src/SimpleTheoremProver.hs b/src/SimpleTheoremProver.hs
new file mode 100644
--- /dev/null
+++ b/src/SimpleTheoremProver.hs
@@ -0,0 +1,60 @@
+module SimpleTheoremProver where
+
+import Data.List (nubBy, find)
+import Data.Set (fromList, union)
+
+-- | Based on https://bor0.wordpress.com/2018/08/07/simple-theorem-prover-in-racket/.
+
+-- | A rule is a way to change a theorem.
+data Rule a = Rule { name :: String , function :: a -> a }
+
+instance Show (Rule a) where
+    show (Rule a _) = a
+
+-- | A theorem is consisted of an initial axiom and rules (ordered set) applied
+data Theorem a = Theorem { axiom :: a , rulesThm :: [Rule a] , result :: a } deriving (Show)
+
+-- | A prover system is consisted of a bunch of axioms and rules to apply between them
+data TheoremProver a = TheoremProver { axioms :: [Theorem a] , rulesThmProver :: [Rule a] } deriving (Show)
+
+-- | An axiom is just a theorem already proven
+mkAxiom :: a -> Theorem a
+mkAxiom a = Theorem a [] a
+
+-- | Applies a single rule to a theorem
+thmApplyRule :: Theorem a -> Rule a -> Theorem a
+thmApplyRule theorem rule =
+    Theorem
+    (axiom theorem)
+    (rulesThm theorem ++ [rule])
+    ((function rule) (result theorem))
+
+-- | Applies all prover's rules to a list of theorems
+thmApplyRules :: TheoremProver a -> [Theorem a] -> [Theorem a]
+thmApplyRules prover (thm:thms) = map (thmApplyRule thm) (rulesThmProver prover) ++ (thmApplyRules prover thms)
+thmApplyRules _ _ = []
+
+-- | Merge two list of proofs but skip duplicate proofs, giving the first argument priority
+-- This is used to avoid circular results in the search tree
+-- E.g. application of rules resulting in an earlier theorem/axiom
+mergeProofs :: Eq a => [Theorem a] -> [Theorem a] -> [Theorem a]
+mergeProofs p1 p2 = nubBy (\t1 t2 -> result t1 == result t2) p1 ++ p2
+
+-- | Finds a proof by constructing a proof tree by iteratively applying theorem rules
+findProofIter :: (Ord a, Eq a) => TheoremProver a -> a -> Int -> [Theorem a] -> Maybe (Theorem a)
+findProofIter _ _ 0 _ = Nothing
+findProofIter prover target depth foundProofs = case (find (\x -> target == result x) foundProofs) of
+    Just prf -> Just prf
+    Nothing  -> 
+        let theorems = thmApplyRules prover foundProofs
+            proofsSet = fromList (map result foundProofs)
+            theoremsSet = fromList (map result theorems) in
+        if (union proofsSet theoremsSet) == proofsSet
+        -- The case where no new theorems were produced, that is, A union B = A
+        then Nothing
+        -- Otherwise keep producing new proofs
+        else findProofIter prover target (depth - 1) (mergeProofs foundProofs theorems)
+
+-- | Find proof helper
+findProof :: Ord a => TheoremProver a -> a -> Int -> Maybe (Theorem a)
+findProof prover target depth = findProofIter prover target depth (axioms prover)
diff --git a/stp.cabal b/stp.cabal
new file mode 100644
--- /dev/null
+++ b/stp.cabal
@@ -0,0 +1,45 @@
+name:                stp
+version:             0.1.0.0
+synopsis:            Simple Theorem Prover
+copyright:           (c) 2018 Boro Sitnikovski
+homepage:            https://github.com/bor0/stp
+license:             BSD3
+license-file:        LICENSE
+author:              Boro Sitnikovski
+maintainer:          buritomath@gmail.com
+category:            Math
+build-type:          Simple
+extra-source-files:  CHANGELOG.md
+cabal-version:       >=1.10
+description:
+    Simple Theorem Prover constructs a proof tree
+    and searches for a target/conclusion given a
+    list of rewrite rules and axioms/theorems.
+extra-source-files:
+    CHANGELOG.md
+    README.md
+    LICENSE
+
+source-repository head
+    type: git
+    location: https://github.com/bor0/stp
+
+source-repository this
+    type: git
+    tag: 0.1.0.0
+    location: https://github.com/bor0/stp
+
+library
+    exposed-modules:     SimpleTheoremProver
+    build-depends:       base >=4.11 && <4.12
+                         , containers ==0.5.11.0
+    hs-source-dirs:      src
+    default-language:    Haskell2010
+
+executable mu-test
+    main-is:             MU.hs
+    build-depends:       base >=4.11 && <4.12
+                         , regex-compat ==0.95.1
+                         , stp
+    hs-source-dirs:      example
+    default-language:    Haskell2010