HELM logo

Hypertextual Electronic Library of Mathematics



The HELM project is meant to integrate the current tools for the automation of formal reasoning and the mechanization of mathematics (proof assistants and logical frameworks) with the most recent technologies for the development of web applications and electronic publishing, eventually passing through the Extensible Markup Language. The final aim is the development of a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge.

In contrast with current digital libraries, where the real document is usually considered as a single ``text'' element, preventing any automatic elaboration of its content, as well as any form of internal navigation, our purpose is that of modeling the inner structure of mathematical documents, at different levels of detail.

The broad goal of the project goes far beyond the trivial suggestion to adopt XML as a neutral specification language for the ``compiled'' versions of the libraries, or even the observation that in this way we could take advantage of a lot of functionalities on XML-documents already offered by standard commercial tools.

First of all, having a common, application independent, meta-language for mathematical proofs, similar software tools could be applied to different logical dialects, regardless of their concrete nature. This would be especially relevant for all those operations like searching, retrieving, displaying or authoring (just to mention a few of them) that are largely independent from the specific logical system.

Moreover, if having a common representation layer is not the ultimate solution to all inter-operability problems between different applications, it is however a first and essential step in this direction.

Finally, this ``standardization'' process naturally leads to a substantial simplification and re-organization of the current, ``monolithic'' architecture of logical frameworks. All the many different and often loosely connected functionalities of these complex programs (proof checking, proof editing, proof displaying, search and consulting, program extraction, and so on) could be clearly split in more or less autonomous tasks, possibly (and hopefully!) developed by different teams, in totally different languages.

This is the new, content-centric architectural design of future systems.

Page maintained by Andrea Asperti.
Page hosted by Department of Computer Science, University of Bologna, Italy.