diff --git a/pkgs/applications/science/logic/iprover/default.nix b/pkgs/applications/science/logic/iprover/default.nix
new file mode 100644
index 000000000000..7bfd8dff12e3
--- /dev/null
+++ b/pkgs/applications/science/logic/iprover/default.nix
@@ -0,0 +1,58 @@
+x@{builderDefsPackage
+  , ocaml, eprover
+  , ...}:
+builderDefsPackage
+(a :  
+let 
+  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ 
+    [];
+
+  buildInputs = map (n: builtins.getAttr n x)
+    (builtins.attrNames (builtins.removeAttrs x helperArgNames));
+  sourceInfo = rec {
+    baseName="iprover";
+    version="0.8.1";
+    name="${baseName}_v${version}";
+    url="${baseName}.googlecode.com/files/${name}.tar.gz";
+    hash="15qn523w4l296np5rnkwi50a5x2xqz0kaza7bsh9bkazph7jma7w";
+  };
+in
+rec {
+  src = a.fetchurl {
+    url = sourceInfo.url;
+    sha256 = sourceInfo.hash;
+  };
+
+  inherit (sourceInfo) name version;
+  inherit buildInputs;
+
+  /* doConfigure should be removed if not needed */
+  phaseNames = ["doConfigure" "doMake" "doDeploy"];
+  configureCommand = "sh configure";
+  doDeploy = a.fullDepEntry (''
+    ensureDir "$out/bin"
+    cp iproveropt "$out/bin"
+
+    ensureDir "$out/share/${name}"
+    cp *.p "$out/share/${name}"
+    echo -e "#! /bin/sh\\n$out/bin/iproveropt --clausifier \"${eprover}/bin/eprover\" --clausifier_options \" --tstp-format --silent --cnf \" \"\$@\"" > "$out"/bin/iprover
+    chmod a+x  "$out"/bin/iprover
+  '') ["defEnsureDir" "minInit" "doMake"];
+      
+  meta = {
+    description = "An automated first-order logic theorem prover";
+    maintainers = with a.lib.maintainers;
+    [
+      raskin
+    ];
+    platforms = with a.lib.platforms;
+      linux;
+    license = "GPLv3";
+  };
+  passthru = {
+    updateInfo = {
+      downloadPage = "http://code.google.com/p/iprover/downloads/list";
+    };
+  };
+}) x
+
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 30a3280110ee..0659b1111020 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -6979,6 +6979,8 @@ let
     inherit (pkgs.emacs23Packages) proofgeneral;
   };
 
+  iprover = callPackage ../applications/science/logic/iprover {};
+
   leo2 = callPackage ../applications/science/logic/leo2 {};
 
   prover9 = callPackage ../applications/science/logic/prover9 { };