From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 19 Jan 2006 15:48:39 +0000 (+0000)
Subject: Some work...
X-Git-Tag: make_still_working~7811
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7521a4856db25447fbcc50a29eacc61d6b1ad3ab;p=helm.git

Some work...
---

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 94e21bb19..04b7427a7 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -634,6 +634,66 @@ services missing from the standard library of the programming language.
 In particular, the \texttt{xml} \component{} is used
 to easily represent, parse and pretty-print XML files.
 
+\section{Using \MATITA}
+
+\begin{figure}[t]
+ \begin{center}
+  \includegraphics[width=0.9\textwidth]{a.eps}
+  \caption{\MATITA{} screenshot}
+  \label{fig:screenshot}
+ \end{center}
+\end{figure}
+
+\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
+split in two main windows: on the left a textual widget is used to edit the
+script, on the right the list of open goal is shown using a MathML rendering
+widget. A distinguished part of the script (shaded in the screenshot) represent
+the commands already executed and can't be edited without undoing them. The
+remaining part can be freely edited and commands from that part can be executed
+moving down the execution point. An additional window --- the ``cicBrowser'' ---
+can be used to browse the library, including the proof being developed, and
+enable content based search on it. In the cicBrowser proofs are rendered in
+natural language, automatically generated from the low-level $\lambda$-terms
+using techniques inspired by \cite{natural,YANNTHESIS}.
+
+In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
+only seen as a convenient way to create mathematical objects. The universe of
+all these objects makes up the \HELM{} library, which is always completely
+visible to the user. The mathematical library is thus conceived as a global 
+hypertext, where objects may freely reference each other. It is a duty of
+the system to guide the user through the relevant parts of the library. 
+
+This methodological assumption has many important consequences
+which will be discussed in the next section.
+%on one side
+%it requires functionalities for the overall management of the library, 
+%%%%%comprising efficient indexing techniques to retrieve and filter the 
+%information; 
+%on the other it introduces overloading in the use of 
+%identifiers and mathematical notation, requiring sophisticated disambiguation
+%techniques for interpreting the user inputs.  
+%In the next two sections we shall separately discuss the two previous 
+%points. 
+A final section is devoted to some innovative aspects
+of the authoring system, such as a step by step tactical execution, 
+content selection and copy-paste. 
+
+\section{Library Managament}
+\subsection{Indexing and searching}
+\subsection{Developments}
+\subsection{Automation}
+\subsection{Naming}
+\subsection{Disambiguation}
+
+%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
+%organized in components which work on data in this format. For instance the
+%rendering engine, which transform $\lambda$-terms encoded as XML document to
+%MathML Presentation documents, can be used apart from \MATITA{} to print  ...
+%FINIRE
+
+
+
+
 \section{Partially specified terms}
 --- il mondo delle tattiche e dintorni ---
 serve una intro che almeno cita il widget (per i patterns) e che fa