From: Andrea Asperti Date: Mon, 5 Dec 2005 09:21:38 +0000 (+0000) Subject: Added a new section on the logical library. X-Git-Tag: make_still_working~8053 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=75cce5f252471a73764953dbb5fa24a450d153bb;p=helm.git Added a new section on the logical library. --- diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib index 4927850ba..f2f024e71 100644 --- a/helm/papers/matita/matita.bib +++ b/helm/papers/matita/matita.bib @@ -912,6 +912,15 @@ year = 1998 } +@misc{content-centric, + author = "Andrea Asperti and Luca padovani and Claudio Sacerdoti Coen + and irene Schena", + title = "Content-centric Logical Envirnoments", + howpublished = "Short Presentation at the Fifteenth IEEE Symposium on Logic in Computer Science", + month = "June", + year = "2000", + key = "content centric" +} @misc{mowgli-proposal, title = "The {MoWGLI Proposal}, {HTML} Version", diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index b3842fbd3..b047caea9 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -139,22 +139,24 @@ have been also conducted with other systems, and notably with \NUPRL{}\cite{nuprl-book}. The work, mostly performed in the framework of the recently concluded European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the -following teps: +following steps: \begin{itemize} \item exporting the information from the internal representation of \COQ{} to a system and platform independent format. Since XML was at the time an emerging standard, we naturally adopted this technology, fostering -a content-centric architecture for future system, where the documents +a content-centric architecture\cite{content-centric} where the documents of the library were the the main components around which everything else has to be build; \item developing indexing and searching techniques supporting semantic - queries to the library; these efforts gave birth to our \WHELP{} -search engine, described in~\cite{whelp}; + queries to the library; +%these efforts gave birth to our \WHELP{} +%search engine, described in~\cite{whelp}; \item developing languages and tools for a high-quality notational -rendering of mathematical information; in particular, we have been -active in the MathML Working group since 1999, and developed inside -\HELM{} a MathML-compliant widget for the GTK graphical environment -which can be integrated in any application. +rendering of mathematical information\footnote{We have been +active in the MathML Working group since 1999.}; +%and developed inside +%\HELM{} a MathML-compliant widget for the GTK graphical environment +%which can be integrated in any application. \end{itemize} According to our content-centric commitment, the library exported from @@ -163,9 +165,9 @@ as Web services. The user could interact with the library and the tools by means of a Web interface that orchestrates the Web services. The Web services and the other tools have been implemented as front-ends -to a set of libraries, collectively called the \HELM{} libraries. +to a set of software libraries, collectively called the \HELM{} libraries. At the end of the \MOWGLI{} project we already disposed of the following -techniques and libraries: +tools and software libraries: \begin{itemize} \item XML specifications for the Calculus of Inductive Constructions, with libraries for parsing and saving mathematical objects in such a format @@ -182,15 +184,15 @@ mathematical notation \cite{disambiguation}; partially specified terms, used by the disambiguating parser; \item complex transformation algorithms for proof rendering in natural language \cite{remathematization}; -\item an innovative rendering widget \cite{padovani}, supporting +\item an innovative, MathML-compliant rendering widget for the GTK +graphical environment\cite{padovani}, supporting high-quality bidimensional rendering, and semantic selection, i.e. the possibility to select semantically meaningful rendering expressions, and to past the respective content into a different text area. \end{itemize} -Starting from all this, the further step of developing our own -proof assistant was too -small and too tempting to be neglected. Essentially, we ``just'' had to +Starting from all this, developing our own proof assistant was not +too far away: essentially, we ``just'' had to add an authoring interface, and a set of functionalities for the overall management of the library, integrating everything into a single system. \MATITA{} is the result of this effort. @@ -1212,6 +1214,46 @@ implicit coercions. \TODO{alias one shot} +\section{The logical library} +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, the user may also dispose of the source script files, +while in the case of Coq he may only rely on XML files of +Coq objects. +The current library just comprises about one thousand theorems in +elementary aspects of arithmetics. The most complex result proved +so far in Matita (that however, at our knoweledge, has never been proved +before in any other system) is the multiplicative property for Eulers' +totient function $\phi$. +The library is organized in five main directories: $logic$ (connectives, +quantifiers, equality, $\dots$), $datatypes$ (basic datatypes and type +constructors), $nat$ (natural numbers), $Z$ (integers), $Q$ (rationals). +The most complex development is $nat$, organized in 25 scripts, listed +in Figure\ref{scripts} +\begin{figure}[htb] +$\begin{array}{lll} +nat.ma & plus.ma & times.ma \\ +minus.ma & exp.ma & compare.ma \\ +orders.ma & le\_arith.ma & lt\_arith.ma \\ +factorial.ma & sigma\_and\_pi.ma & minimization.ma \\ +div\_and\_mod.ma & gcd.ma & congruence.ma \\ +primes.ma & nth\_prime.ma & ord.ma\\ +count.ma & relevant\_equations.ma & permutation.ma \\ +factorization.ma & chinese\_reminder.ma & fermat\_little\_th.ma \\ +totient.ma& & \\ +\end{array}$ +\caption{\label{scripts}Matita scripts on natural numbers} +\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 +developing wiki-technologies to support a collaborative +development of the library, encouraging people to expand, +modify and elaborate previous contributions. + + \acknowledgements We would like to thank all the students that during the past five years collaborated in the \HELM{} project and contributed to