moved some old stuff to the history

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

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index f3b1a12c328d6e9545d0f2b02b8d835e99916bad..a0c014251979413ea0b1edaba8e0cd26f52b47d0 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -99,7 +99,7 @@
 
  \begin{abstract}
   \MATITA{} is a new document-centric proof assistant that integrates several
 
  \begin{abstract}
   \MATITA{} is a new document-centric proof assistant that integrates several

-  Mathematical Knowledge Management techniques and tools. In this paper
+  Mathematical Knowledge Management tools and techniques. In this paper

   we describe the architecture of \MATITA{} and the peculiarities of its user
   interface.
  \end{abstract}
   we describe the architecture of \MATITA{} and the peculiarities of its user
   interface.
  \end{abstract}


@@ -114,10 +114,11 @@
 \section{Introduction}
 \label{sec:intro}
 
 \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
 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}
 features.
 
 \subsection{Historical perspective}


@@ -1577,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,
 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)}.
 
 x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
 \texttt{(fun n0: nat => m + n = n0)}.
 


@@ -1755,36 +1757,37 @@ scripts, listed in Tab.~\ref{tab:scripts}.
  \label{tab:scripts}
 \end{table}
 
  \label{tab:scripts}
 \end{table}
 

-\section{Conclusions and future works}
+\section{Conclusions and future work}

 \label{sec:conclusion}
 
 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
 \label{sec:conclusion}
 
 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 techniques and tools.
-Among them, an innovative searching technique that is equally addressed to
-end users and to automatic proof searching procedures; a \MATHML-based
+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
 rendering interface coupled with a disambiguating parser to fully exploit

-the usual mathematical notation, peeking constants and symbols from the
-whole library; direct manipulation of terms, with a corresponding elaborated
-textual syntax to record the user actions; a fine-grained execution of
-tacticals to simplify script structuring and replaying; an integrated
-browser to navigate the hypertext formed by the concepts in the library,
-integrated with natural language rendering of proof; compatibility with
-the library of the Coq proof assistant.
-
-In the near future we plan to continue development focusing on and enhanching
-the peculiarities of \MATITA, starting from its document centric phylosophy.
+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, 
 In particular, 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
+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.
 
 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 medium
-term to attract users to form a critical size community for entering in
+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
 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