From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 1 Feb 2006 17:57:43 +0000 (+0000)
Subject: Abstract and conclusions.
X-Git-Tag: make_still_working~7699
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ae585c99c2e9d9b7c9c100b11a18c220bfbd4e8;p=helm.git

Abstract and conclusions.
---

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index e8d55f5a1..f3b1a12c3 100644
--- 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 techniques and tools. 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,8 +110,6 @@
 
 % toc & co: to be removed in the final paper version
 \tableofcontents
-\listoffigures
-\listoftables
 
 \section{Introduction}
 \label{sec:intro}
@@ -1754,16 +1755,40 @@ 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 works}
 \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 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
+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.
+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
+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
+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