From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 14 Nov 2005 13:02:05 +0000 (+0000)
Subject: Introduction (partial).
X-Git-Tag: V_0_7_2_3~89
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a618d60f5082a7c50f0c15006a53bd57d959ba9c

Introduction (partial).
---

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index ab37f7849..6738aed4a 100644
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -133,6 +133,33 @@ discussion), but surely
 readable (the actual quality largely depends by the way the lambda 
 term is written). 
 
+Summing up, we already disposed of the following tools/techniques:
+\begin{itemize}
+\item XML specifications for the Calculus of Inductive Constructions,
+with tools for parsing and saving mathematical objects in such a format;
+\item metadata specifications and tools for indexing and querying the
+XML knowledge base;
+\item a proof checker (i.e. the {\em kernel} of a proof assistant), 
+implemented to check that we exported form the coq library all the 
+logically relevant content;
+\item a sophisticated parser (used by the search engine), able to deal 
+with potentially ambiguous and incomplete information, typical of the 
+mathematical notation \cite{};
+\item a {\em refiner}, i.e. a type inference system, based on complex 
+existential variables, used by the disambiguating parser;
+\item complex transformation algorithms for proof rendering in natural
+language;
+\item an innovative rendering widget, supporting high-quality bidimensional
+rendering, and semantic selection, i.e. the possibility to select semantically
+meaningfull rendering expressions, and to past the respective contebt 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
+add an authoring interface, and a set of functionalities for the
+overall management of the library, integrating everything into a
+single system. {\em Matita} is the result of this effort.