absolute path and factorization for matita.basedir

[helm.git] / helm / papers / whelp / main.tex

\documentclass[runningheads,a4paper]{article}
\pagestyle{headings}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{hyperref}

\newcommand{\andreaEmail}{asperti@cs.unibo.it}
\newcommand{\zackEmail}{zacchiro@cs.unibo.it}
\newcommand{\moogle}{Moogle}
\newcommand{\IR}{\ensuremath{\mathcal{R}}}

\title{Searching mathematics on the Web:\\
state of the art and future developments}

\author{
\begin{tabular}{c@{\hspace{2em}}c}
 Andrea Asperti & Stefano Zacchiroli \\
 \href{mailto:\andreaEmail}{\texttt{\andreaEmail}} &
  \href{mailto:\zackEmail}{\texttt{\zackEmail}}
\end{tabular}\\[2em]
Department of Computer Science, University of Bologna\\
Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY}

\begin{document}
\maketitle

\begin{abstract}
 A huge amount of mathematical knowledge is nowadays available on the World Wide
 Web. Many different solutions and technologies for searching that knowledge
 have been developed as well. We present the state of the art of searching
 mathematics on the Web, giving some insight on future developments in this
 area.
\end{abstract}

\section{Introduction}
The World Wide Web has become one of the main resources used by mathematicians
in every day work. Its usefulness is not limited to browsing fellow researchers,
university, or research projects web pages. A full range of mathematical
services are available as well on the web, ranging from electronic libraries of
mathematics to communities of distributed agents, implemented as web services,
able to cooperate in order to solve a given mathematical problem.

Searching such a huge amount of mathematical sources is a particularly 
complex problem, given the variety of different users with completely 
different needs, and the heterogeneity of the mathematical information
and its possible encodings.

The different kind of queries may be roughly categorized in three 
main groups:
\begin{description}
\item[Bibliographic searches] this is the most traditional kind of query,
aimed at retrieving a document given its author, title, date of publication,
a list of keywords or similar information. A typical query could be e.g.
{\em give me a listing of all articles written by Karl Weierstrass on
  the subject of analytic functions}.
\item[Mathematical services] in this case the user in typically interested
to {\em solve} a problem with the help of some mathematical tool, or a 
combination of them. A typical query in this context could be the request
for a web service able to establish the primality of a number given as input
by the user. 
\item[Content based searches] the third and probably most ambitious 
category of queries are those based on the mathematical content of the 
information (opposed to its textual representation). These queries are
aimed at a very fine-grained analysis of the repository, looking e.g.
for all documents stating something about the expression
$cos(z) + i~sin(z)$, where of course $z$ has to be understood as an
universally quantified variable whose actual name is thus irrelevant
(try with Google!). 
\end{description}

In this paper ws discuss in more detail the previous categories of queries,
presenting the state of the art and the main research directions.  A particular
attention will be devoted to {\em mathematical services} and, especially, {\em
content based searches} being the most innovative and peculiar kind of queries
for mathematical repositories.

\section{Bibliographic searches}
\label{sec:bibliographic}

Most part of printed human knowledge available all over the world is stocked
inside libraries. The problem of how to search those libraries in an efficient
manner has been traditionally solved by the combined use of metadata (data about
the documents themselves) and indexes. 
In this case, mathematical documents do not substantially differ from
other kinds of documents and standard knowledge 
management and indexing techniques can be profitably applied. 
From each document of the library a set
of metadata is extracted and several orthogonal indexes are created on top of
them referencing the physical locations of the actual documents. Searches
performed using that indexes are called \emph{bibliographic searches}.

Metadata could include information about document title, author, editor,
classification and so on. The classification field is of particular interest 
for
searches since it defines a taxonomy over human knowledge: related documents 
are likely to share a common classification.

Since the beginning, several classifications have been developed by librarians,
the most widespread being the Dewey Decimal Classification~\cite{dewey} in which
``Natural sciences \& mathematics'' have been assigned decimal number 500. Since
Dewey's is too lax for properly classifying mathematical documents, other
classifications have been developed by mathematicians, the most widespread being
MSC 2000~\cite{msc2000} --- Mathematical Subject Classification Scheme ---
maintained by the American Mathematical Society. In this classification for
example 35E15 is a subtopic of partial differential equation (35xxx) with
constant coefficients (35Exx), documents with that classification will be about
the initial value problem (35E15).

