X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fmathql%2Fdoc%2Fmathql_overview.tex;h=761b688cb070cbac3b2f7d82dc90f51beeb20ea3;hb=78cf601fd8b8dbb386b0db315dcbfdbe8256c15f;hp=d511c7aa1f3e405310cc201c23d1f321254485d1;hpb=1c84c6e1df257ad284a256ee0c2c1a203f81b713;p=helm.git

diff --git a/helm/mathql/doc/mathql_overview.tex b/helm/mathql/doc/mathql_overview.tex
index d511c7aa1..761b688cb 100644
--- a/helm/mathql/doc/mathql_overview.tex
+++ b/helm/mathql/doc/mathql_overview.tex
@@ -8,39 +8,25 @@ context of the {\HELM}%
 project \cite{APSCGS03}.
 Its name suggests that it is supposed to be the first of a group of query
 languages for retrieving information from distributed digital libraries of
-formal mathematical knowledge, but no other languages of this proposal have
-been implemented yet except for {\MathQL} that is not Mathematics-oriented.
-So the name is a bit misleading.    
-
-\xcomment {
-
-The MathQL proposal rises within the HELM project with the final aim of
-providing a set of query languages for digital libraries of formalized
-mathematical resources, capable of expressing content-aware requests.
-
+formal mathematical knowledge by means of content-aware requests, but no other
+languages of this proposal have been implemented yet except for {\MathQL} that
+is not Mathematics-oriented. So the name is a bit misleading.    
 This proposal has several domains of application and may be useful for
 database or on-line libraries reviewers, for proof assistants or
 proof-checking systems, and also for learning environments because these
 applications require features for classifying, searching and browsing
 mathematical information in a semantically meaningful way.
 
-As the most natural way to handle content information about a resource is
-by means of metadata, our first task is providing a query language that we
-call MathQL level 1 (or {\MathQL} for short), suitable for a metadata
-framework.
 Other languages to be defined in the context of the MathQL proposal may be
 suitable for queries about the semantic structure of mathematical data:
-this includes content-based pattern-matching (MathQL-2) and possibly other
-forms of formal matching involving for instance isomorphism, unification and
+this includes content-based pattern-matching and possibly other forms of
+formal matching involving for instance isomorphism, unification and
 $\delta$-expansion%
-\footnote{by $\delta$-expansion we mean the expansion of definitions.}
-(MathQL-3).
-
-In this perspective the role of a query on metadata can be that of producing a
+\footnote{By $\delta$-expansion we mean the expansion of definitions.}.
+In this perspective the role of a query on metadata is that of producing a
 filtered knowledge base containing relevant information for subsequent queries
-of other kind.
-
-}
+of other kind (see \cite{GSC03} for a more detailed description of this
+approach).
 
 {\MathQL} is carefully designed for making up for two limitations that seem to
 characterize several implementations and proposals of current {\RDF}-oriented