From a031418f35afefcad507d6f13d6a33fd35f3c86b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 31 Jan 2006 10:51:24 +0000 Subject: [PATCH] minor fixes to ENGLISH added CoqArt book --- helm/papers/matita/matita.bib | 17 ++++++++++++++--- helm/papers/matita/matita2.bbl | 5 +++++ helm/papers/matita/matita2.tex | 6 +++--- 3 files changed, 22 insertions(+), 6 deletions(-) diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib index 7d98905d5..fd1ef3b6e 100644 --- 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 865dcc468..03704995b 100644 --- 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 65b5882af..bd22ffe54 100644 --- 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 -- 2.39.5