From f9a26b56a3945afb2ff6167fcac61a21377bf0cf Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 1 Feb 2006 22:56:18 +0000 Subject: [PATCH] review on csc's latest additions --- helm/papers/matita/matita2.tex | 35 +++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index f3b1a12c3..7eeeb83b5 100644 --- 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 -- 2.39.2