minor fixes to ENGLISH

[helm.git] / helm / papers / matita / matita.bib

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",