ocaml 3.09 transition

[helm.git] / helm / papers / use_case / use_case.tex

diff --git a/helm/papers/use_case/use_case.tex b/helm/papers/use_case/use_case.tex
index 5372f3369d49854ed18bd7bfb7e7e8ef30ea3b02..b416efb8b2d8d5be6f9065af1f2143d91f624730 100644 (file)
--- a/helm/papers/use_case/use_case.tex
+++ b/helm/papers/use_case/use_case.tex
@@ -68,7 +68,7 @@ gravi?) and suggestions for improvement (especially in performance).
 We also actively contributed to software development. In particular,
 let us mention the implementation of Gdome2 \cite{Gdome2}, a level2 
 compliant DOM api written in C++ for the gnome programming environment, 
-that was mostly performed and tuned within the framework of the 
+that was mostly developed and tuned within the framework of the 
 \mowgli project, and GtkMathView (\cite{}), a rendering widget for 
 MathML.
 
@@ -81,10 +81,40 @@ Cenni sulla struttura del paper? Vediamo alla fine.
 
 
 \section{The repository}
-Un po di dati sulla libreria dimensione minima, media max dei files,
+The aim of \mowgli was to test the feasibility of passing from a machine
+readable to a machine understandable encoding of mathematical information, 
+and to explore the the new potentialities offered by such 
+encoding.
+To this aim, we needed large collections of documents enriched with 
+semantic markup, and the natural solution was to use one of the many
+interesting libraries of formalized mathematics already existent in
+the world; in particular, we used the library of the Coq Proof assistant, 
+developed at INRIA Future. 
+This gave us a pretty large ($tot$) repository of {\em fully structured} 
+mathematical documents: the actual dtd contains {\em no textual elements 
+at all}. As a matter of fact, text is the most typical example of 
+information which is machine-readable but not machine understandable. 
+By banishing text, we intentionally adopted (here, as in many other 
+aspects of our project) an {\extreme} position, not as a phisolophical 
+choice or commitment, but as a mere working hypothesis.
+
+The actual details of the DTD are not so relevant here. Let us just say
+that we had essentially two main classes of documents, characterized by
+the different nesting depth of the markup: {\b proof objects} 
+(usually quite deep) and the corresponding {\b intermediate goals} 
+(relatively flat, being collections of formulas). 
+ 
+Anticipare il perche' dell'enfasi sulla profondita', se (come
+pensiamo) il comportamento risutla essere sensibile a questo
+fattore. Se non lo e', cassiamo direttamente il discorso 
+profondita' (o semplicemnte diciamo che non sembra essere rilevante).
+
+Adesso mettiamo un po' di dati sulla libreria dimensione minima, 
+media max dei files,
 idem per profondita' e larghezza. 
+
 Cenni sul DTD? Spiegare se/perche' non abbiamo mai sentito bisogno
-di una schema?
+di una schema?