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 is located in meta-prl/refiner/reflib of the MetaPRL directory. Some parts of this file are modified by Huang. 2. is also located in meta-prl/refiner/reflib with no modification. 3. is modified from meta-prl/refiner/reflib/jlogic_sig.mlz. 4. and 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.