交互式定理证明的程序式与陈述式风格的综合
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
摘要：
我们提出了一个综合的两个证明风格的交互式定理证明：程序风格（其中证明是脚本的命令，如在Coq）和声明式风格（其中证明是文本在一个受控的自然语言，如在Isabelle/Isar）。我们的方法结合了声明式风格的优点-编写正式证明的可能性，如正常的数学文本-和程序风格-强大的自动化和帮助形成的证明，包括确定中间步骤的声明。我们的方法是新的，显着不同的方式，程序和声明式的证明风格已经结合在伊莎贝尔，Ssreflect和Matita系统。我们的方法是通用的，可以实现任何程序的交互式定理证明器，无论其架构和逻辑基础。为了展示我们提出的方法的可行性，我们将其完全实现为一个名为miz 3的证明接口，位于HOL Light交互式定理证明器之上。这个接口使用的声明式语言是Mizar系统语言的一个轻微变体，可以用于任何交互式定理证明器，无论其逻辑基础如何。miz 3界面允许轻松访问HOL Light的全套战术和正式库，因此具有“工业实力”。我们的方法提供了一种方法，自动转换任何程序的证明，一个声明的副本，其中转换后的证明是类似的大小，原来的。由于所有的声明式系统本质上都有相同的证明语言，这提供了一种在交互式定理证明器之间移植证明的简单方法。
英文摘要：
We propose a synthesis of the two proof styles of interactive theorem proving: the procedural style (where proofs are scripts of commands, like in Coq) and the declarative style (where proofs are texts in a controlled natural language, like in Isabelle/Isar). Our approach combines the advantages of the declarative style - the possibility to write formal proofs like normal mathematical text - and the procedural style - strong automation and help with shaping the proofs, including determining the statements of intermediate steps. Our approach is new, and differs significantly from the ways in which the procedural and declarative proof styles have been combined before in the Isabelle, Ssreflect and Matita systems. Our approach is generic and can be implemented on top of any procedural interactive theorem prover, regardless of its architecture and logical foundations. To show the viability of our proposed approach, we fully implemented it as a proof interface called miz3, on top of the HOL Light interactive theorem prover. The declarative language that this interface uses is a slight variant of the language of the Mizar system, and can be used for any interactive theorem prover regardless of its logical foundations. The miz3 interface allows easy access to the full set of tactics and formal libraries of HOL Light, and as such has "industrial strength". Our approach gives a way to automatically convert any procedural proof to a declarative counterpart, where the converted proof is similar in size to the original. As all declarative systems have essentially the same proof language, this gives a straightforward way to port proofs between interactive theorem provers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
