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 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
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:
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.
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
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.
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
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}
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.