
TL;DR
This paper presents a web-based interface for the Matita proof assistant that enhances user experience with annotations and active elements, supporting all core functionalities of the traditional interface.
Contribution
It introduces a web interface for Matita that integrates annotations and semantic elements to improve usability and proof processing efficiency.
Findings
Supports all basic functionalities of the local interface
Enriches documents with annotations for readability and processing
Stores automatic information to optimize proof re-execution
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
