Building Interactive Digital Libraries of Formal Algorithmic Knowledge |
|
Building Interactive Digital Libraries of Formal Algorithmic Knowledge |
|
|
The Helm system has been developed by Andrea Asperti's group at the University of Bologna. The following is a quote from their web-page describing the project.
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. HelmFrom the point of view of digital libraries of formalized mathematics, we believe that methods of accounting for the mathematics is crucial. The Helm group is embarked on a program of brokering formalized mathematics on the web -- independent from the developers of the proof tools and those who have developed the library content. In collaboration with the Italian group, XML style sheets for displaying Nuprl proofs have been designed. The Helm display is distinguished from the display of the same material on the Prl pages in that we show (for proofs in the left column) the primitive rules generated by each tactic invocation. This is valuable information for those wanting to learn what the tactics do and to inspect proofs at their lowest level. The project is in progress and we are adding new proofs every day.