An intuitionistic first-order theorem prover -- JProver.

See the "README" file for more information.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2563 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 66 insertions, 0 deletions

diff --git a/contrib/jprover/README b/contrib/jprover/README
new file mode 100644
index 0000000000..2dfb428275
--- /dev/null
+++ b/contrib/jprover/README
@@ -0,0 +1,66 @@
+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.
+
+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.ml      ------  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 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.
+
+