...

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 7cfdde2e9146809dbad8ca0f5d03fbfe4d0aa190..be3cc61bf9d501c71e592a1a97ce43d93a8743e3 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -288,6 +288,54 @@ an improvement over fully specified terms since they allow to omit redundant
 information that can be inferred by the refiner.
 
 \subsection{Terms at the content level}
+The language used to communicate proofs and expecially expressions with the
+user does not only needs to be extendible and accomodate the usual mathematical
+notation. It must also reflect the comfortable degree of imprecision and
+ambiguity that the mathematical language provides.
+
+For instance, it is common practice in mathematics to speak of a generic
+equality that can be used to compare any two terms. However, it is well known
+that several equalities can be identified as soon as we care for decidability
+or for their computational properties. For instance equality over real
+numbers is well known to be undecidable, whereas it is decidable over
+rational numbers.
+
+Similarly, we usually speak of natural numbers and their operations and
+properties without caring about their representation. However the computational
+properties of addition over the binary representation are very different from
+those of addition over the unary representation. And addition over two natural
+numbers is definitely different from addition over two real numbers.
+
+Formal mathematics cannot hide these differences and obliges the user to be
+very precise on the types he is using and their representation. However,
+to communicate formulae with the user and with external tools, it seems good
+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
+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.
+
+The translation from partially refined 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
+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
+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 ???
 
 \subsection{Terms at the presentation level}