...

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 8708e44580f7958ca7ad06bd5533367c65fc459d..76cd8aa1886b02210351060e37622cc23b3a406e 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -183,7 +183,7 @@ to be used as a Web service. \MATITA{} can directly link the code of the
 that forwards every request to the Getter.
 
 To better understand the architecture of \MATITA{} and the role of each
-library, we can focus on the rappresentation of the mathematical information.
+library, we can focus on the representation of the mathematical information.
 \MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
 Constructions (CIC). In CIC terms are used to represent mathematical
 expressions, types and proofs. \MATITA{} is able to handle terms at
@@ -313,29 +313,45 @@ practice to stick to the usual imprecise mathematical ontology. In the
 Mathematical Knowledge Management community this imprecise language is called
 the \emph{content level} representation of expressions.
 
-In \MATITA{} we provide two translations from partially refined terms
+In \MATITA{} we provide two translations from partially specified terms
 to content level terms and the other way around. The first translation can also
-be applied to fully refined terms since a fully refined term is a special case
-of partially refined term where no metavariable or implicit term occurs.
+be applied to fully specified terms since a fully specified term is a special
+case of partially specified term where no metavariable or implicit term occurs.
 
-The translation from partially refined terms to content level terms must
+The translation from partially specified terms to content level terms must
 discriminate between terms used to represent proofs and terms used to represent
 expressions. The firsts are translated to a content level representation of
-proofs steps that can easily be rendered in natural language. The latters
+proof steps that can easily be rendered in natural language. The latters
 are translated to MathML Content formulae. MathML Content is a W3C standard
 for the representation of content level expressions in an XML extensible format.
 
 The translation to content level is implemented in the
-\texttt{acic\_to\_content} library. Its input are \emph{annotated partially
-refined terms}. Annotated partially refined terms are maximally unshared
-partially refined terms enriched with additional typing information for each
+\texttt{acic\_content} library. Its input are \emph{annotated partially
+specified terms}. Annotated partially specified terms are maximally unshared
+partially specified terms enriched with additional typing information for each
 subterm. This information is used to discriminate between terms that represent
 proofs and terms that represent expressions. Part of it is also stored at the
 content level since it is required to generate the natural language rendering
-of proofs. The \emph{cic\_to\_acic} library annotates partially refined terms.
-
-The translation from content level terms to partially refined terms is
-also performed in \ldots ???
+of proofs. The terms need to be maximally unshared (i.e. they must be a tree
+and not a DAG). The reason is that to the occurrences of a subterm in
+two different positions we need to associate different typing informations.
+This association is made easier when the term is represented as a tree since
+it is possible to label each node with an unique identifier and associate
+the typing information using a map on the identifiers.
+The \texttt{cic\_acic} library annotates partially specified terms.
+
+We do not provide yet a reverse translation from content level proofs to
+partially specified terms. But in \texttt{disambiguation} we do provide
+the reverse translation for expressions. The mapping from
+content level expressions to partially specified terms is not unique due to
+the ambiguity of the content level. As a consequence the translation
+is guided by an \emph{interpretation}, that is a function that chooses for
+every ambiguous expression one partially specified term. The
+\texttt{disambiguation} library contains the implementation of the
+disambiguation algorithm we presented in \cite{disambiguation} that is
+responsible of building in an efficicent way the set of all ``correct''
+interpretations. An interpretation is correct if the partially refined term
+obtained using the interpretation is refinable.
 
 \subsection{Terms at the presentation level}