Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
Kazuhisa Nakasho, Yasunari Shidama

TL;DR
This paper presents a documentation generator that organizes symbol information from the HTML-ized Mizar library, enhancing accessibility and usability for proof system users by providing features like symbol lists and search.
Contribution
It introduces a novel symbol-focused documentation system for the Mizar library, inspired by API reference models, improving navigation and reference for proof assistants.
Findings
Implemented a symbol-centric documentation system
Features include symbol list, incremental search, referrer list
Supports users of proof assistance systems
Abstract
The purpose of this project is to collect symbol information in the Mizar Mathematical Library and manipulate it into practical and organized documentation. Inspired by the MathWiki project and API reference systems for computer programs, we developed a documentation generator focusing on symbols for the HTML-ized Mizar library. The system has several helpful features, including a symbol list, incremental search, and a referrer list. It targets those who use proof assistance systems, the volume of whose libraries has been rapidly increasing year by year.
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.
Taxonomy
TopicsMathematics, Computing, and Information Processing · History and Theory of Mathematics
