\newcommand{\component}{component}
\newcommand{\components}{components}
-\newcommand{\AUTO}{\textsc{Auto}}
\newcommand{\BOXML}{BoxML}
\newcommand{\COQ}{Coq}
-\newcommand{\COQIDE}{CoqIde}
-\newcommand{\ELIM}{\textsc{Elim}}
\newcommand{\GDOME}{Gdome}
\newcommand{\GTK}{GTK+}
\newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
-\newcommand{\IN}{\ensuremath{\dN}}
-\newcommand{\INSTANCE}{\textsc{Instance}}
-\newcommand{\IR}{\ensuremath{\dR}}
-\newcommand{\IZ}{\ensuremath{\dZ}}
-\newcommand{\LIBXSLT}{LibXSLT}
+% \newcommand{\IN}{\ensuremath{\dN}}
\newcommand{\LEGO}{Lego}
-\newcommand{\LOCATE}{\textsc{Locate}}
-\newcommand{\MATCH}{\textsc{Match}}
\newcommand{\MATHML}{MathML}
\newcommand{\MATITA}{Matita}
\newcommand{\MATITAC}{\texttt{matitac}}
\newcommand{\MATITADEP}{\texttt{matitadep}}
\newcommand{\MOWGLI}{MoWGLI}
\newcommand{\MOWGLIIST}{IST-2001-33562}
-\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
-\newcommand{\NATIND}{\mathit{nat\_ind}}
\newcommand{\NUPRL}{NuPRL}
\newcommand{\OCAML}{OCaml}
-\newcommand{\PROP}{\mathit{Prop}}
\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
\newcommand{\REWRITEHINT}{\textsc{RewriteHint}}
\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
\newcommand{\OP}[1]{``\texttt{#1}''}
\newcommand{\FILE}[1]{\texttt{#1}}
\newcommand{\TAC}[1]{\texttt{#1}}
-\newcommand{\NOTE}[1]{\ednote{#1}{}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
\newcommand{\sequent}[2]{
\savebox{\tmpxyz}[0.9\linewidth]{
\begin{minipage}{0.9\linewidth}
- \texttt{#1} \\
+ \ensuremath{#1} \\
\rule{3cm}{0.03cm}\\
- \texttt{#2}
+ \ensuremath{#2}
\end{minipage}}\setlength{\fboxsep}{3mm}%
\begin{center}
\fcolorbox{black}{gray}{\usebox{\tmpxyz}}
\runningtitle{The \MATITA{} proof assistant}
\runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
- \begin{motto}
- ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
- \end{motto}
+%\begin{motto}
+% ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
+% \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
-
-\TODO{rivedere tutti gli usi di \TEXMACRO{NOTE}}
\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}
35'000 theorems)
was chosen as a privileged test bench for our work, although experiments
have been also conducted with other systems, and notably
-with \NUPRL~\cite{nuprl-book}.\TODO{citare la tesi di vincenzo(?)}
+with \NUPRL~\cite{nuprl-book}.
The work, mostly performed in the framework of the recently concluded
European project \MOWGLIIST{} \MOWGLI~\cite{pechino}, mainly consisted in the
following steps:
language~\cite{remathematization};
\item an innovative, \MATHML-compliant rendering widget~\cite{padovani}
- for the \GTK{} graphical environment,\footnote{\url{http://www.gtk.org/}}
+ for the \GTK{}\footnote{\url{http://www.gtk.org}} graphical environment,
supporting high-quality bidimensional
rendering, and semantic selection, i.e. the possibility to select semantically
meaningful rendering expressions, and to paste the respective content into
others systems
whose proof language is procedural. Traditionally, in a procedural system
the user interacts only with the \emph{script}, while proof terms are internal
-records kept by the system. On the contrary, in \MATITA{} proof terms are
-praised as declarative versions of the proof. Playing that role, they are the
-primary mean of communication of proofs (once rendered to natural language
-for human audiences).
-
-The user interfaces now adopted by all the proof assistants based on a
-procedural proof language have been inspired by the CtCoq pioneering
+records kept by the system.
+In \MATITA{}, which has been conceived for a potentially distributed
+library, proof terms are also meant as the primary representation for
+storage and communication with other systems (e.g. \COQ).
+%On the contrary, in \MATITA{} proof terms are
+%praised as declarative versions of the proof. Playing that role, they are the
+%primary mean of communication of proofs (once rendered to natural language
+%for human audiences).
+
+All the user interfaces currently adopted by proof assistants based on a
+procedural proof language have been influenced by the CtCoq pioneering
system~\cite{ctcoq1}. One successful incarnation of the ideas introduced
by CtCoq is the Proof General generic interface~\cite{proofgeneral},
that has set a sort of
-standard way to interact with the system. Several procedural proof assistants
-have either adopted or cloned Proof General as their main user interface.
-The authoring interface of \MATITA{} is a clone of the Proof General interface.
+standard way to interact with the system.
+%Several procedural proof assistants
+%have either adopted or cloned Proof General as their main user interface.
+The authoring interface of \MATITA{} essentially offers the same
+functionalities of the Proof General interface or CoqIde.
On the contrary, the interface to interact with the library is rather
innovative and directly inspired by the Web interfaces to our Web servers.
Calculus of (Co)Inductive Constructions), the same implementation
language (\OCAML\footnote{\url{http://caml.inria.fr/}}),
and the same (procedural, script based) authoring philosophy.
-However, the analogy essentially stops here and no code is shared
-between the two systems.
+However, the analogy essentially stops here; in particular, no code is shared
+between the two systems and the algorithms are often different.
In a sense, we like to think of \MATITA{} as the way \COQ{} would
look like if entirely rewritten from scratch: just to give an
the parser for ambiguous mathematical notation.
The size and complexity improvements over \COQ{} must be understood
-historically. \COQ{}\cite{CoqArt} is a quite old
+historically. \COQ~\cite{CoqArt} is a quite old
system whose development started 20 years ago. Since then,
several developers have took over the code and several new research ideas
-that were not considered in the original architecture have been experimented
+and optimizations that were not considered in the original architecture
+have been experimented
and integrated in the system. Moreover, there exists a lot of developments
for \COQ{} that require backward compatibility between each pair of releases;
since many central functionalities of a proof assistant are based on heuristics
or arbitrary choices to overcome undecidability (e.g. for higher order
unification), changing these functionalities maintaining backward compatibility
-is very difficult. Finally, the code of \COQ{} has been greatly optimized
-over the years; optimization reduces maintainability and rises the complexity
-of the code.
+is very difficult.
+%Finally, the code of \COQ{} has been greatly optimized
+%over the years; optimization reduces maintainability and rises the complexity
+%of the code.
In writing \MATITA{} we have not been hindered by backward compatibility and
we have took advantage of the research results and experiences previously
depend on a restricted set of \components.
Only the proof assistant \MATITA{} and the \WHELP{} search engine are
-applications meant to be used directly by the user. All the other applications
-are Web services developed in the \HELM{} and \MOWGLI{} projects and already
-described elsewhere. In particular:
+applications meant to be used directly by the user; all the other applications
+are Web services developed in the \HELM{} and \MOWGLI{} projects. The
+following applications have already been described elsewhere:
\begin{itemize}
\item The \emph{\GETTER}~\cite{zack-master} is a Web service to
The Proof Checker application is the Web service that provides an interface
to the \texttt{cic\_proof\_checking} \component.
- We use metadata and a sort of crawler to index the mathematical concepts
+ We use metadata to index the mathematical concepts
in the distributed library. We are interested in retrieving a concept
by matching, instantiation or generalization of a user or system provided
mathematical formula. Thus we need to collect metadata over the fully
The \texttt{whelp} \component{} implements a search engine that performs
approximated queries by matching/instantiation/generalization. The queries
operate only on the metadata and do not involve any actual matching
- (see the \texttt{cic\_unification} \component in
+ (see the \texttt{cic\_unification} \component{} in
Sect.~\ref{sec:partiallyintro}). Not performing any actual matching
a query only returns a complete and hopefully small set of matching
candidates. The process that has issued the query is responsible of
\label{sec:partiallyintro}
\emph{Partially specified terms} are CIC terms where subterms can be omitted.
-Omitted subterms can bear no information at all or they may be associated to
-a sequent. The formers are called \emph{implicit terms} and they occur only
-linearly. The latters may occur multiple times and are called
-\emph{metavariables}. An \emph{explicit substitution} is applied to each
-occurrence of a metavariable. A metavariable stands for a term whose type is
+Omitted subterms come in two flavours:
+\emph{implicit terms} that do not require a declaration, but can only occur
+linearly; and \emph{metavariables}~\cite{geuvers-jojgov,munoz} whose declaration
+associates with them a sequent and whose occurrences are coupled with an
+explicit substitution.
+A metavariable stands for a term whose type is
given by the conclusion of the sequent. The term must be closed in the
context that is given by the ordered list of hypotheses of the sequent.
The explicit substitution instantiates every hypothesis with an actual
metavariables and that can introduce
\emph{implicit coercions}~\cite{barthe95implicit} to make a
partially specified term well-typed. The refiner of \MATITA{} is implemented
-in the \texttt{cic\_unification} \component. As the type checker is based on
-the conversion check, the refiner is based on \emph{unification} that is
-a procedure that makes two partially specified term convertible by instantiating
-as few as possible metavariables that occur in them.
+in the \texttt{cic\_unification} \component. In the same way as the
+type checker is based on
+convertibility, the refiner is based on \emph{unification}~\cite{strecker}
+that is a procedure that makes two partially specified term convertible by
+instantiating as few metavariables as possible that occur in them.
Since terms are used in CIC to represent proofs, correct incomplete
proofs are represented by refinable partially specified terms. The metavariables
\label{sec:contentintro}
The language used to communicate proofs and especially formulae with the
-user does not only needs to be extendible and accommodate the usual mathematical
-notation. It must also reflect the comfortable degree of imprecision and
-ambiguity that the mathematical language provides.
+user does not only need to be extendible and accommodate the usual mathematical
+notation. It must also reflect the comfortable and suggestive degree of
+notational abuse so typical of the mathematical language.
For instance, it is common practice in mathematics to speak of a generic
equality that can be used to compare any two terms. However, it is well known
those of addition over the unary representation. And addition over two natural
numbers is definitely different from addition over two real numbers.
-Formalized mathematics cannot hide these differences and obliges the user to be
+Formalized mathematics cannot hide these differences and forces the user to be
very precise on the types he is using and their representation. However,
to communicate formulae with the user and with external tools, it seems good
practice to stick to the usual imprecise mathematical ontology. In the
the \emph{content level}~\cite{adams} representation of formulae.
In \MATITA{} we provide translations from partially specified terms
-to content level terms and the other way around. The first translation can also
-be applied to fully specified terms since a fully specified term is a special
-case of partially specified term where no metavariable or implicit term occurs.
-
-The translation from partially specified terms to content level terms must
+to content level terms and the other way around.
+The former translation must
discriminate between terms used to represent proofs and terms used to represent
-formulae. The firsts are translated to a content level representation of
-proof steps that can in turn easily be rendered in natural language
-using techniques inspired by~\cite{natural,YANNTHESIS}. The representation
+formulae. Using techniques inspired by~\cite{natural,YANNTHESIS}, the firsts
+are translated to a content level representation of
+proof steps that can in turn easily be rendered in natural language.
+The representation
adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now
isomorphic to it. Terms that represent formulae are translated to \MATHML{}
Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard
The translation to content level is implemented in the
\texttt{acic\_content} \component. Its input are \emph{annotated partially
-specified terms}, that are maximally unshared
+specified terms}, that are
partially specified terms enriched with additional typing information for each
subterm. This information is used to discriminate between terms that represent
proofs and terms that represent formulae. Part of it is also stored at the
content level since it is required to generate the natural language rendering
-of proofs. The terms need to be maximally unshared (i.e. they must be a tree
-and not a DAG). The reason is that to different occurrences of a subterm
-we need to associate different typing information.
-This association is made easier when the term is represented as a tree since
-it is possible to label each node with an unique identifier and associate
-the typing information using a map on the identifiers.
-The \texttt{cic\_acic} \component{} unshares and annotates terms. It is used
+of proofs.
+The \texttt{cic\_acic} \component{} annotates terms. It is used
by the \texttt{library} \component{} since fully specified terms are stored
in the library in their annotated form.
in a command as functions from a context to a partially refined term. The
function is obtained by partially applying our disambiguation function to
the content level term to be disambiguated. Our solution should be compared with
-the one adopted in the \COQ{} system, where ambiguity is only relative to
-De Brujin indexes.
+the one adopted in the \COQ{} system (where ambiguity is only relative to
+De Bruijn indexes).
In \COQ, variables can be bound either by name or by position. A term
occurring in a command has all its variables bound by name to avoid the need of
a context during disambiguation. This makes more complex every
These mechanisms will be further discussed in Sect.~\ref{sec:disambiguation}.
Finally, the \texttt{grafite\_parser} \component{} implements a parser for
-the concrete syntax of the commands of \MATITA. The parser process a stream
+the concrete syntax of the commands of \MATITA. The parser processes a stream
of characters and returns a stream of abstract syntax trees (the ones
defined by the \texttt{grafite} component and whose semantics is given
by \texttt{grafite\_engine}). When the parser meets a command that changes
\label{sec:library}
A proof assistant provides both an interface to interact with its library and
-an \emph{authoring} interface to develop new proofs and theories. According
+an authoring interface to develop new proofs and theories. According
to its historical origins, \MATITA{} strives to provide innovative
functionalities for the interaction with the library. It is more traditional
in its script based authoring interface. In the remaining part of the paper we
library. To this aim, \MATITA{} uses a sophisticated indexing mechanism
for mathematical concepts, based on a rich metadata set that has been
tuned along the European project \MOWGLIIST{} \MOWGLI. The metadata
-set, and the searching facilites built on top of them --- collected
+set, and the searching facilities built on top of them --- collected
in the so called \WHELP{} search engine --- have been
extensively described in~\cite{whelp}. Let us just recall here that
-the \WHELP{} metadata model is essentially based a single ternary relation
+the \WHELP{} metadata model is essentially based on a single ternary relation
\REF{p}{s}{t} stating that a concept $s$ refers a concept $t$ at a
given position $p$, where the position specify the place of the
occurrence of $t$ inside $s$ (we currently work with a fixed set of
indexed, and becomes immediately visible in the library. Several
interesting and innovative features of \MATITA{} described in the following
sections rely in a direct or indirect way on its metadata system and
-the search features. Here, we shall just recall some of its most
+the search functionalities. Here, we shall just recall some of its most
direct applications.
-A first, very simple but not negligeable feature is the \emph{duplicate check}.
+A first, very simple but not negligible feature is the \emph{duplicate check}.
As soon as a theorem is stated, just before starting its proof,
the library is searched
to check that no other equivalent statement has been already proved
(based on the pattern matching functionality of \WHELP); if this is the case,
a warning is raised to the user. At present, the notion of equivalence
adopted by \MATITA{} is convertibility, but we may imagine to weaken it
-in the future, covering for instance isomorphisms.
+in the future, covering for instance isomorphisms~\cite{delahaye}.
Another useful \WHELP{} operation is \HINT; we may invoke this query
at any moment during the authoring of a proof, resulting in the list
Software applications that involve input of mathematical content should strive
to require the user as less drift from informal mathematics as possible. We
believe this to be a fundamental aspect of such applications user interfaces.
-Being that drift in general very large when inputing
-proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
-mathematical formulae which can be input using a \TeX-like encoding (the
-concrete syntax corresponding to presentation level terms) and are then
+The drift is still very large for
+proofs~\cite{debrujinfactor}, while better results may be achieved for
+mathematical formulae. In \MATITA{} formulae can be written using a
+\TeX-like syntax (corresponding to presentation level terms) and are then
translated (in multiple steps) to partially specified terms as sketched in
Sect.~\ref{sec:contentintro}.
some of its parameters, helps in keeping the input terse without sacrificing
expressiveness.
-\subsubsection{Disambiguation aliases}
+\subsubsection{Disambiguation preferences}
\label{sec:disambaliases}
Consider the following command that states a theorem over integer numbers:
\begin{grafite}
theorem Zlt_compat:
- \forall x, y, z. x < y \to y < z \to x < z.
+ \forall x,y,z. x < y \to y < z \to x < z.
\end{grafite}
The symbol \OP{<} is likely to be overloaded in the library
with the same source. It is possible to record \emph{disambiguation
preferences} to select one of the aliases of an overloaded source.
-Preferences can be explicitely given in the script (using the
-misleading \texttt{alias} commands), but
+Preferences can be explicitly given in the script (using the \texttt{alias}
+command), but
are also implicitly added when a new concept is introduced (\emph{implicit
-preferences}) or after a sucessfull disambiguation that did not require
+preferences}) or after a successful disambiguation that did not require
user interaction. Explicit preferences are added automatically by \MATITA{} to
record the disambiguation choices of the user. For instance, after the
disambiguation of the command above, the script is altered as follows:
\begin{grafite}
alias symbol "lt" = "integer 'less than'".
theorem Zlt_compat:
- \forall x, y, z. x < y \to y < z \to x < z.
+ \forall x,y,z. x < y \to y < z \to x < z.
\end{grafite}
The ``alias'' command in the example sets the preferred alias for the
When starting a new authoring session the set of disambiguation preferences
is empty. Until it contains a preference for each overloaded symbol to be
used in the script, the user can be faced with questions from the disambiguator.
-To reduce the likelyhood of user interactions, we introduced
+To reduce the likelihood of user interactions, we introduced
the \texttt{include} command. With \texttt{include} it is possible to import
at once in the current session the set of preferences that was in effect
at the end of the execution of a given script.
+The inclusion mechanism is thus sensibly different from that of other systems
+where concepts are effectively loaded and made visibible by inclusion; in \MATITA{}
+all concepts are always visible, and inclusion, that is optional, is only used
+to set up preferences.
-Preferences can be changed. For instance, at the start of the development
+Preferences can be changed. For instance, at the beginning of the development
of integer numbers the preference for the symbol \OP{<} is likely
to be the one over natural numbers; sooner or later it will be set to the one
over integer numbers.
Consider, for example:
\begin{grafite}
theorem Zlt_mono:
- \forall x, y, k. x < y \to x < y + k.
+ \forall x,y,k. x < y \to x < y + k.
\end{grafite}
No refinable partially specified term corresponds to the preferences:
\OP{+} over natural numbers, \OP{<} over integer numbers. To overcome this
limitation we organized disambiguation in \emph{multiple passes}: when the
-disambiguator fails, disambiguation is tried again with a less strict set of
+disambiguator fails, disambiguation is tried again with a less restrictive set of
preferences.
Several disambiguation parameters can vary among passes. With respect to
\subsubsection{Operator instances}
\label{sec:disambinstances}
-Consider now the following theorem:
+Consider now the following theorem, where \texttt{pos} injects natural numbers
+into positive integers:
+
\begin{grafite}
theorem lt_to_Zlt_pos_pos:
- \forall n, m: nat. n < m \to pos n < pos m.
+ \forall n,m: nat. n < m \to pos n < pos m.
\end{grafite}
and assume that there exist in the library aliases for \OP{<} over natural
numbers and over integer numbers. None of the passes described above is able to
this reason we always attempt a fresh instances pass only after attempting a
shared instances pass.
-\paragraph{One-shot preferences} Disambiguation preferences as seen so far are
-instance-independent. However, implicit preferences obtained as a result of a
-disambiguation pass which uses fresh instances ought to be instance-dependent.
-Informally, the set of preferences that can be respected by the disambiguator on
-the theorem above is: ``the first instance of the \OP{<} symbol is over natural
-numbers, while the second is on integer numbers''.
+%\paragraph{One-shot preferences} Disambiguation preferences as seen so far are
+%instance-independent. However, implicit preferences obtained as a result of a
+%disambiguation pass which uses fresh instances ought to be instance-dependent.
+%Informally, the set of preferences that can be respected by the disambiguator on
+%the theorem above is: ``the first instance of the \OP{<} symbol is over natural
+%numbers, while the second is on integer numbers''.
Instance-dependent preferences are meaningful only for the term whose
-disambiguation generated it. For this reason we call them \emph{one-shot
+disambiguation generated them. For this reason we call them \emph{one-shot
preferences} and \MATITA{} does not use them to disambiguate further terms in
the script.
Consider the following theorem about derivation:
\begin{grafite}
theorem power_deriv:
- \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
+ \forall n: nat, x: R. d x^n dx = n * x^(n - 1).
\end{grafite}
and assume that in the library there is an alias mapping \OP{\^} to a partially
specified term having type: \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}. In
coercion from \texttt{nat} to \texttt{R} appears (assuming such a coercion has
been defined in advance).
-Implicitc coercions are not always desirable. For example, in disambiguating
-\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses
-2 coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
-among the possible partially specified term choices. For this reason we always
-attempt a disambiguation pass which require the refiner not to use the coercions
-before attempting a coercion-enabled pass.
-
-The choice of whether implicit coercions are enabled or not interact with the
+Implicit coercions are not always desirable. For example, consider the term
+\texttt{\TEXMACRO{forall} x. x < x + 1} and assume that the preferences for \OP{<}
+and \OP{+} are over real numbers. The expected interpretation assignes the
+type \texttt{R} to \texttt{x}.
+However, if we had a coercion from natural to real numbers an alternative
+interpretation is to assign the type \texttt{nat} to \texttt{x} inserting the coercion
+as needed. Clearly, the latter interpretation looks artificial and
+for this reason we enable coercions only in case of failure of previous
+attempts.
+
+The choice of whether implicit coercions are enabled or not interacts with the
choice about operator instances. Indeed, consider again
\texttt{lt\_to\_Zlt\_pos\_pos}, which can be disambiguated using fresh operator
-instances. In case there exists a coercion from natural numbers to (positive)
-integers (which indeed does), the
-theorem can be disambiguated using twice that coercion on the left hand side of
-the implication. The obtained partially specified term however would not
-probably be the expected one, being a theorem which proves a trivial
-implication.
-Motivated by this and similar examples we choose to always prefer fresh
-instances over implicit coercions, i.e. we always attempt disambiguation
-passes with fresh instances
-and no implicit coercions before attempting passes with implicit coercions.
+instances. In case there exists a coercion from natural numbers to positive
+integers ({\texttt{pos} itself), the command
+can be disambiguated as
+\texttt{\TEXMACRO{forall} n,m: nat. pos n < pos m \TEXMACRO{to} pos n < pos m}.
+This is not the expected interpretation;
+by this and similar examples we choose to always prefer fresh
+instances over implicit coercions.
\subsubsection{Disambiguation passes}
\label{sec:disambpasses}
According to the criteria described above, in \MATITA{} we perform the
disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
-our experience that choice gives reasonable performance and minimizes the need
+our experience that choice gives reasonable performance and reduces the need
of user interaction during the disambiguation.
\begin{table}[ht]
- \caption{Disambiguation passes sequence\strut}
- \label{tab:disambpasses}
\begin{center}
\begin{tabular}{c|c|c|c}
\multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
- & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Preferences}}
+ & \multicolumn{1}{p{3.1cm}|}{\centering\raisebox{-1.5ex}{\textbf{Preferences}}}
& \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
& \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
\hline
\PASS & Library-preferences & Fresh instances & Enabled
\end{tabular}
\end{center}
+ \caption{Disambiguation passes sequence\strut}
+ \label{tab:disambpasses}
\end{table}
-\subsection{Generation and invalidation}
+\subsection{Invalidation and regeneration}
\label{sec:libmanagement}
%The aim of this section is to describe the way \MATITA{}
Invalidation (see Sect.~\ref{sec:library}) is implemented in two phases.
-The first one is the calculation of all the concepts that recursively
+The first one is the computation of all the concepts that recursively
depend on the ones we are invalidating. It can be performed
-using the relational database that stores the metadata.
+from the metadata stored in the relational database.
This technique is the same used by the \emph{Dependency Analyzer}
and is described in~\cite{zack-master}.
literal of included explicit disambiguation preferences
(see Sect.~\ref{sec:disambaliases}).
-\TODO{da rivedere: da dove salta fuori ``regenerating content''?}
-Regenerating the content of a modified script file involves the preliminary
-invalidation of all its old content.
+The re-execution of a script to regenerate part of the library
+requires the preliminary invalidation of the concepts generated by the
+script.
\subsubsection{Batch vs Interactive}
user, the latter is automatically invoked by \MATITA{}
to regenerate parts of the library previously invalidated.
-\TODO{come sopra: ``content of a script''?}
While they share the same engine for generation and invalidation, they
provide different granularity. \MATITAC{} is only able to re-execute a
-whole script and similarly to invalidate the whole content of a script
-(together with all the other scripts that rely on a concept defined
+whole script and similarly to invalidate all the concepts generated
+by a script (together with all the other scripts that rely on a concept defined
in it).
\subsection{Automation}
main parameters: the \emph{depth} (whit the obvious meaning), and the
\emph{width} that is the maximum number of (new) open goals allowed at
any instant. \MATITA{} has only one notion of metavariable, corresponding
-to the so called existential variables of Coq; so, \MATITA's \TAC{auto}
+to the so called existential variables of \COQ; so, \MATITA's \TAC{auto}
tactic should be compared with \COQ's \TAC{EAuto} tactic.
Recently we have extended automation with paramodulation based
facts and a new \emph{given} clause suitably selected from a set of passive
equations. The latter tries to simplify the equations
orienting them according to a suitable weight associated to terms.
-\MATITA{} currently supports several different weigthing functions
+\MATITA{} currently supports several different weighting functions
comprising Knuth-Bendix ordering (kbo) and recursive path ordering (rpo),
that integrates particularly well with normalization.
theorem example1:
\forall x: nat. (x+1)*(x-1) = x*x - 1.
intro.
-apply (nat_case x)
-[ simplify; reflexivity;
-| intro; demodulate; reflexivity; ]
+apply (nat_case x);
+ [ simplify; reflexivity
+ | intro; demodulate; reflexivity ]
qed.
\end{grafite}
\begin{grafite}
theorem example2:
- \forall x, y: nat. (x+y)*(x+y) = x*x + 2*x*y + y*y.
-intros; demodulate; reflexivity;
+ \forall x,y: nat. (x+y)*(x+y) = x*x + 2*x*y + y*y.
+intros; demodulate; reflexivity
qed.
\end{grafite}
Take for instance the statement:
\begin{grafite}
- \forall n: nat. n = plus n O
+\forall n: nat. n = plus n O
\end{grafite}
Possible legal names are: \texttt{plus\_n\_O}, \texttt{plus\_O},
\texttt{eq\_n\_plus\_n\_O} and so on.
-Similarly, consider the theorem:
+Similarly, consider the statement
\begin{grafite}
- \forall n, m: nat. n < m to n \leq m
+\forall n,m: nat. n < m to n \leq m
\end{grafite}
In this case \texttt{lt\_to\_le} is a legal name,
while \texttt{lt\_le} is not.
in this case, is the following. You should start with defining the
symmetric property for relations:
\begin{grafite}
-definition symmetric =
- \lambda A: Type. \lambda R. \forall x, y: A.
- R x y \to R y x
+definition symmetric \def
+ \lambda A: Type. \lambda R. \forall x,y: A.
+ R x y \to R y x.
\end{grafite}
Then, you may state the symmetry of equality as:
\begin{grafite}
match expression.
A typical example is the following:
\begin{grafite}
-\forall n,m:nat.
+\forall n,m: nat.
match (eqb n m) with
[ true \Rightarrow n = m
- | false \Rightarrow n \neq m]
+ | false \Rightarrow n \neq m ]
\end{grafite}
where \texttt{eqb} is boolean equality.
In this cases, the name can be build starting from the matched
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}
$\NT{multipath}$ is omitted the whole assumption is selected. Remember that
the user can be mostly unaware of patterns concrete syntax, since the system
is able to write down a \NT{sequent\_path} starting from a graphical
- selection.\NOTE{Questo ancora non va in matita}
+ selection.
A \NT{multipath} is a CIC term in which a special constant \OP{\%} is allowed.
The roots of discharged subterms are marked with \OP{?}, while \OP{\%} is used
\end{description}
\subsubsection{Examples}
-%To explain how the first phase works let us give an example. Consider
-%you want to prove the uniqueness of the identity element $0$ for natural
-%sum, and that you can rely on the previously demonstrated left
-%injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
-%Typing
-%\begin{grafite}
-%theorem valid_name: \forall n,m. m + n = n \to m = O.
-% intros (n m H).
-%\end{grafite}
Consider the following sequent:
\sequent{n: nat\\m: nat\\H: m + n = n}{m = O}
-To change the right part of the equality of the \texttt{H}
-hypothesis with \texttt{O + n}, the user selects and pastes it as the pattern
+To change the right part of the equality of the $H$
+hypothesis with $O + n$, the user selects and pastes it as the pattern
in the following statement.
\begin{grafite}
change in H:(? ? ? %) with (O + n).
\end{grafite}
-To understand the pattern (or produce it by hand) the user should be
-aware that the notation \texttt{m + n = n} hides the term
-\texttt{eq nat (m + n) n}, so
-that the pattern selects only the third argument of \texttt{eq}.
+To understand the pattern (or produce it by hand) the user should be aware that
+the notation $m + n = n$ hides the term $\mathrm{eq}~\mathrm{nat}~(m + n)~n$, so
+that the pattern selects only the third argument of $\mathrm{eq}$.
-The experienced user may also write by hand a concise pattern
-to change at once all the occurrences of \texttt{n} in the hypothesis
-\texttt{H}:
+The experienced user may also write by hand a concise pattern to change at once
+all the occurrences of $n$ in the hypothesis $H$:
\begin{grafite}
change in H match n with (O + n).
\end{grafite}
-In this case the \NT{sequent\_path} selects the whole \texttt{H}, while
-the second phase locates \texttt{n}.
+In this case the \NT{sequent\_path} selects the whole $H$, while
+the second phase locates $n$.
The latter pattern is equivalent to the following one, that the system
can automatically generate from the selection.
change in H:(? ? (? ? %) %) with (O + n).
\end{grafite}
-\subsubsection{Tactics supporting patterns}
-
-\TODO{Grazie ai pattern, rispetto a Coq noi abbiamo per esempio la possibilita' di fare riduzioni profonde!!!}
-
-\TODO{mergiare con il successivo facendo notare che i patterns sono una
-interfaccia comune per le tattiche}
-
-In \MATITA{} all the tactics that can be restricted to subterms of the current
-sequent accept the pattern syntax. These tactics are:
-\TAC{simplify}, \TAC{change}, \TAC{fold}, \TAC{unfold}, \TAC{generalize},
-\TAC{replace} and \TAC{rewrite}.
+\subsubsection{Comparison with \COQ{}}
-\NOTE{attualmente rewrite e fold non supportano fase 2. per
-supportarlo bisogna far loro trasformare il pattern phase1+phase2
-in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
-con una pattern\_of(select(pattern))}
+In \MATITA{} all the tactics that act on subterms of the current sequent
+accept pattern arguments. Additional arguments can be disambiguated in the
+contexts of the terms selected by the pattern
+(\emph{context-dependent arguments}).
-\subsubsection{Comparison with \COQ{}}
+%\NOTE{attualmente rewrite e fold non supportano fase 2. per
+%supportarlo bisogna far loro trasformare il pattern phase1+phase2
+%in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
+%con una pattern\_of(select(pattern))}
\COQ{} has two different ways of restricting the application of tactics to
subterms of the current sequent, both relying on the same special syntax to
\begin{grafite}
pattern n at 2 in H
\end{grafite}
-would have resulted in this sequent:
-\sequent{n: nat\\m : nat\\H: (fun n0: nat => m + n = n0) n}{m = 0}
+would have resulted in the sequent:
+\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 behaviour.
+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,
+can occur in context-dependent arguments. For example, consider the sequent:
+\sequent{n: nat\\x: nat\\H: \forall m. n + m*n = x + m}{m = O}
+In \MATITA{} the user can issue the command:
+\begin{grafite}
+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 forced to change the whole hypothesis rewriting its right hand side
+as well.
\subsection{Tacticals}
\label{sec:tinycals}
-%There are mainly two kinds of languages used by proof assistants to recorder
-%proofs: tactic based and declarative. We will not investigate the philosophy
-%around the choice that many proof assistant made, \MATITA{} included, and we
-%will not compare the two different approaches. We will describe the common
-%issues of the tactic-based language approach and how \MATITA{} tries to solve
-%them.
-
The procedural proof language implemented in \MATITA{} is pretty standard,
with a notable exception for tacticals.
-%\subsubsection{Tacticals overview}
-
Tacticals first appeared in LCF~\cite{lcf} as higher order tactics.
They can be seen as control flow constructs like looping, branching,
error recovery and sequential composition.
Qed.
\end{grafite}
-The third command is an application of the sequencing tactical \OP{..~;~..},
+The third command is an application of the sequencing tactical \OP{$\ldots$~;~$\ldots$},
that combines the tactic \TAC{split} with the application of the branching
-tactical \OP{..~;[~..~|~..~|~..~]} to other tactics or tacticals.
+tactical \OP{$\ldots$~;[~$\ldots$~|~$\ldots$~|~$\ldots$~]} to other tactics or tacticals.
The usual implementation of tacticals executes them atomically as any
other command. In \MATITA{} this is not the case: each punctuation
symbol is executed as a single command.
-%The latter is applied to all the goals opened by \texttt{split}
-%
-%(here we have two goals, the two sides of the logic and). The first
-%goal $B$ (with $A$ in the context) is proved by the first sequence of
-%tactics \texttt{rewrite} and \texttt{assumption}. Then we move to the
-%second goal with the separator ``\texttt{|}''.
-%
-%Giving serious examples here is rather difficult, since they are hard
-%to read without the interactive tool. To help the reader in
-%understanding the following considerations we just give few common
-%usage examples without a proof context.
-%
-%\begin{grafite}
-% elim z; try assumption; [ ... | ... ].
-% elim z; first [ assumption | reflexivity | id ].
-%\end{grafite}
-%
-%The first example goes by induction on a term \texttt{z} and applies
-%the tactic \texttt{assumption} to each opened goal eventually recovering if
-%\texttt{assumption} fails. Here we are asking the system to close all
-%trivial cases and then we branch on the remaining with ``\texttt{[}''.
-%The second example goes again by induction on \texttt{z} and tries to
-%close each opened goal first with \texttt{assumption}, if it fails it
-%tries \texttt{reflexivity} and finally \texttt{id}
-%that is the tactic that leaves the goal untouched without failing.
-%
-%Note that in the common implementation of tacticals both lines are
-%compositions of tacticals and in particular they are a single
-%statement (i.e. derived from the same non terminal entry of the
-%grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
-%this is not true, since each atomic tactic or punctuation is considered
-%a single statement.
-
-\subsubsection{Common issues of tactic-based proof languages}
-We will examine the two main problems of tactic-based proof scripts:
+\subsubsection{Common issues of tacticals}
+We will examine the two main problems of procedural proof languages:
maintainability and readability.
-%Huge libraries of formal mathematics have been developed, and backward
-%compatibility is a really time consuming task. \\
-%A real-life example in the history of \MATITA{} was the reordering of
-%goals opened by a tactic application. We noticed that some tactics
-%were not opening goals in the expected order. In particular the
-%\texttt{elim} tactic on a term of an inductive type with constructors
-%$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
-%\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
-%but some theorems about integers were there. The inductive type of
-%$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
-%induction proofs on this type where written without tacticals and,
-%obviously, considering the three induction cases in the wrong order.
-%Fixing the behavior of the tactic broke the library and two days of
-%work were needed to make it compile again. The whole time was spent in
-%finding the list of tactics used to prove the third induction case and
-%swap it with the list of tactics used to prove the second case. If
-%the proofs was structured with the branch tactical this task could
-%have been done automatically.
-%
-%From this experience we learned that the use of tacticals for
-%structuring proofs gives some help but may have some drawbacks in
-%proof script readability.
-
Tacticals are not only used to make scripts shorter by factoring out
common cases and repeating commands. They are the primary way of making
scripts more maintainable. They also have the well-known duty of
However, authoring a proof structured with tacticals is annoying.
Consider for example a proof by induction, and imagine you
-are using one of the state of the art graphical interfaces for proof assistant:
-Proof General. After applying the induction principle you have to choose:
+are using one of the state of the art graphical interfaces for proof assistant
+like Proof General. After applying the induction principle you have to choose:
immediately structure the proof or postpone the structuring.
If you decide for the former you have to apply the branching tactical and write
at once tactics for all the cases. Since the user does not even know the
To show the intermediate steps, the proof must be de-structured on the
fly, for example replacing \OP{;} with \OP{.} where possible.
-%Proof scripts
-%readability is poor by itself, but in conjunction with tacticals it
-%can be nearly impossible. The main cause is the fact that in proof
-%scripts there is no trace of what you are working on. It is not rare
-%for two different theorems to have the same proof script.\\
-%Bad readability is not a big deal for the user while he is
-%constructing the proof, but is considerably a problem when he tries to
-%reread what he did or when he shows his work to someone else. The
-%workaround commonly used to read a script is to execute it again
-%step-by-step, so that you can see the proof goal changing and you can
-%follow the proof steps. This works fine until you reach a tactical. A
-%compound statement, made by some basic tactics glued with tacticals,
-%is executed in a single step, while it obviously performs lot of proof
-%steps. In the fist example of the previous section the whole branch
-%over the two goals (respectively the left and right part of the logic
-%and) result in a single step of execution. The workaround does not work
-%anymore unless you de-structure on the fly the proof, putting some
-%``\texttt{.}'' where you want the system to stop.\\
-
-%Now we can understand the tradeoff between script readability and
-%proof structuring with tacticals. Using tacticals helps in maintaining
-%scripts, but makes it really hard to read them again, cause of the way
-%they are executed.
-
\MATITA{} has a peculiar tacticals implementation that provides the
same benefits as classical tacticals, while not burdening the user
during proof authoring and re-playing.
-%\MATITA{} uses a language of tactics and tacticals, but tries to avoid
-%this tradeoff, alluring the user to write structured proof without
-%making it impossible to read them again.
-
\subsubsection{The \MATITA{} approach}
\begin{table}
::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
\NT{block\_kind} &
::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
- \NT{block\_delimiter} &
+ \NT{block\_delim} &
::= & \verb+begin+ ~|~ \verb+end+ & \\
- \NT{tactical} &
- ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
+ \NT{command} &
+ ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delim} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} \\
\end{array}
\]
\hrule
\end{table}
\MATITA{} tacticals syntax is reported in Tab.~\ref{tab:tacsyn}.
-While one would expect to find structured constructs like
-$\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
-This is essential the base idea of \MATITA{} tacticals: step-by-step
-execution.
-
-The low-level tacticals implementation of \MATITA{} allows a step-by-step
-execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
-not executed as an atomic operation. This has major benefits for the
-user during proof structuring and re-playing.
+LCF tacticals have been replaced by unstructured more primitive commands;
+every LCF tactical is semantically equivalent to a sequential composition of
+them. As usual, each command is executed atomically, so that a sequence
+corresponding to an LCF tactical is now executed in multiple steps.
For instance, reconsider the previous example of a proof by induction.
-With step-by-step tacticals the user can apply the induction principle, and just
-open the branching tactical \OP{[}. Then he can interact with the
-system until the proof of the first case is terminated. After that
-\OP{|} is used to move to the next goal, until all goals are
-closed. After the last goal, the user closes the branching tactical with
-\OP{]} and he just finished a structured proof.
-
-While \MATITA{} tacticals help in structuring proofs they allow you to
-choose the amount of structure you want. There are no constraints imposed by
-the system, and if the user wants he can even write completely un-structured
-proofs.
-
-Re-playing a proof is also made simpler. There is no longer any need
-to destructure the proof on the fly since \MATITA{} executes each
-tactical not atomically.
-
-%\item[Rereading]
-% is possible. Going on step by step shows exactly what is going on. Consider
-% again a proof by induction, that starts applying the induction principle and
-% suddenly branches with a ``\texttt{[}''. This clearly separates all the
-% induction cases, but if the square brackets content is executed in one single
-% step you completely loose the possibility of rereading it and you have to
-% temporary remove the branching tactical to execute in a satisfying way the
-% branches. Again, executing step-by-step is the way you would like to review
-% the demonstration. Remember that understanding the proof from the script is
-% not easy, and only the execution of tactics (and the resulting transformed
-% goal) gives you the feeling of what is going on.
-%\end{description}
+In \MATITA{} the user can apply the induction principle, and just
+open the branching punctuation symbol \OP{[}. Then he can interact with the
+system (applying tactics and so forth) until he decides to move to the
+next branch using \OP{|}. After the last branch, the punctuation symbol
+\OP{]} must be used to collect goals possibly left open, accordingly to
+the semantics of the LCF branching tactical \OP{$\ldots$~;[~$\ldots$~|~$\ldots$~|~$\ldots$~]}. The result effortlessly obtained is a structured script.
+
+The user is not forced to fully structure his script. If he wants, he
+can even write completely unstructured proofs using only the \OP{.}
+punctuation symbol.
+
+Re-playing a proof is also straightforward since there is no longer any need
+to manually destructure the proof.
\section{Standard library}
\label{sec:stdlib}
-\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
-can be read, checked and referenced in further developments.
-However, in order to test the actual usability of the system, a
-new library of results has been started from scratch. In this case,
-of course, we wrote (and offer) the source script files,
-while, in the case of \COQ, \MATITA{} may only rely on XML files of
-\COQ{} objects.
+\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{} can be
+read, checked and referenced in further developments. However, in order to test
+the actual usability of the system, a new library of results has been started
+from scratch. In this case, of course, we wrote (and offer) the source scripts,
+while in the case of \COQ{} \MATITA{} may only rely on XML files of \COQ{}
+objects.
+
The current library just comprises about one thousand theorems in
elementary aspects of arithmetics up to the multiplicative property for
Eulers' totient function $\phi$.
+
The library is organized in five main directories: \texttt{logic} (connectives,
-quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type
+quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type
constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q}
(rationals). The most complex development is \texttt{nat}, organized in 25
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 a 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
\theendnotes
-\TODO{rivedere bibliografia, \'e un po' povera}
-
\bibliography{matita}
\end{document}
projects / helm.git / blobdiff