review on csc's latest additions

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

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index f3b1a12c328d6e9545d0f2b02b8d835e99916bad..7eeeb83b53641f7f80afccb7b1bbf20b6e5dcaea 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
-  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}
@@ -1755,28 +1755,29 @@ scripts, listed in Tab.~\ref{tab:scripts}.
  \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
-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
-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, 
-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
@@ -1784,7 +1785,7 @@ 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
+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