A Web Interface for Matita

From MaRDI portal
Publication:2907340

DOI10.1007/978-3-642-31374-5_28zbMATH Open1360.68739arXiv1207.2892OpenAlexW3122284613MaRDI QIDQ2907340FDOQ2907340


Authors: Andrea Asperti, Wilmer Ricciotti Edit this on Wikidata


Publication date: 7 September 2012

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: This article describes a prototype implementation of a web interface for the Matita proof assistant. The interface supports all basic functionalities of the local Gtk interface, but takes advantage 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 of the script. The latter kind comprises information automatically generated by the proof assistant during previous compilations, and stored to improve the performance of re-executing expensive operations like disambiguation or automation.


Full work available at URL: https://arxiv.org/abs/1207.2892







Cited In (1)

Uses Software





This page was built for publication: A Web Interface for Matita

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2907340)