overall management of the library, integrating everything into a
single system. \MATITA{} is the result of this effort.
-\subsection{The System}
-DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
-
-\begin{itemize}
- \item scelta del sistema fondazionale
- \item sistema indipendente (da \COQ)
- \item compatibilit\`a con sistemi legacy
-\end{itemize}
-
\subsection{Relationship with \COQ{}}
At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
%be able to contribute to \COQ{}'s code is quite steep and requires direct
%and frequent interactions with \COQ{} developers.
+\subsection{The system}
+
+DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''\\
+ROBA CHE MANCA:
+\begin{itemize}
+ \item scelta del sistema fondazionale
+ \item sistema indipendente (da \COQ)
+ \item compatibilit\`a con sistemi legacy
+\end{itemize}
+
\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.
+
+%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
+
+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{Architecture}
+\label{architettura}
+
+\begin{figure}[ht]
\begin{center}
\includegraphics[width=0.9\textwidth]{librariesCluster.ps}
\caption{\MATITA{} libraries}
\end{center}
\end{figure}
-\section{Architecture}
-\label{architettura}
Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
project.
%In particular, the \texttt{xml} \component{} is used to easily represent,
%parse and pretty-print XML files.
-\section{Using \MATITA (boh \ldots cambiare titolo)}
-
-\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.
-
-%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
-
-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 Management}
\subsection{Indexing and searching}
\subsection{Automation}
-\subsection{\MATITA's naming convention}
+\subsection{Naming convention}
A minor but not entirely negligible aspect of \MATITA{} is that of
adopting a (semi)-rigid naming convention for identifiers, derived by
our studies about metadata for statements.
expression and the suffix \verb+_to_Prop+. In the above example,
\verb+eqb_to_Prop+ is accepted.
-\section{The \MATITA{} user interface}
+\section{User interface}
\subsection{Disambiguation}
\label{sec:disambiguation}
goal) gives you the feeling of what is going on.
\end{description}
-\section{The \MATITA{} library}
+\section{Standard library}
\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
can be read, checked and referenced in further developments.
projects / helm.git / commitdiff