Literate Proving: Presenting and Documenting Formal Proofs
Literate Proving: Presenting and Documenting Formal Proofs
复制标题
文字证明：呈现和记录形式证明
DOI：
10.1007/11618027_11
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Gow
中科院分区：
文献类型：
--
作者：
P. Cairns;J. Gow
文学证明类似于数学领域的文学编程。也就是说，文字证明的目标是让人类对形式数学进行清晰的阐述，甚至可以让人们阅读起来很愉快，同时保持对实际证明的忠实表示。本文描述了迷宫，一种通用的识字证明系统。作者使用任意 XML 标记正式证明文件（例如 Mizar 文件），并使用迷宫来获取选定的摘录并将其转换为演示文稿，例如作为乳胶。为了帮助其使用，maze 内置了转换功能，包括漂亮的打印和校样草图，以便包含在 LATEX 文档中。这些转变挑战了文字证明中的忠实性概念，但有人认为这应该是文字证明与文字编程的一个显着特征。
Literate proving is the analogue for literate programming in the mathematical realm. That is, the goal of literate proving is for humans to produce clear expositions of formal mathematics that could even be enjoyable for people to read whilst remaining faithful representations of the actual proofs. This paper describes maze, a generic literate proving system. Authors markup formal proof files, such as Mizar files, with arbitary XML and use maze to obtain the selected extracts and transform them for presentation, e.g. as LATEX. To aid its use, maze has built in transformations that include pretty printing and proof sketching for inclusion in LATEX documents. These transformations challenge the concept of faithfulness in literate proving but it is argued that this should be a distinguishing feature of literate proving from literate programming.