From d44115e936254b8d77b12a659f5e5d8ca85d8663 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 30 Jan 2006 15:46:50 +0000 Subject: [PATCH] - use kluwer bibtex style for numbered references - do not ignore .bbl any longer --- helm/papers/matita/matita.bib | 6 +- helm/papers/matita/matita2.bbl | 119 +++++++++++++++++++++++++++++++++ helm/papers/matita/matita2.tex | 12 ++-- 3 files changed, 130 insertions(+), 7 deletions(-) create mode 100644 helm/papers/matita/matita2.bbl diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib index 12b28d754..9e74514b7 100644 --- a/helm/papers/matita/matita.bib +++ b/helm/papers/matita/matita.bib @@ -952,6 +952,7 @@ @misc{debrujinfactor, title = "The ``de Bruijn factor''", howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}", + year = {2000}, author = "Freek Wiedijk", } @@ -972,6 +973,7 @@ title = "The {C}oq Proof Assistant Reference Manual", author = "The Coq Development Team", howpublished = "\\\url{http://coq.inria.fr/doc/main.html}", + year = {2005}, key = "CoqManual" } @@ -1065,6 +1067,7 @@ title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0", editor="{Patrick Ion} and others", howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}", + year = {2003}, url = "\url{http://www.w3.org/TR/MathML2}", key = "Mathematical" } @@ -1121,7 +1124,8 @@ editor="{Tim Bray} and others", @misc{omdoc, title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)", - howpublished = "\\\url{http://www.mathweb.org/omdoc/omdoc.ps}", + howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}", + year = {2005}, key = "OMDoc" } diff --git a/helm/papers/matita/matita2.bbl b/helm/papers/matita/matita2.bbl new file mode 100644 index 000000000..3974d0107 --- /dev/null +++ b/helm/papers/matita/matita2.bbl @@ -0,0 +1,119 @@ +\begin{thebibliography}{00} + +\bibitem{mkm-helm} +Asperti, A., F. Guidi, L. Padovani, C. {Sacerdoti Coen}, and I. Schena: 2003, + `Mathematical Knowledge Management in {HELM}'. +\newblock {\em Annals of Mathematics and Artificial Intelligence} {\bf + 38(1-3)}, 27--46. + +\bibitem{whelp} +Asperti, A., F. Guidi, C. {Sacerdoti Coen}, E. Tassi, and S. Zacchiroli: 2004, + `A content based mathematical search engine: Whelp'. +\newblock In: {\em Post-proceedings of the Types 2004 International + Conference}, Vol. LNCS, (to appear). pp. xxx--xxx. + +\bibitem{content-centric} +Asperti, A., L. padovani, C. {Sacerdoti Coen}, and irene Schena: 2000, + `Content-centric Logical Envirnoments'. +\newblock Short Presentation at the Fifteenth IEEE Symposium on Logic in + Computer Science. + +\bibitem{remathematization} +Asperti, A., L. Padovani, C. {Sacerdoti Coen}, and I. Schena: 2001, `{XML}, + Stylesheets and the re-mathematization of Formal Content'. +\newblock In: {\em EXTREME}. + +\bibitem{pechino} +Asperti, A. and B. Wegner: 2003, `An Approach to Machine-Understandable + Representation of the Mathematical Information in Digital Documents'. +\newblock In: F. Bai and B. Wegner (eds.): {\em Electronic Information and + Communication in Mathematics}, Vol. LNCS, 2730. pp. 14--23. + +\bibitem{proofgeneral} +Aspinall, D.: 2000, `{P}roof {G}eneral: A Generic Tool for Proof Development'. +\newblock In: {\em Tools and Algorithms for the Construction and Analysis of + Systems, TACAS 2000}, Vol. 1785 of {\em LNCS}. + +\bibitem{proof-by-pointing} +Bertot, Y.: 1993, `Proof by Pointing'. +\newblock In: {\em Symposium on Theoretical Aspects Computer Software (STACS)}, + Vol. 789 of {\em Lecture Notes in Computer Science}. + +\bibitem{ctcoq1} +Bertot, Y.: 1999, `The CtCoq System: Design and Architecture'. +\newblock {\em Formal Aspects of Computing} {\bf 11}, 225--243. + +\bibitem{gdome2} +Casarini, P. and L. Padovani: 2002, `The {G}nome {DOM} {E}ngine'. +\newblock {\em Markup Languages: Theory \& Practice} {\bf 3}(2), 173--190. + +\bibitem{nuprl-book} +Constable, R.~L., S.~F. Allen, H.~M. Bromley, W.~R. Cleaveland, J.~F. Cremer, + R.~W. Harper, D.~J. Howe, T.~B. Knoblock, N.~P. Mendler, P. Panangaden, J.~T. + Sasaki, and S.~F. Smith: 1986, {\em Implementing Mathematics with the {N}uprl + Development System}. +\newblock NJ: Prentice-Hall. + +\bibitem{YANNTHESIS} +Coscoy, Y.: 2000, `Explication textuelle de preuves pour le {C}alcul des + {C}onstructions {I}nductives'. +\newblock Ph.D. thesis, Universit\'e de Nice-Sophia Antipolis. + +\bibitem{natural} +Coscoy, Y., G. Kahn, and L. Thery: 1995, `{Extracting Text from Proofs}'. +\newblock Technical Report RR-2459, Inria (Institut National de Recherche en + Informatique et en Automatique), France. + +\bibitem{mathml} +Mathematical: 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{omdoc} +OMDoc: 2005, `{OMDoc}: An Open Markup Format for Mathematical Documents + (Version 1.1)'. +\newblock \\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}. + +\bibitem{padovani} +Padovani, L.: 2003a, `MathML Formatting'. +\newblock Ph.D. thesis, University of Bologna. +\newblock Technical Report UBLCS 2003-03. + +\bibitem{latexmathml} +Padovani, L.: 2003b, `On the Roles of LATEX and MathML in Encoding and + Processing Mathematical Expressions'. +\newblock In: {\em MKM '03: Proceedings of the Second International Conference + on Mathematical Knowledge Management}. London, UK, pp. 66--79. + +\bibitem{exportation-module} +{Sacerdoti Coen}, C.: 2003, `From Proof-Assistans to Distributed Libraries of + Mathematics: Tips and Pitfalls'. +\newblock In: A. Asperti, B. Buchberger, and J.~H. Davenport (eds.): {\em + Proceedings of the Second International Conference on Mathematical Knowledge + Management, MKM 2003}, Vol. LNCS, 2594. pp. 30--44. + +\bibitem{disambiguation} +{Sacerdoti Coen}, C. and S. Zacchiroli: 2004, `Efficient Ambiguous Parsing of + Mathematical Formulae'. +\newblock In: A.~T. Andrea~Asperti, Grzegorz~Bancerek (ed.): {\em Proceedings + of Mathematical Knowledge Management 2004}, Vol. LNCS, 3119. pp. 347--362. + +\bibitem{CoqManual} +Team, T. C.~D.: 2005, `The {C}oq Proof Assistant Reference Manual'. +\newblock \\\url{http://coq.inria.fr/doc/main.html}. + +\bibitem{Werner} +Werner, B.: 1994, `Une Th\'eorie des {C}onstructions {I}nductives'. +\newblock Ph.D. thesis, Universit\'e Paris VII. + +\bibitem{debrujinfactor} +Wiedijk, F.: 2000, `The ``de Bruijn factor'''. +\newblock \\\url{http://www.cs.ru.nl/~freek/factor/}. + +\bibitem{zack-master} +Zacchiroli, S.: 2003, `Web {s}ervices per il supporto alla dimostrazione + interattiva'. +\newblock Master's thesis, University of Bologna. + +\end{thebibliography} diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index d2e1616ed..9617915f2 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -85,7 +85,7 @@ \fcolorbox{black}{gray}{\usebox{\tmpxyz}} \end{center}} -\bibliographystyle{alpha} +\bibliographystyle{klunum} \begin{document} @@ -308,7 +308,7 @@ a a set of \emph{modules} also forming a DAG. Modules and \components{} provide coherent sets of functionalities at different scales. Applications that require only a few functionalities -depend on a restricted set of \components{}. +depend on a restricted set of \components. Only the proof assistant \MATITA{} and the \WHELP{} search engine are applications meant to be used directly by the user. All the other applications @@ -475,7 +475,7 @@ unification procedures of the \texttt{cic\_unification} \component. The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the commands of the \MATITA{} proof assistant. Most of the commands are tactics. Other commands are used to give definitions and axioms or to state theorems -and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}. +and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA. It implements the semantics of each command in the grafite AST as a function from status to status. It implements also an undo function to go back to previous statuses. @@ -699,7 +699,7 @@ to its historical origins, \MATITA{} strives to provide innovative functionalities for the interaction with the library. It is more traditional in its script based authoring interface. -In the remaining part of the paper we focus on the user view of \MATITA{}. +In the remaining part of the paper we focus on the user view of \MATITA. This section is devoted to the aspects of the tool that arise from the document centric approach to the library. Sect.~\ref{sec:authoring} describes the peculiarities of the authoring interface. @@ -1075,7 +1075,7 @@ user interaction during the disambiguation. %store the XML encoding of the objects defined in the script, the %disambiguation aliases and the interpretation and notational convention defined, %while the latter is used to store all the metadata needed by -%\WHELP{}. +%\WHELP. % %While the consistency of the data store in the two media has %nothing to do with the nature of @@ -1224,7 +1224,7 @@ expression and the suffix \verb+_to_Prop+. In the above example, The authoring interface of \MATITA{} is very similar to Proof General. We chose not to build the \MATITA{} UI over Proof General for two reasons. First of all we wanted to integrate our XML-based rendering technologies, mainly -\GTKMATHVIEW{}. At the time of writing Proof General supports only text based +\GTKMATHVIEW. At the time of writing Proof General supports only text based rendering.\footnote{This may change with the future release of Proof General based on Eclipse, but is not yet the case.} The second reason is that we wanted to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit -- 2.39.2