专注于HTML化的Mizar库的符号的文档生成器
Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
摘要：
这个项目的目的是收集Mizar数学图书馆中的符号信息，并将其转化为实用和有组织的文档。受MathWiki项目和计算机程序的API参考系统的启发，我们开发了一个文档生成器，专注于HTML化的Mizar库的符号。该系统有几个有用的功能，包括一个符号列表，增量搜索，和一个查询列表。它针对的是那些使用证明辅助系统的人，他们的图书馆数量逐年迅速增加。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
