% \end{motto}
\begin{abstract}
- \TODO{scrivere abstract}
+ \MATITA{} is a new document-centric proof assistant that integrates several
+ Mathematical Knowledge Management tools and techniques. 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,
% toc & co: to be removed in the final paper version
\tableofcontents
-\listoffigures
-\listoftables
\section{Introduction}
\label{sec:intro}
-\MATITA{} is the Proof Assistant under development by the \HELM{}
+\MATITA is the Proof Assistant under development by the \HELM{}
team~\cite{mkm-helm} at the University of Bologna, under the direction of
-Prof.~Asperti. This paper describes the overall architecture of
-the system, focusing on its most distinctive and innovative
+Prof.~Asperti. \MATITA{} is free software, the source code is available for
+download at \url{http://matita.cs.unibo.it}. This paper describes the overall
+architecture of the system, focusing on its most distinctive and innovative
features.
\subsection{Historical perspective}
The authoring interface of \MATITA{} is very similar to Proof
General~\cite{proofgeneral}. We
chose not to build the \MATITA{} UI over Proof General for two reasons. First
-of all we wanted to integrate our XML-based rendering technologies, mainly
-\GTKMATHVIEW, in the UI.
+of all we wanted to integrate in the UI our rendering technologies, mainly
+\GTKMATHVIEW, to render sequents exploiting the bidimensional mathematical layouts
+of \MATHML-Presentation.
At the time of writing Proof General supports only text based
rendering.\footnote{This may change with future releases of Proof General
-based on Eclipse (\url{http://www.eclipse.org/}), but is not yet the
-case.} The second reason is that we wanted
+based on Eclipse (\url{http://www.eclipse.org/}).} The second reason is that we wanted
to build the \MATITA{} UI on top of a state-of-the-art and widespread graphical
toolkit as \GTK{} is.
-Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
-featuring two windows. The background one is very like to the Proof General
-interface. The main difference is that we use the \GTKMATHVIEW{} widget to
-render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
-advantage of the whole bidimensional mathematical notation. The foreground
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface.
+The foreground
window is an instance of the cicBrowser (see Sect.~\ref{sec:library}) used to
-render in natural language the proof being developed.
+render in natural language the proof under development.
Note that the syntax used in the script view is \TeX-like, but
Unicode\footnote{\url{http://www.unicode.org/}} is
\end{figure}
Since the concepts of script based proof authoring are well-known, the
-remaining part of this section is dedicated to the distinguishing
+remaining part of this section is devoted to the distinguishing
features of the \MATITA{} authoring interface.
\subsection{Direct manipulation of terms}
pattern n at 2 in H
\end{grafite}
would have resulted in the sequent:
-\sequent{n: nat\\m : nat\\H: (fun n0: nat => m + n = n0) n}{m = 0}
+\sequent{n: nat\\m : nat\\H: (fun~n0: nat => m + n = n0)~n}{m = 0}
where \texttt{H} is $\beta$-expanded over the second \texttt{n}
occurrence.
At this point, since \COQ{} unification algorithm is essentially first-order,
-the application of an elimination principle (of the form $\forall P.\forall
+the application of an elimination principle (a term of type\linebreak
+$\forall P.\forall
x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
\texttt{(fun n0: nat => m + n = n0)}.
-Since \TAC{rewrite}, \TAC{replace} and several other tactics boils down to
+Since \TAC{rewrite}, \TAC{replace} and several other tactics boil down to
the application of the equality elimination principle, the previous
trick implements the expected behavior.
The idea behind this way of identifying subterms in not really far
from the idea behind patterns, but fails in extending to
complex notation, since it relies on a mono-dimensional sequent representation.
-Real math notation places arguments upside-down (like in indexed sums or
+Real mathematical notation places arguments upside-down (like in indexed sums or
integrations) or even puts them inside a bidimensional matrix.
In these cases using the mouse to select the wanted term is probably the
more effective way to tell the system what to do.
-
-One of the goals of \MATITA{} is to use modern publishing techniques, and
-adopting a method for restricting tactics application domain that discourages
-using heavy math notation would have definitively been a bad choice.
+One of the goals of \MATITA{} is to use modern publishing techniques,
+so we prefer our method that does not discourage the use of complex layout schemata.
In \MATITA{}, tactics accepting pattern arguments can be more expressive than
the equivalent tactics in \COQ{} since variables bound in the pattern context,
change in H: \forall _. (? ? % ?) with (S m) * n.
\end{grafite}
to change $n+m*n$ with $(S~m)*n$. To achieve the same effect in \COQ, the
-user is obliged to change the whole hypothesis rewriting its right hand side
+user is forced to change the whole hypothesis rewriting its right hand side
as well.
\subsection{Tacticals}
\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 work}
\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 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, 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 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
+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\linebreak medium
+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
+usability of the system.
\acknowledgements
We would like to thank all the people that during the past
projects / helm.git / blobdiff