The practice of limiting the scope on the library to the logical environment
is contrary to our commitment of being able to fully exploit as much as possible
-of the library at any given time. To reconcile the two worlds, we have
-designed \MATITA \ldots \NOTE{Da completare se lo riteniamo un punto interessante.}
+of the library at any given time. To reconcile consistency and visibility
+we have departed from the traditional implementation of an environment
+allowing environments to be built on demand in a top-down way. The new
+implementation is based on a modified meta-theory that changes the way
+convertibility, type checking, unification and refinement judgements.
+The modified meta-theory is fully described in \cite{libraryenvironments}.
+Here we just remark how a strong commitment on the way the user interacts
+with the library has lead to modifications to the logical core of the proof
+assistant. This is evidence that breakthroughs in the user interfaces
+and in the way the user interacts with the tools and with the library could
+be achieved only by means of strong architectural changes.
\subsubsection{Accessibility}
A large library that is completely in scope needs effective indexing and
scenario the tactics must retrieve a set of candidates for backward or
forward reasoning in a few milliseconds.
+The choice of several proof assistants is to use ad-hoc data structures,
+such as context trees, to index all the terms currently in scope. These
+data structures are expecially designed to quickly retrieve terms up
+to matching, instantiation and generalization. All these data structures
+try to maximize sharing of identical subterms so that matching can be
+reduced to a visit of the tree (or dag) that holds all the maximally shared
+terms together.
+
+Since the terms to be retrieved (or at least their initial prefix)
+are stored (actually ``melted'') in the data structure, these data structures
+must collect all the terms in a single location. In other words, adopting
+such data structures means centralizing the library.
+
+In the \MOWGLI{} project we have tried to follow an alternative approach
+that consists in keeping the library fully distributed and indexing it
+by means of spiders that collect metadata and store them in a database.
+The challenge is to be able to collect only a smaller as possible number
+of metadata that provide enough information to approximate the matching
+operation. A matching operation is then performed in two steps. The first
+step is a query to the remote search engine that stores the metadata in
+order to detect a (hopefully small) complete set of candidates that could
+match. Completeness means that no term that matches should be excluded from
+the set of candiates. The second step consists in retrieving from the
+distributed library all the candidates and attempt the actual matching.
+
+In the last we years we have progressively improved this technique.
+Our achievements can be found in \cite{query1,query2,query3}.
+
+The technique and tools already developed have been integrated in \MATITA{},
+that is able to contact a remote \WHELP{} search engine \cite{whelp} or that
+can be directly linked to the code of the \WHELP. In either case the database
+used to store the metadata can be local or remote.
+
+Our current challenge consists in the exploitation of \WHELP{} inside of
+\MATITA. In particular we are developing a set of tactics, for instance
+based on paramodulation \cite{paramodulation}, that perform queries to \WHELP{}
+to restrict the scope on the library to a set of interesting candidates,
+greatly reducing the search space. Moreover, queries to \WHELP{} are performed
+during parsing of user provided terms to disambiguate them.
+
In Sect.~\ref{sec:metadata} we describe the technique adopted in \MATITA.
\subsubsection{Library management}
\subsubsection{Disambiguation stages}
-\subsection{notazione}
+\subsection{notation}
\label{sec:notation}
\ASSIGNEDTO{zack}
+Mathematical notation plays a fundamental role in mathematical practice: it
+helps expressing in a concise symbolic fashion concepts of arbitrary complexity.
+Its use in proof assistants like \MATITA{} is no exception. Formal mathematics
+indeed often impose to encode mathematical concepts at a very high level of
+details (e.g. Peano numbers, implicit arguments) having a restricted toolbox of
+syntactic constructions in the calculus.
+
+Consider for example one of the point reached while proving the distributivity
+of times over minus on natural numbers included in the \MATITA{} standards
+library. (Part of) the reached sequent can be seen in \MATITA{} both using the
+notation for various arithmetical and relational operator or without using it.
+The sequent rendered without using notation would be as follows:
+\sequent{
+\mathtt{H}: \mathtt{le} z y\\
+\mathtt{Hcut}: \mathtt{eq} \mathtt{nat} (\mathtt{plus} (\mathtt{times} x (\mathtt{minus}
+y z)) (\mathtt{times} x z))\\
+(\mathtt{plus} (\mathtt{minus} (\mathtt{times} x y) (\mathtt{times} x z))
+(\mathtt{times} x z))}{
+\mathtt{eq} \mathtt{nat} (\mathtt{times} x (\mathtt{minus} y z)) (\mathtt{minus}
+(\mathtt{times} x y) (\mathtt{times} x z))}
+while the corresponding sequent rendered with notation enabled would be:
+\sequent{
+H: z\leq y\\
+Hcut: x*(y-z)+x*z=x*y-x*z+x*z}{
+x*(y-z)=x*y-x*z}
+
+
\subsection{mathml}
\ASSIGNEDTO{zack}
open the branching tactical \verb+[+. Then you can interact with the system
reaching a proof of the first case, without having to specify the whole
branching tactical. When you have proved all the induction cases, you close
- the branching tactical with \verb+]+ and you are done with a structured proof
- without the.
+ the branching tactical with \verb+]+ and you are done with a structured proof.
\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