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 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.shtml
2012
A. Asperti; W.Ricciotti
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/127276
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact