1 files changed, 76 insertions, 0 deletions
diff --git a/contrib/jprover/README b/contrib/jprover/README
new file mode 100644
index 00000000..ec654a03
--- /dev/null
+++ b/contrib/jprover/README
@@ -0,0 +1,76 @@
+An intuitionistic first-order theorem prover -- JProver.
+
+Usage:
+
+Require JProver.
+Jp [num].
+
+Whem [num] is provided, proof is done automatically with
+the multiplicity limit [num], otherwise no limit is forced
+and JProver may not terminate.
+
+Example:
+
+Require JProver.
+Coq < Goal (P:Prop) P->P.
+1 subgoal
+
+============================
+ (P:Prop)P->P
+
+Unnamed_thm < Jp 1.
+Proof is built.
+Subtree proved!
+-----------------------------------------
+
+Description:
+JProver is a theorem prover for first-order intuitionistic logic.
+It is originally implemented by Stephan Schmitt and then integrated into
+MetaPRL by Aleksey Nogin (see jall.ml). After this, Huang extracted the
+necessary ML-codes from MetaPRL and then integrated it into Coq.
+The MetaPRL URL is http://metaprl.org/. For more information on 
+integrating JProver into interactive proof assistants, please refer to
+
+   "Stephan Schmitt, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin, 
+   Jprover: Integrating connection-based theorem proving into interactive 
+   proof assistants. In International Joint Conference on Automated 
+   Reasoning, volume 2083 of Lecture Notes in Artificial Intelligence, 
+   pages 421-426. Springer-Verlag, 2001" - 
+   http://www.cs.cornell.edu/nogin/papers/jprover.html
+ 
+
+Structure of this directory:
+This directory contains
+
+        README          ------  this file
+        jall.ml         ------  the main module of JProver
+        jtunify.ml      ------  string unification procedures for jall.ml
+        jlogic.ml       ------  interface module of jall.ml
+        jterm.ml
+        opname.ml       ------  implement the infrastructure for jall.ml
+        jprover.ml4     ------  the interface of jall.ml to Coq
+        JProver.v       ------  declaration for Coq
+        Makefile        ------  the makefile
+        go              ------  batch file to load JProver to Coq dynamically
+
+
+Comments:
+1. The original <jall.ml> is located in meta-prl/refiner/reflib of the
+MetaPRL directory. Some parts of this file are modified by Huang.
+
+2. <jtunify.ml> is also located in meta-prl/refiner/reflib with no modification.
+
+3. <jlogic.ml> is modified from meta-prl/refiner/reflib/jlogic_sig.mlz.
+
+4. <jterm.ml> and <opname.ml> are modified from the standard term module
+of MetaPRL in meta-prl/refiner/term_std.
+
+5. The Jp tactic currently cannot prove formula such as
+   ((x:nat) (P x)) -> (EX y:nat| (P y)), which requires extra constants
+in the domain when the left-All rule is applied.
+
+
+
+by Huang Guan-Shieng (Guan-Shieng.Huang@lri.fr), March 2002.
+
+