diff options
| -rw-r--r-- | contrib/jprover/README | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/contrib/jprover/README b/contrib/jprover/README index 2dfb428275..fa08415f71 100644 --- a/contrib/jprover/README +++ b/contrib/jprover/README @@ -28,6 +28,16 @@ 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 @@ -55,7 +65,7 @@ MetaPRL directory. Some parts of this file are modified by Huang. 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 +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. |