The arrival of the web era has increased accessibility of mathematical 
libraries
and improved the expressivity of queries, but has not (yet?) radically changed
the way in which bibliographic searches are performed.

Zentralblatt MATH~\cite{zmath}, coordinated by FIZ Karlsruhe, is the most
prominent project in this area being the longest running indexing and
abstracting service in pure and applied mathematics available on the web. It
classifies more than 2,000,000 entries accordingly to MSC 2000. Searches are
possible via various fields, like author, title, document type, MSC
classification, year of publication and so on. Boolean combinations of the
various fields for fine grained searches are possible as well.

For each results title, abstract and all metadata information associated to the
document are shown and other interesting actions are possible like browsing
related documents (same MSC 2000 classification) and on-line ordering of the
printed document.

While Zentralblatt is the most relevant indexing and abstracting services, 
other
on-line databases of mathematical documents are available offering, on a smaller
scale, similar classification services. Just to name a few of them:
MathSciNet~\cite{mathscinet} by the American Mathematical Society and the
Electronic Research Archive for Mathematics (ERAM)~\cite{eram}.

\subsection{The European project Euler}
A big improvement in the accessibility of all these electronic libraries have
been induced by the European based Euler project~\cite{euler}. On the behalf of
this project a web based gateway, with searching capabilities really similar to
those of Zentralblatt MATH, has been developed. Using Euler the user have access
to the catalogues and repositories of mathematical documents of participating
institutions, while the latter keep control over creation and maintenance of
their data.

Euler is the state of the art of mathematical bibliographic searches on 
the web:
a portal offering unified access to documents from Zentralblatt, the CWI
database of the Dutch national research center of mathematics~\cite{cwi}, ERAM
and many more institutions. Once an entry is found, access to the electronic or
printed version of the document is mediated via the web site of the document
owner.

Euler is currently supported by the European Community as a take-up
Project (n.IST-2000-29445), based on the achievements of the successfully 
completed EULER project (FP4 "Telematics for Libraries" project LB-5609).

\subsection{Key phrases and information clouds}
To manage huge scientific archive metadata are essential, in particular key
phrases which should come from a large standardized (controlled) and updateable
list. A major problem here is that a perfectly good key phrase for a given chunk
of text may very well simply not occur there (or be so linguistically disguised
that it cannot actually be recognized). Scientists get around this by looking at
the surrounding text.

This is the idea of an \emph{identification cloud} which in its simplest form is
just a list of words (possibly with weights) that is attached to a standard key
phrase and that are likely to occur in texts dealing with the concepts embodied
by that key phrase.  The concept was introduced in the ongoing project Trial
Solution (IST-1999-11397)~\cite{clouds} with promising results. 


\section{Mathematical services}
\label{sec:webservices}

In the last years several research efforts have been made for the
standardization and the deployment of web services~\cite{webservices}. Fitting
properly in the semantic web~\cite{semanticweb} framework, web services are
software systems designed to support machine to machine interaction over a
network (usually the Internet), typically exposing a programming interface based
on exchange of XML documents~\cite{xml}.

