From cb452e26fdaa2000f5e9c4e3fa5de512626f8ee7 Mon Sep 17 00:00:00 2001 From: huang Date: Thu, 4 Apr 2002 08:54:56 +0000 Subject: Add citations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2607 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/jprover/README | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) 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. and 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. -- cgit v1.2.3