--- /dev/null
+\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}
\fcolorbox{black}{gray}{\usebox{\tmpxyz}}
\end{center}}
-\bibliographystyle{alpha}
+\bibliographystyle{klunum}
\begin{document}
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
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.
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.
%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
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
projects / helm.git / commitdiff