respect to \COQ. For instance, the API of the components of \MATITA{} comprise
989 functions, to be compared with the 4'286 functions of \COQ.
-FINQUI SPELL CHECKATO
-
Finally, \MATITA{} has several innovative features over \COQ{} that derive
from the integration of Mathematical Knowledge Management tools with proof
assistants. Among them, the advanced indexing tools over the library and
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 mantaining backward compatibility
+unification), changing these functionalities maintaining backward compatibility
is very difficult. Finally, the code of \COQ{} has been greatly optimized
-over the years; optimization reduces maintenability and rises the complexity
+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
developed by others, comprising the authors of \COQ. Moreover, starting from
-scratch, we have designed in advance the architecture and we have splitted
+scratch, we have designed in advance the architecture and we have split
the code in coherent minimally coupled components.
In the future we plan to exploit \MATITA{} as a test bench for new ideas and
are Web services developed in the HELM and MoWGLI projects and already described
elsewhere. In particular:
\begin{itemize}
- \item The \emph{Getter} is a Web service to retrieve an (XML) document
+ \item The \emph{\GETTER} is a Web service to retrieve an (XML) document
from a physical location (URL) given its logical name (URI). The Getter is
responsible of updating a table that maps URIs to URLs. Thanks to the Getter
it is possible to work on a logically monolithic library that is physically
distributed on the network. More information on the Getter can be found
in~\cite{zack-master}.
- \item \emph{Whelp} is a search engine to index and locate mathematical
+ \item \emph{\WHELP} is a search engine to index and locate mathematical
notions (axioms, theorems, definitions) in the logical library managed
by the Getter. Typical examples of a query to Whelp are queries that search
for a theorem that generalize or instantiate a given formula, or that
an XML document that lists the URIs of a complete set of candidates that
are likely to satisfy the given query. The set is complete in the sense
that no notion that actually satisfies the query is thrown away. However,
- the query is only approssimated in the sense that false matches can be
+ the query is only approximated in the sense that false matches can be
returned. Whelp has been described in~\cite{whelp}.
- \item \emph{Uwobo} is a Web service that, given the URI of a mathematical
+ \item \emph{\UWOBO} is a Web service that, given the URI of a mathematical
notion in the distributed library, renders it according to the user provided
- two dimensional mathematical notation. Uwobo may also embed the rendering
+ two dimensional mathematical notation. \UWOBO{} may also embed the rendering
of mathematical notions into arbitrary documents before returning them.
- The Getter is used by Uwobo to retrieve the document to be rendered.
- Uwobo has been described in~\cite{zack-master}.
+ The Getter is used by \UWOBO{} to retrieve the document to be rendered.
+ \UWOBO{} has been described in~\cite{zack-master}.
\item The \emph{Proof Checker} is a Web service that, given the URI of
notion in the distributed library, checks its correctness. Since the notion
is likely to depend in an acyclic way over other notions, the proof checker
dependencies, checking in turn every notion for correctness.
The proof checker has been described in~\cite{zack-master}.
\item The \emph{Dependency Analyzer} is a Web service that can produce
- a textual or graphical representation of the dependecies of an object.
+ a textual or graphical representation of the dependencies of an object.
The dependency analyzer has been described in~\cite{zack-master}.
\end{itemize}
\subsection{Content level terms}
\label{sec:contentintro}
-The language used to communicate proofs and expecially formulae with the
-user does not only needs to be extendible and accomodate the usual mathematical
+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.
every ambiguous formula one partially specified term. The
\texttt{cic\_disambiguation} \component{} implements the
disambiguation algorithm we presented in~\cite{disambiguation} that is
-responsible of building in an efficicent way the set of all ``correct''
+responsible of building in an efficient way the set of all ``correct''
interpretations. An interpretation is correct if the partially specified term
obtained using the interpretation is refinable.
Scripts are not seen as constituents of the library. They are not published
and indexed, so they cannot be searched or browsed using \HELM{} tools.
-However, they play a central role for the mainteinance of the library.
+However, they play a central role for the maintenance of the library.
Indeed, once a notion is invalidated, the only way to restore it is to
fix the possibly broken script that used to generate it.
Moreover, during the authoring phase, scripts are a natural way to
expressions to partially specified terms, which are part of the runtime status
of \MATITA. They can be provided by users with the \texttt{alias} statement, but
are usually automatically added when evaluating \texttt{include} statements
-(\emph{implicit aliases}). Aliases implicitely inferred during disambiguation
+(\emph{implicit aliases}). Aliases implicitly inferred during disambiguation
are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
which require interactive choice are saved in batch compilable format. Thus,
after evaluating the above theorem the script will be changed to the following
snippet (assuming that the interpretation of \OP{<} over integers has been
-choosed):
+chosen):
\begin{grafite}
alias symbol "lt" = "integer 'less than'".
\end{grafite}
But how are disambiguation aliases used? Since they come from the parts of the
-library explicitely included we may be tempted of using them as the only
+library explicitly included we may be tempted of using them as the only
available interpretations. This would speed up the disambiguation, but may fail.
Consider for example:
and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
-Mathematichans would write the term that way since it is well known that the
+Mathematicians would write the term that way since it is well known that the
natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
number for the purpose of real multiplication. The refiner of \MATITA{} supports
\emph{implicit coercions} for this reason: given as input the above content
using the \WHELP{} technology, in response to the user alteration or
removal of mathematical objects.
-As already sketched in Sec.~\ref{sec:fullyspec} what we generate
+As already sketched in Sect.~\ref{sec:fullyspec} what we generate
from a script is split among two storage media, a
classical filesystem and a relational database. The former is used to
store the XML encoding of the objects defined in the script, the
\item all identifiers should (but this is not strictly compulsory)
separated by an underscore,
\item identifiers in two different hypothesis, or in an hypothesis
-and in the conlcusion must be separated by the string ``\verb+_to_+'';
+and in the conclusion must be separated by the string ``\verb+_to_+'';
\item the identifier may be followed by a numerical suffix, or a
-single or duoble apostrophe.
+single or double apostrophe.
\end{itemize}
Take for instance the theorem
\[ \forall A:Type. symmetric \;A\;(eq \; A)\]
and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem.
So, somehow unexpectedly, the introduction of semi-rigid naming convention
-has an important benefical effect on the global organization of the library,
+has an important beneficial effect on the global organization of the library,
forcing the user to define abstract notions and properties before
using them (and formalizing such use).
using techniques inspired by \cite{natural,YANNTHESIS} and already described
in~\cite{remathematization}.
-Note that the syntax used in the script view is \TeX-like, however unicode is
+Note that the syntax used in the script view is \TeX-like, however Unicode is
fully supported so that mathematical glyphs can be input as such.
\begin{figure}[!ht]
$\NT{sequent\_path}$ starting from a visual selection.
\NOTE{Questo ancora non va in matita}
- A $\NT{multipath}$ is a CiC term in which a special constant $\%$
+ A $\NT{multipath}$ is a CIC term in which a special constant $\%$
is allowed.
The roots of discharged subterms are marked with $?$, while $\%$
is used to select roots. The default $\NT{multipath}$, the one that
that the pattern selects only the third argument of $eq$.
The experienced user may also write by hand a concise pattern
-to change at once all the occcurrences of $n$ in the hypothesis $H$:
+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}
con una pattern\_of(select(pattern))}
\subsubsection{Comparison with \COQ{}}
-\COQ{} has a two different ways of restricting the application of tactis to
+\COQ{} has two different ways of restricting the application of tactics to
subterms of the sequent, both relaying on the same special syntax to identify
a term occurrence.
The base idea is that to identify a subterm of the sequent we can
write it and say that we want, for example, the third and the fifth
-occurce of it (counting from left to right). In our previous example,
+occurrences of it (counting from left to right). In our previous example,
to change only the left part of the equivalence, the correct command
is
\begin{grafite}
In these cases using the mouse to select the wanted term is probably the
only way to tell the system exactly what you want to do.
-One of the goals of \MATITA{} is to use modern publishing techiques, and
+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 definitively be a bad choice.
\subsection{Tacticals}
There are mainly two kinds of languages used by proof assistants to recorder
proofs: tactic based and declarative. We will not investigate the philosophy
-aroud the choice that many proof assistant made, \MATITA{} included, and we
-will not compare the two diffrent approaches. We will describe the common
+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.
\end{figure}
We do not plan to maintain the library in a centralized way,
-as most of the systems do. On the contary we are currently
+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.
projects / helm.git / commitdiff