The work, presented at the International Conference on Computer Intelligent Mathematics (CICM 2012), consists in a prototype implementation of a web interface for the Matita proof assistant, aiming in particular to the following goals: 1. creation of a web collaborative working environment for interactive theorem proving, in order to foster knowledge-intensive cooperation, content creation and management; 2. exploitation of the markup to enrich the document with several kinds of annotations or active elements; annotations may have both a presentational/ hypertextual nature, aimed to improve the quality of the proof script as a human readable document, or a more semantic nature, aimed to help the system in its processing (or re-processing) of the script; 3. platform independence with respect to operating systems, and wider accessibility also for users using devices with limited resources; 4. overcoming the installation issues typical of interactive provers, also in view of attracting a wider audience, especially in the mathematical community. The interface is accessible at the following url: http://matita.cs.unibo.it/matitaweb.shtml
A. Asperti, W.Ricciotti (2012). A Web Interface for the Matita Proof Assistant.
A Web Interface for the Matita Proof Assistant
ASPERTI, ANDREA;RICCIOTTI, WILMER
2012
Abstract
The work, presented at the International Conference on Computer Intelligent Mathematics (CICM 2012), consists in a prototype implementation of a web interface for the Matita proof assistant, aiming in particular to the following goals: 1. creation of a web collaborative working environment for interactive theorem proving, in order to foster knowledge-intensive cooperation, content creation and management; 2. exploitation of the markup to enrich the document with several kinds of annotations or active elements; annotations may have both a presentational/ hypertextual nature, aimed to improve the quality of the proof script as a human readable document, or a more semantic nature, aimed to help the system in its processing (or re-processing) of the script; 3. platform independence with respect to operating systems, and wider accessibility also for users using devices with limited resources; 4. overcoming the installation issues typical of interactive provers, also in view of attracting a wider audience, especially in the mathematical community. The interface is accessible at the following url: http://matita.cs.unibo.it/matitaweb.shtmlI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
