minor fixes to ENGLISH

added CoqArt book

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index 7d98905d56e5ff0b6833e5df58753c6a6fee2b1a..fd1ef3b6e43ce3759a26cf340da90645fbbc5c27 100644 (file)
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -1,4 +1,4 @@
-@inproceedings{paramodulation,
+@book{paramodulation,
   author = "Robert Nieuwenhuis and Alberto Rubio",
   title = "Paramodulation-based thorem proving",
   booktitle = "Handbook of Automated Reasoning",
@@ -6,6 +6,7 @@
   pages = "471--443",
   publisher = "Elsevier and MIT Press",
   year = 2001,
+  NOTE = {ISBN-0-262-18223-8}
 }
 
 @inproceedings{latexmathml,
@@ -76,12 +77,12 @@
 }
 
 @inproceedings{proof-by-pointing,
-  author = "Yves Bertot",
+  author = "Yves Bertot and Gilles Kahn and Laurent Théry",
   title = "Proof by Pointing",
   booktitle = "Symposium on Theoretical Aspects Computer Software (STACS)",
   series = "Lecture Notes in Computer Science",
   volume = "789",
-  year = 1993
+  year = 1994
 }
 
 @inproceedings{thery-cyp,
@@ -296,6 +297,16 @@
   year            = 1989
 }
 
+@book{CoqArt,
+  author          = "Yves Bertot and Pierre Castéran",
+  title           = "{Interactive Theorem Proving and Program Development}",
+  publisher       = {Springer Verlag},
+  series          = {Texts in Theoretical Computer Science},
+  year            = 2004
+  NOTE            = {ISBN-3-540-20854-2}
+    
+}
+
 @inproceedings{proofgeneral,
   author          = "David Aspinall",
   title           = "{P}roof {G}eneral: A Generic Tool for Proof Development",

diff --git a/helm/papers/matita/matita2.bbl b/helm/papers/matita/matita2.bbl
index 865dcc468d80226e826cf57364e2813f1d0a7588..03704995b8785b2392e8368c9a46ab90b1c565b5 100644 (file)
--- a/helm/papers/matita/matita2.bbl
+++ b/helm/papers/matita/matita2.bbl
@@ -89,6 +89,11 @@ MathML: 2003, `Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0'.
 \newblock W3C Recommendation 21 February 2001,
   \url{http://www.w3.org/TR/MathML2}.
 
+\bibitem{paramodulation}
+Nieuwenhuis, R. and A. Rubio: 2001, `Paramodulation-based thorem proving'.
+\newblock In: J.~A. Robinson and A. Voronkov (eds.): {\em Handbook of Automated
+  Reasoning}. pp. 471--443.
+
 \bibitem{omdoc}
 OMDoc: 2005, `{OMDoc}: An Open Markup Format for Mathematical Documents
   (Version 1.1)'.

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 65b5882af121a964c1c2ec38d7c98055b0c4852f..bd22ffe544f5ff51e1df4f95888f2e911b873314 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -134,7 +134,7 @@ features.
 \subsection{Historical perspective}
 
 The origins of \MATITA{} go back to 1999. At the time we were mostly 
-interested to develop tools and techniques to enhance the accessibility
+interested in developing tools and techniques to enhance the accessibility
 via Web of libraries of formal mathematics. Due to its dimension, the
 library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems) 
 was chosen as a privileged test bench for our work, although experiments
@@ -150,7 +150,7 @@ following steps:
   the time an emerging standard, we naturally adopted that technology,
   fostering a content-centric architecture~\cite{content-centric} where
   the documents of the library were the the main components around which
-  everything else has to be build;
+  everything else has to be built;
 
  \item developing indexing and searching techniques supporting semantic
   queries to the library; 
@@ -273,7 +273,7 @@ assistants. Among them, the advanced indexing tools over the library and
 the parser for ambiguous mathematical notation.
 
 The size and complexity improvements over \COQ{} must be understood
-historically. \COQ{} is a quite old
+historically. \COQ{}\cite{CoqArt} is a quite old
 system whose development started 20 years ago. Since then,
 several developers have took over the code and several new research ideas
 that were not considered in the original architecture have been experimented