Added a tactic entry for Jprover + commented out inputenc in the main file

(no use having both fontenc and inputenc)


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

3 files changed, 87 insertions, 10 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 81ccc657e..87ec44812 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1791,6 +1791,57 @@ incompatibilities.
 
 \SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
+\subsection{{\tt Jp} {\em (Jprover)}}\tacindex{Jp {\em (Jprover)}}
+\label{Jprover}
+
+The tactic \texttt{Jp}, due to Huang Guan-Shieng, is a direct port of
+the {\em Jprover}\cite{SLKN01} semi-decision procedure for first-order
+intuitionistic logic implemented in {\em Nuprl}\cite{Kre02}. It is a
+connection-based procedure restricted to the intuitionnistic case by a
+constraint solver. 
+
+Search is bounded by a multiplicity parameter indicating how many
+copies of a formula may be used in the proof process. 
+For instance, a multiplicity of 1 restricts Jp to the
+intuitionistic first-order logic without contraction (but with weakening).
+
+\begin{coq_eval}
+Variable S:Set.
+Variables P Q:S->Prop.
+Variable f:S->S.
+\end{coq_eval}
+
+\begin{coq_example*}
+Lemma example: (exists x |P x\/Q x)->(exists x |P x)\/(exists x |Q x).
+jp.
+Qed.
+
+Lemma example2: (forall x ,P x->P (f x))->forall x,P x->P (f(f x)).
+jp.
+Qed.
+\end{coq_example*}
+
+\begin{Variants}
+ \item {\tt Jp $n$}\\
+   \tacindex{Jp $n$} 
+   Tries the {\em Jprover} procedure with multiplicities up to $n$,
+   starting from 1.
+ \item {\tt Jp}\\
+   Tries the {\em Jprover} procedure without multiplicity bound, 
+   possibly running forever.
+\end{Variants}
+
+\begin{ErrMsgs}
+ \item \errindex{multiplicity limit reached}\\
+   The procedure tried all multiplicities below the limit and
+   failed. Goal might be solved by increasing the multiplicity limit. 
+ \item \errindex{formula is not provable}\\
+   The procedure determined that goal was not provable in
+   intuitionistic first-order logic, no matter how big the
+   multiplicity is.
+\end{ErrMsgs}
+
+
 % \subsection{\tt Linear}\tacindex{Linear}\label{Linear}
 % The tactic \texttt{Linear}, due to Jean-Christophe Filli{\^a}atre
 % \cite{Fil94}, implements a decision procedure for {\em Direct
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index baad64c60..af404d505 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -1,6 +1,6 @@
 \documentclass[11pt,a4paper]{book}
 \usepackage[T1]{fontenc}
-\usepackage[latin1]{inputenc}
+%\usepackage[latin1]{inputenc}
 \usepackage{url}
 \usepackage{verbatim}
 \usepackage{palatino}
diff --git a/doc/biblio.bib b/doc/biblio.bib
index 87783c50b..2317ee3bc 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -120,10 +120,10 @@ s},
 
 @PhdThesis{Bou97These,
   author =       {S. Boutin},
-  title =        {Réflexions sur les quotients},
+  title =        {R�éflexions sur les quotients},
   school =       {Paris 7},
   year =         1997,
-  type =         {thèse d'Université},
+  type =         {th�èse d'Universit�é},
   month =        apr
 }
 
@@ -166,7 +166,7 @@ s},
 
 @PHDTHESIS{CPar95,
         AUTHOR             = {C. Parent},
-        SCHOOL             = {Ecole {Normale} {Sup{\'e}rieure} de {Lyon}},
+        SCHOOL             = {Ecole {Normale} {Sup�érieure} de {Lyon}},
         TITLE              = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}},
         YEAR               = {1995}
 }
@@ -218,7 +218,7 @@ s},
 @INPROCEEDINGS{CoPa89,
         AUTHOR             = {Th. Coquand and C. Paulin-Mohring},
         BOOKTITLE          = {Proceedings of Colog'88},
-        EDITOR             = {P. Martin-L{\"o}f and G. Mints},
+        EDITOR             = {P. Martin-L�öf and G. Mints},
         PUBLISHER          = {Springer-Verlag},
         SERIES             = {LNCS},
         TITLE              = {Inductively defined types},
@@ -288,7 +288,7 @@ s},
         AUTHOR             = {J. Courant},
         MONTH              = sep,
         SCHOOL             = {DEA d'Informatique, ENS Lyon},
-        TITLE              = {Explicitation de preuves par r{\'e}currence implicite},
+        TITLE              = {Explicitation de preuves par r�écurrence implicite},
         YEAR               = {1994}
 }
 
@@ -296,7 +296,7 @@ s},
   author    = "Delahaye, D.",
   title     = "Information {R}etrieval in a {{\sf Coq}} {P}roof {L}ibrary using
                {T}ype {I}somorphisms",
-  booktitle = "Proceedings of TYPES'99, Lökeberg",
+  booktitle = "Proceedings of TYPES'99, L�ökeberg",
   publisher = "Springer-Verlag LNCS",
   year      = "1999",
   note      =
@@ -321,9 +321,9 @@ s},
 
 @INPROCEEDINGS{DelMay01,
   author    = "Delahaye, D. and Mayero, M.",
-  title     = "{\tt Field}: une procédure de décision pour les nombres réels
+  title     = "{\tt Field}: une proc�édure de d�écision pour les nombres r�éels
                en {{\sf Coq}}",
-  booktitle = "Journées Francophones des Langages Applicatifs, Pontarlier",
+  booktitle = "Journ�ées Francophones des Langages Applicatifs, Pontarlier",
   publisher = "INRIA",
   month     = "Janvier",
   year      = "2001",
@@ -500,7 +500,7 @@ s},
 }
 
 @TechReport{Gim98,
-  author = 	 {E. Giménez},
+  author = 	 {E. Gim�énez},
   title = 	 {A Tutorial on Recursive Types in Coq},
   institution =  {INRIA},
   year = 	 1998,
@@ -661,6 +661,16 @@ Alan Robinson},
         YEAR               = {1952}
 }
 
+@MANUAL{Kre02,
+        AUTHOR             = {C. Kreitz},
+        TITLE              = {The Nuprl Proof Development System, Version 5~:
+Reference Manual and User's Guide},
+        INSTITUTION        = {Department of Computer Science, 
+Cornell University},
+        MONTH              = dec,
+        YEAR               = {2002}
+} 
+
 @BOOK{Kri90,
         AUTHOR             = {J.-L. Krivine},
         PUBLISHER          = {Masson},
@@ -908,6 +918,22 @@ the Calculus of Inductive Constructions}},
         YEAR               = {1994}
 }
 
+@INPROCEEDINGS{SLKN01,
+        AUTHOR             = {S. Schmitt and L. Lorigo and C. Kreitz 
+and A. Nogin},
+        TITLE              = {Integrating Connection-based Theorem Proving 
+into Interactive Proof Assistants}, 
+        BOOKTITLE          = {Proceedings of International Joint Conference on 
+Automated Reasoning},
+        EDITOR             = {R. Gore and A. Leitsch and T. Nipkow},
+        PUBLISHER          = {Springer},
+        SERIES             = {LNAI},
+        VOLUME             = {2083},
+        PAGES              = {421--426},
+        YEAR               = {2001}
+}
+
+
 @MASTERSTHESIS{Ter92,
         AUTHOR             = {D. Terrasse},
         MONTH              = sep,