|
|
Implementation
The MathQL-1 Suite for HELM is implemented in Caml and is currently available through
the HELM CVS repository.
The Suite provides the following software components:
- The basic Caml package for MathQL-1 (mathql)
provides a HELM independent Caml
representation of queries and query results, plus some general purpose utilities.
- The MathQL-1 interpreter (mathql_interpreter)
provides the proper search engine and is now HELM independent.
- The HELM query generator (mathql_generator)
allows to build specific kinds of MathQL-1 queries, which are meaningful
in the context of HELM, starting from a high-level description of the wanted
results. These queries are described at an abstract level in the following
paper:
- F. Guidi and C. Sacerdoti Coen: Querying Distributed Digital Libraries
of Mathematics. In Proc. of the 11th Symposium on the Integration of
Symbolic Computation and Mechanized Reasoning (Calculemus 2003). Rome, Italy,
September 2003. pages 17-30, Aracne. 2003.
- The testing software for the MathQL-1 Suite (mathql_test)
provides three textual interfaces (one for the basic package, one for the
interpreter and one for the query generator) with specific features meant
for testing.
The current version of the Suite, realized entirely by F. Guidi, implements
MathQL-1 version 3 (i.e. MathQL-1.3). The newly implemented features, which
are not included in the official documentation
yet, are reported in the What's new section.
The latest HELM
query engine (enter here
if you are behind a restrictive firewall), powered by MathQL-1.3, allows
to issue both user-defined queries and the specific queries produced by the
HELM query generator.
|