X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;fp=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=4883fa4ad1b04802b7f8c8ba16dc161d026067e0;hb=1284797c1b63732de9af2a433722e1ff8e564ed0;hp=494b1c25a7bf2bd5ba54a37b4cc595b9cb023f32;hpb=0b057a6f3f1b803c387d3fcef714f801d42225b2;p=helm.git diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 494b1c25a..4883fa4ad 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -817,7 +817,7 @@ effective way, assuming as little knowledge as possible about the 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 @@ -837,7 +837,7 @@ 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 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 @@ -910,10 +910,10 @@ specified terms. In case of overloaded sources there exists multiple aliases 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 +Preferences can be explicitly given in the script (using the misleading \texttt{alias} commands), 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: @@ -940,7 +940,7 @@ status. Unlike aliases, they are not part of the library. 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. @@ -1037,7 +1037,7 @@ partially specified term where in place of \texttt{n} the application of a 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 +Implicit 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 @@ -1219,7 +1219,7 @@ The former derives new facts by a set of active 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. @@ -1589,7 +1589,7 @@ x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with Since \TAC{rewrite}, \TAC{replace} and several other tactics boils 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 @@ -1605,7 +1605,7 @@ using heavy math notation would have definitively been a bad choice. In \MATITA{}, tactics accepting pattern arguments can be more expressive than the equivalent tactics in \COQ{} since variables bound in the pattern context, -can occurr in context-dependent arguments. For example, consider the sequent: +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} @@ -1765,7 +1765,7 @@ scripts, listed in Tab.~\ref{tab:scripts}. 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 +developing Wiki-technologies to support collaborative development of the library, encouraging people to expand, modify and elaborate previous contributions.