The MathQL proposal rises in the context of the HELM project, which aims at the development of a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of structured mathematical knowledge based on XML technology, through the integration of the current proof assistants and logical frameworks with the most recent technologies for the development of Web applications and electronic publishing.
The objective of the MathQL proposal is the development of a set of query languages enabling the retrieval of formalized mathematical Web resources on the basis of content-aware requests. The first of these languages, MathQL-1, is focused on querying an arbitrary RDF database because RDF is the W3C standard for describing Web resources at the general-purpose content level.
As an RDF query language, MathQL-1 provides the main features required by the RDF community while complying with the needs of HELM. The peculiar aspects of this language concern the query results, which are highly structured and possess their own syntax, formally explained by a rigorous semantics.
MathQL-1 is particularly helpful in distributed systems where query engines are implemented as stand-alone units, because in this situation the query results are exchanged between the system components as well as the queries, and thus both the queries and the query results need to be encoded in a clearly defined format.
Other languages to be developed in the context of the MathQL proposal will be suitable for queries about the semantic structure of mathematical data: this will include content-based pattern-matching (MathQL-2) and possibly other forms of formal matching involving for instance isomorphism, unification and definitions expansion (MathQL-3).