diff options
Diffstat (limited to 'contrib/jprover/README')
| -rw-r--r-- | contrib/jprover/README | 76 |
1 files changed, 0 insertions, 76 deletions
diff --git a/contrib/jprover/README b/contrib/jprover/README deleted file mode 100644 index ec654a03..00000000 --- a/contrib/jprover/README +++ /dev/null @@ -1,76 +0,0 @@ -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. - - |