From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Nov 2005 10:57:55 +0000 (+0000)
Subject: ...
X-Git-Tag: V_0_7_2_3~43
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5b0a2dd87795f7a5cd0909c341e5a5e789371194

...
---

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index d0305c381..23ca6e18a 100644
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -332,12 +332,50 @@ library as a whole will be logically inconsistent.
 Logical inconsistency has never been a problem in the daily work of a
 mathematician. The mathematician simply imposes himself a discipline to
 restrict himself to consistent subsets of the mathematical knowledge.
-However, in doing so he doesn't choose the subset in advance by forgetting
-the rest of his knowledge.
+However, in doing so he does not choose the subset in advance by forgetting
+the rest of his knowledge. On the contrary he may proceed with a sort of
+top-down strategy: he may always inspect or use part of his knowledge, but
+when he actually does so he should check recursively that inconsistencies are
+not exploited.
+
+Contrarily to the mathematical practice, the usual tendency in the world of
+assisted automation is that of building a logical environment (a consistent
+subset of the library) in a bottom up way, checking the consistency of a
+new axiom or theorem as soon as it is added to the environment. No lemma
+or definition outside the environment can be used until it is added to the
+library after every notion it depends on. Moreover, very often the logical
+environment is the only part of the library that can be inspected,
+that we can search lemmas in and that can be exploited by automatic tactics.
+
+Moving one by one notions from the library to the environment is a costly
+operation since it involves re-checking the correctness of the notion.
+As a consequence mathematical notions are packages into theories that must
+be added to the environment as a whole. However, the consistency problem is
+only raised at the level of theories: theories must be imported in a bottom
+up way and the system must check that no inconsistency arises.
+
+The practice of limiting the scope on the library to the logical environment
+is contrary to our commitment of being able to fully exploit as much as possible
+of the library at any given time. To reconcile the two worlds, we have
+designed \MATITA \ldots \NOTE{Da completare se lo riteniamo un punto interessante.}
+
+\subsubsection{Accessibility}
+A large library that is completely in scope needs effective indexing and
+searching methods to make the user productive. Libraries of formal results
+are particularly critical since they hold a large percentage of technical
+lemmas that do not have a significative name and that must be retrieved
+using advanced methods based on matching, unification, generalization and
+instantiation.
+
+The efficiency of searching inside the library becomes a critical operation
+when automatic tactics exploit the library during the proof search. In this
+scenario the tactics must retrieve a set of candidates for backward or
+forward reasoning in a few milliseconds.
+
+In Sect.~\ref{sec:metadata} we describe the technique adopted in \MATITA.
+
+\subsubsection{Library management}
 
-Contrarily to a mathematician, the usual tendency in the world of assisted
-automation is that of restricting in advance the part of the library that
-will be used later on, checking its consistency by construction.
 
 \subsection{ricerca e indicizzazione}
 \label{sec:metadata}