From 5b0a2dd87795f7a5cd0909c341e5a5e789371194 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Nov 2005 10:57:55 +0000 Subject: [PATCH] ... --- helm/papers/matita/matita.tex | 48 +++++++++++++++++++++++++++++++---- 1 file changed, 43 insertions(+), 5 deletions(-) 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} -- 2.39.2