help path is no longer hard coded but relative to runtime base dir

[helm.git] / helm / papers / matita / matita2.tex

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index e8d55f5a1d4d9286c78e3aa0153e018a4a93274a..a0c014251979413ea0b1edaba8e0cd26f52b47d0 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -98,7 +98,10 @@
 % \end{motto}
 
  \begin{abstract}
-  \TODO{scrivere abstract}
+  \MATITA{} is a new document-centric proof assistant that integrates several
+  Mathematical Knowledge Management tools and techniques. In this paper
+  we describe the architecture of \MATITA{} and the peculiarities of its user
+  interface.
  \end{abstract}
 
  \keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
@@ -107,16 +110,15 @@
 
 % toc & co: to be removed in the final paper version
 \tableofcontents
-\listoffigures
-\listoftables
 
 \section{Introduction}
 \label{sec:intro}
 
-\MATITA{} is the Proof Assistant under development by the \HELM{}
+\MATITA is the Proof Assistant under development by the \HELM{}
 team~\cite{mkm-helm} at the University of Bologna, under the direction of
-Prof.~Asperti. This paper describes the overall architecture of
-the system, focusing on its most distinctive and innovative 
+Prof.~Asperti. \MATITA{} is free software, the source code is available for
+download at \url{http://matita.cs.unibo.it}. This paper describes the overall
+architecture of the system, focusing on its most distinctive and innovative
 features.
 
 \subsection{Historical perspective}
@@ -1576,7 +1578,8 @@ where \texttt{H} is $\beta$-expanded over the second \texttt{n}
 occurrence. 
 
 At this point, since \COQ{} unification algorithm is essentially first-order,
-the application of an elimination principle (of the form $\forall P.\forall
+the application of an elimination principle (a term of type\linebreak
+$\forall P.\forall
 x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
 \texttt{(fun n0: nat => m + n = n0)}.
 
@@ -1754,16 +1757,41 @@ scripts, listed in Tab.~\ref{tab:scripts}.
  \label{tab:scripts}
 \end{table}
 
-We do not plan to maintain the library in a centralized way, 
-as most of the systems do. On the contrary we are currently
-developing Wiki-technologies to support collaborative 
-development of the library, encouraging people to expand, 
-modify and elaborate previous contributions.
-
-\section{Conclusions}
+\section{Conclusions and future work}
 \label{sec:conclusion}
 
-\TODO{conclusioni}
+In this paper we have described the architecture of the \MATITA{} proof
+assistant and the peculiarities of its user interface. \MATITA{} is
+characterized by the central role played by its library and the integration
+with modern Mathematical Knowledge Management tools and techniques.
+Among them: an innovative search technique that is addressed to both
+end-users and automatic proof search procedures; a \MATHML-based
+rendering interface coupled with a disambiguating parser to fully exploit
+the usual mathematical notation, using constants and symbols from the
+whole library; direct manipulation of terms in the GUI,
+with a corresponding elaborated
+textual syntax to record user actions; fine-grained execution of
+tacticals to simplify script structuring and replaying; a browsing
+tool to navigate the hypertext formed by the concepts in the library,
+integrated with natural language rendering of proofs; compatibility with
+the library of the \COQ{} proof assistant.
+
+In the near future we plan to continue the development focusing on and enhancing
+the peculiarities of \MATITA, starting from its document-centric philosophy.
+In particular, we do not plan to maintain the library in a centralized way, 
+as most of the other systems do. On the contrary we are currently developing
+Wiki-technologies to support collaborative development of the library,
+encouraging people to expand, modify and elaborate previous contributions.
+As a first step in this direction, we will integrate \MATITA{} with a
+revision control system, building on the invalidation and re-generation
+concepts already implemented to grant logical consistency.
+
+Thanks to an increasing dissemination activity, we hope in the\linebreak medium
+term to attract users to form a critical mass of users to enter in
+direct competition with the (still too few) major actors in the field.
+To this aim, we are also progressing in the development of a core library,
+mainly to identify possible unnoticed problems and to give evidence of the
+usability of the system.
 
 \acknowledgements
 We would like to thank all the people that during the past