\subsection{The W3C standardization effort}
The standardization activity of the World Wide Web Consortium in the
area of Web Services is articulated in 5 working groups: Web
Services Architecture Working Group, XML Protocol Working Group, Web
Services Description Working Group, Web Services Choreography Working
Group and an auxiliary Coordination Group. The most relevant ones
are:
\begin{description}

 \item[Web Services Description
  Working Group] 
  This group\footnote{\url{http://www.w3.org/2002/ws/desc/}} is
  chartered to design an XML based language that should be able to
  describe a web service \emph{interface}. This task includes also the
  design of web service \emph{messages}, \emph{message exchange
  patterns} and \emph{protocol bindings}.
  
  The group has already released, among other documents, a working draft of WSDL
  (Web Services Description Language) 2.0~\cite{wsdl} and an additional document
  which describe bindings of this language to other existing technologies like
  SOAP, HTTP GET and POST methods, MIME~\cite{wsdlbindings}.

 \item[Web Services Choreography Working]
  This ``young'' group\footnote{\url{http://www.w3.org/2002/ws/chor/}},
  started since January 2003, is chartered to design a language that is
  able to describe choreographies of web services. Intend meaning of a
  \emph{Web Service Choreography} is some kind of interaction between
  web services.

  One possible usage of a choreographies is the creation of complex web services
  simply composing simple web services as we compose functions in math. 
\end{description}

\subsection{The Monet project IST-2001-34145}

Web service technologies could be really effective in solving long standing
problems of interapplication communication.  Still, W3C standards provide only a
framework in which this problem could be solved and do not instantiate the
technologies to specific fields of interest.  The road of standardizing and
deploying web service technologies for the special needs of mathematicians has
been took by the European Community funded Monet project~\cite{monet1,monet2}.
Aim of the project, recently completed, was the development of a framework in
which mathematical web services can describe their capabilities in as much
detail as is necessary to allow a sophisticated software agent to select a
suitable service based on an analysis of the characteristics of a user's
problem.

Using standards and technologies developed by the Monet project it is possible
to implement what we call a mathematical \emph{functional search}, that is
finding on the network a web service able to resolve a given mathematical
\emph{problem}\footnote{Monet takes care of several other aspects of
mathematical web services like client-broker architecture, publishing and
discovery of services, planning, orchestration and so on. We will focus our
discussion on the discovery part of Monet}.

Characteristics of mathematical web services in Monet are described in the XML
based language MSDL~\cite{msdl} (Mathematical Service Description Language). An
MSDL document is composed of several parts: classification, implementation
details, service interface and binding descriptions, broker interface and
service metadata. All these data could be used for querying an\emph{Instance
Store} (IS) for available services.

From the point of view of the mathematician, the most interesting part is the
classification, a specification of \emph{what} the service does. Classification
is done on several axis: at each service several classification could be applied
and each of them could be used in user queries.

A first classification is done giving a description of the \emph{mathematical
problems} the service is able to solve. Descriptions include problem inputs,
output and pre/post conditions. For example, minimization of a multivariate
function over the real numbers could be described as follows:
\begin{description}
 \item[Input] $F: \IR^n\to\IR$
 \item[Output] 1. $x\in\IR^n$;\quad 2. $m\in\IR$
 \item[Post-conditions] 1. $F(x)=m$;\quad 2. $\nexists y\in\IR~|~F(y)<m$
\end{description}
MSDL mandates the XML format of such problem descriptions, but not the format
used to describe mathematical formulae like the above one. They are usually
encoded in OpenMath~\cite{openmath} fragments, but they can be MathML
content~\cite{mathml} fragments as well. Additionally, each problem belongs to a
specific class of problems, for example \texttt{definite\_integration} for
problems related to definite integration.

Other interesting ways of classifying mathematical web services in Monet are by
the means of \emph{standardized taxonomies} like GAMS (Guide of Available
Mathematical Software)~\cite{gams} from NIST, and accordingly \emph{algorithms}
implemented by the service.

Once a web service has been described in a MSDL document, it can be registered
to one or more ISs and found by users via queries.

The simplest form of queries is just a MSDL document used as a template: user
fill some fields and leave others empty. For example if we are looking for any
service able to compute the eigenvalues of a matrix, we have simply to create a
fake MSDL description of a service in the GAMS class D4a (``Ordinary eigenvalue
problems''). Unfortunately, Monet has not yet developed any user friendly
interface for writing MSDL documents, and for the moment a user has to manually
write the XML document by hand.

One of the main contribution of Monet is a set of \emph{ontologies} which could
be used by the IS. One ontology is for example defined over the GAMS taxonomy so
that the query engine is able, using an external reasoner over ontologies, to
return not only services in GAMS class D4a for the above example query, but also
services in all subclasses, for example D4a5 (``Ordinary eigenvalue problems on
tridiagonal matrixes'').

However, the most useful way of querying an Instance Store is not the basic
template query, but rather the queries \emph{via user input}. An IS could for
example queried with the following input (properly encoded in OpenMath):
$$\int^{1.0}_{0.0}\sin(x)\,\mathrm{d}x$$

We may now see an interesting use of one of the Monet ontologies: the problem
ontology. In this ontology each class of mathematical problems is associated to
an \texttt{openmath\_head} property which reference an OpenMath symbol likely to
be found in problem instances. For \texttt{definite\_integration} this symbol is
\texttt{defint}, the definite integral symbol $\int^x_y$. Due to the tree
structure of OpenMath formulae the IS could easily match the above user input
with problems of the \texttt{definite\_integration} class and retrieve all the
services computing definite integral.

On user request, the IS could do even more instantiating service inputs from
user input and return to the user directly the result of the integral
computation.

Monet standards are really promising, but in order for them to be useful we
still have to wait for deployment and actual use of related technologies by
widespread mathematical software packages.

\section{Content based searches}
The World Wide Web is already the largest resource of mathematical 
knowledge, however almost all mathematical documents available on the
Web are marked up only for presentation, preventing any attempt
of automation, interoperability,  transformation or processing. 
The long-term goal, in this area, is to overcome these limitations 
passing from a machine-readable to a machine-understandable representation 
of the information. In its deepest semantical sense, this means moving towards
a real formalizations of the mathematical content, that is an essential
prerequisite for most kind of automatic processing.  

The interest around content (or semantic) based functionalities has
been growing in recent years (see e.g.~\cite{pechino,mizarsearchengine,cairns,diffeq,mizarbrowsing}).
For instance,~\cite{diffeq} provides a quite paradigmatic case study.
The problem is to achieve an automatic classification of the differential 
equations appearing in some mathematical document according to a given set
of criteria (comprising e.g. the order, whether is ordinary or partial,
whether it is linear, homogeneous and so on). This implies a 
reconstruction of the semantics of the formula, possibly its transformation
(e.g its normalization to some kind of normal form), and finally its 
analysis. 

The general problems are essentially of three different kinds:
\begin{enumerate}
 \item provide tools which help to automatically reconstruct the mathematical
  content of mathematical expressions (especially meant for legacy documents),
  and/or help to assist a direct content-based authoring of new documents
 \item define and maintain well documented {\em content
  dictionaries}\footnote{We use here the terminology of the OpenMath
  Consortium~\cite{openmath}}, fixing the ontology of relevant fragments of the
  current mathematical notation
 \item developing techniques, languages and tools supporting and exploiting
  innovative content based functionalities.
\end{enumerate}

\subsection{The MoWGLI project IST-2001-33562}
The goal of exploiting content based techniques for mathematical 
knowledge management has been explicitly addressed by the
European Project IST-2001-33562 
MoWGLI\footnote{\url{http://mowgli.cs.unibo.it}} (ending in march 2005).
MoWGLI was also intentionally conceived as a major test-bench for
XML-technology (DOM, Stylesheets, MathML, SVG, RDF, XMLQuery, etc.)
whose extensive use and testing has been a major leitmotif of
the project.

The main technological issues dealt within MoWGLI have been
\emph{rendering} (in particular, rendering engines for MathML),
\emph{Web publishing} (mostly done on the fly from XML sources
via XSLT transformations), and \emph{searching} (via a rich set 
of metadata automatically extracted from the content description 
of the information).

Developing and testing these tools required the possibility of
having at our disposal, and as soon as possible, large collections 
of documents encoded with semantic markup. 
One strategy which has been pursued has been to develop a tool
(called \emph{Hermes}) supporting a latex-based authoring mode for
mathematical articles. 
A more rapid way to get meaningful repositories of fully structured
mathematical knowledge was by exporting them from the available 
libraries of Logical Frameworks and Proof Assistants. In particular
the library of the Coq~\cite{coq} proof assistant developed at INRIA has been
successfully exported into XML and is currently searchable
and browsable by means of MoWGLI's technology at 
\url{http://helm.cs.unibo.it/}.

\subsubsection{Searching via metadata}
One of the main achievement of Mowgli is the feasibility of performing
sophisticated queries via a restricted set of metadata automatically
extracted from the structured representation of the information. The
structural content is essential since it allows to consider the {\em
position} of items in the document as a viable metadata. Although 
canonical indexing techniques like tree automata,
discrimination trees~\cite{McCune}, 
substitution trees~\cite{Graf} or context trees~\cite{Ganzinger} 
can be profitably used in order to solve 
specific matching problems, the metadata approach provide a degree
of flexibility and modularity that goes beyond (and is orthogonal to)
all previous approaches. 

Even in the case of iterated searching finalized to automatic proving
(that is one of the most widely investigated subject in the literature)
the cost of retrieving and applying all matching statements is in
fact neglectable with respect to the exponential grow of the search space
along different branches. Finding good heuristics to control the 
branching factor and having a simple mechanism to filter out 
unwanted solutions is thus more relevant than implementing an
efficient matching algorithm. Metadata provides such a simple, effective 
and absolutely flexible mechanism.

In particular, Mowgli's metadata for mathematical expressions
have the general shape
\[Ref(source,target,position)\]
stating that {\em source} contains a reference to {\em target} at the 
specified {\em  position}.
By suitably describing such a position we may reach the same 
degree of granularity of a substitution tree (where each variable 
marks indeed a different position), thus providing a complete 
description of the term. However, a very minimal set of
``interesting'' positions, that, essentially just discriminates
among hypothesis and conclusions, and root operators from inner
ones, turns out to be already extremely effective.

A prototype implementation of a content based search engine called 
\moogle{} has been
developed at the University of Bologna and is available on the web at 
\url{http://helm.cs.unibo.it}. The engine is used to search the library
of the Coq Proof Assistant \cite{coq}, composed of about 40000 theorems 
in various fields of mathematics. 
\moogle{} supports 4 kinds of queries (see also~\cite{metadata1,metadata2}):
\begin{description}
\item[locate] this query is used to retrieve a mathematical item (theorem,
 definition, lemma, \ldots) from its short name
\item[match] match allows to retrieve a mathematical item from a
pattern provided by the user (possibly containing wild cards).
For instance, we may retrieve a proof of a statement contained in the repository
from the statement itself
\item[elim] Coq is a logical framework based on the Calculus of Inductive
Constructions, and induction is the main logical tool. Several induction
principles (traditionally called elimination principles in this context) 
could be associated to a given datatype. The elim query takes in input a
datatype and gives back the list of its elimination principles
\item[hint] hint is probably the most sophisticated query. It takes
in input a (closed) statement and gives back a list of theorems of
the repository which can be applied to the conclusion of the statement
in the attempt of proving it in a backward fashion. 
\end{description}

\subsubsection{Hermes}
The main problem of semantic-based techniques is still the 
actual authoring cost of semantically enriched documents. 

A second major technical achievement of MoWGLI is the development of an
authoring tool for scientific documents
(Hermes\footnote{\url{http://psyx.org/romeo/hermes/}}) supporting manual and
automatic generation of MathML content, and automatic generation of MathML
presentation, enabling an author to add and recover semantic depth and clarity
to \LaTeX{} written documents.

The prototype implementation of Hermes has the following components:
\begin{itemize}
\item a set of helper \LaTeX\ macros, which allows the author to disambiguate
the meaning of the mathematical expressions he writes, while allowing 
some choices for the presentation; this set is included by the author 
 in the originally written \LaTeX\ document.
A \LaTeX\ run on the macro-enriched document will output a ``semantic DVI'' file
(a DVI file containing ``special'' annotations of various combinations of 
graphical and non-graphical symbols in the source).
\item a scanner which extracts from the resulting DVI 
file the semantic tokens seeded by the macro collection above and sends 
them to the parser below.
\item a parser creating the final content-oriented XML representation. 
\item an XSLT stylesheet, transforming the content-oriented XML document into
a renderable, cross-referenced, document.
\end{itemize}


\begin{thebibliography}{}
 \bibitem{dewey} Dewey Decimal Classification, \url{http://www.oclc.org/dewey/}
 \bibitem{msc2000} Mathematical Subject Classification, American Mathematical
  Society, \url{http://www.ams.org/msc}
 \bibitem{zmath} Zentralblatt MATH, \url{http://www.emis.de/ZMATH/}
 \bibitem{mathscinet} MathSciNet, Mathematical Reviews on the Web,\newline
  \url{http://www.ams.org/mathscinet}
 \bibitem{eram} The Jahrbuch Project Electronic Research Archive for Mathematics
  (ERAM), \url{http://www.emis.de/projects/JFM/}
 \bibitem{euler} EULER - Your Portal to Mathematics Publications,\newline
  \url{http://www.emis.de/projects/EULER/About.html}
 \bibitem{cwi} Centrum voor Wiskunde en Informatica Library,\newline
  \url{http://www.cwi.nl/library/}
 \bibitem{clouds} Hazewinkel, M. Statistics of information clouds.  Discussion
  paper in the framework of the TRIAL SOLUTION project, CWI Amsterdam, 14 Sept.
  2001.
 \bibitem{webservices} Web Services Activity, World Wide Web Consortium,\newline
  \url{http://www.w3.org/2002/ws/}
 \bibitem{semanticweb} Semantic Web, World Wide Web Consortium,\newline
  \url{http://www.w3.org/2001/sw/}
 \bibitem{xml} Tim Bray and Jean Paoli and C. M. {Sperberg-McQueen} and Eve
  Maler (Eds): ``Extensible Markup Language (XML) 1.0 (2nd Edition)'', W3C
  Recommendation (2000), \url{http://www.w3.org/TR/2000/REC-xml-20001006}
 \bibitem{wsdl} Roberto Chinnici et al. eds., ``Web Services Description
  Language (WSDL) Version 2.0 Part 1: Core Language'',
  \url{http://www.w3.org/TR/wsdl20/}
 \bibitem{wsdlbindings} Hugo Haas et al. eds., ``Web Services Description
  Language (WSDL) Version 2.0 Part 3: Bindings'',
  \url{http://www.w3.org/TR/wsdl20-bindings/}
 \bibitem{monet1} O.Caprotti, M.Dewar, D.Turi.  Mathematical Service Matching
  Using Description Logic and OWL.  In Proceeding of the Third International
  Conference on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland.
  LNCS 3119.
 \bibitem{monet2} O.Caprotti, J.H. Davenport, M.Dewar, J.Padget.  Mathematics on
  the (Semantic) NET. In Proceedings of ESWS 2004, First European  Semantic Web
  Symposium. LNCS 3053, pp. 213--224
 \bibitem{msdl} Mathematical Service Description Language: Final Version. The
  MONET Consortium (IST-2001-34145). Deliverable D14,\newline
  \url{http://monet.nag.co.uk/cocoon/monet/publicdocs/monet-msdl-final.pdf}
 \bibitem{openmath} The OpenMath Society, The OpenMath 2.0 Standard,\newline
  \url{http://www.openmath.org/standard/om20-2004-06-30/omstd20html-0.xml}
 \bibitem{mathml} David Carlisle et al. eds., Mathematical Markup Language
  (MathML) Version 2.0 (Second Edition), W3C Recommendation 21 October 2003,
  \url{http://www.w3.org/TR/2003/REC-MathML2-20031021/}
 \bibitem{gams} Guide to Available Mathematical Software,
  \url{http://gams.nist.gov/}
 \bibitem{pechino} A.Asperti, B.Wegner. An Approach to Machine-Understandable
  Representation of the Mathematical Information in Digital Documents.  In:
  Fengshai Bai and Bernd Wegner (eds.): Electronic Information and Communication
  in Mathematics, LNCS vol. 2730, pp. 14--23, 2003
 \bibitem{mizarsearchengine} G. Bancerek, P. Rudnicki. Information Retrieval in
  MML. In Proceedings of the Second International Conference on Mathematical
  Knowledge Management, MKM 2003. LNCS, 2594.
 \bibitem{cairns} P.Cairns. Informalising Formal Mathemtics: Searching the Mizar
  Library with Latent Semantics. In Proceeding of the Third International
  Conference on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland.
  LNCS 3119.
 \bibitem{diffeq} D. Draheim, W. Neun, D. Suliman. Classifying Differential
  Equations on the Web Statements. In Proceeding of the Third International
  Conference on Mathematical Knowledge Management, MKM 2004. LNCS, 3119.
 \bibitem{mizarbrowsing} G. Bancerek, J.Urban. Integrated Semantic Browsing of
  the Mizar Mahemtical Repository. In Proceeding of the Third International
  Conference on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland.
  LNCS 3119.
 \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr}
 \bibitem{McCune} W.McCune. Experiments with discrimination tree indexing and
  path indexing for term retrieval. Journal of Automated Reasoning,
  9(2):147-167, October 1992.
 \bibitem{Graf} P.Graf. Substitution Tree Indexing. Proceedings of the 6th RTA
  Conference, Springer-Verlag LNCS 914, pp. 117-131, Kaiserlautern, Germany,
  April 4-7, 1995.
 \bibitem{Ganzinger} H.Ganzinger, R.Nieuwehuis, P.Nivela.  Fast Term Indexing
  with Coded Context Trees. Journal of Automated Reasoning.  To appear.
 \bibitem{metadata1} F. Guidi, C. Sacerdoti Coen. Querying Distributed Digital
  Libraries of Mathematics. In Proceedings of Calculemus 2003, 11th Symposium on
  the Integration of Symbolic Computation and Mechanized Reasoning.  Aracne
  Editrice.
 \bibitem{metadata2} A. Asperti, M. Selmi. Efficient Retrieval of Mathematical
  Statements. In Proceeding of the Third International Conference on
  Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland. LNCS 3119.
\end{thebibliography}

\end{document}