XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy
XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy
复制标题
XML 化 Mizar：使 MML 的语义处理和表示变得容易
DOI：
10.1007/11618027_23
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Urban
中科院分区：
文献类型：
--
作者：
J. Urban
自7.2版本以来，Mizar系统在验证过程中为Mizar文章提供了非常详细的基于XML的语义描述。这种格式现在用于Mizar完成的大多数处理，例如，也是整个Mizar内部数据库。切换到这种基于XML的表示的主要动机是使与Mizar的语义通信和MML的表示更容易被各种外部工具和系统访问。本文简要描述了这种格式及其当前实现，并展示了其用法示例。这些例子包括在支持XML的现代浏览器（如Mozilla）中展示链接的Mizar文章，在Emacs的Mizar模式下提供创作帮助，以及在Mizar数学库上加载基于XML的查询语言（如XQuery）到本地XML数据库（如eXist）的实验。这项工作使得目前最大的正式数学库可用于许多种表示，数据挖掘和自动推理应用程序和实验，本文的目标也是鼓励，促进和提供食谱，为开发这样的应用程序。
Since version 7.2 the Mizar system produces quite detailed XML-based semantic description of Mizar articles during their verification. This format is now used natively for most of the processing done by Mizar, e.g., also for the whole Mizar internal database. The main motivation for switching to this XML-based representation is to make semantic communication with Mizar and presentation of the MML more accessible to a variety of external tools and systems. This article briefly describes this format and its current implementation, and shows examples of its usage. These examples include presentation of linked Mizar articles in modern XML-capable browsers like Mozilla, authoring assistance in the Mizar mode for Emacs, and experiments with XML-based querying languages like XQuery over the Mizar Mathematical Library loaded into a native XML databases like eXist. This work makes the currently largest repository of formal mathematics available to many kinds of presentational, data-mining, and automated reasoning applications and experiments, and the goal of this article is also to encourage, facilitate and provide recipes for the development of such applications.