From a618d60f5082a7c50f0c15006a53bd57d959ba9c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 14 Nov 2005 13:02:05 +0000 Subject: [PATCH] Introduction (partial). --- helm/papers/matita/matita.tex | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) 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. -- 2.39.2