交互式定理证明中过程式与声明式风格的综合
计算机科学中的逻辑
2015-07-01 v2
摘要
我们提出了交互式定理证明中两种证明风格的综合：过程式风格（其中证明是命令脚本，如 Coq）和声明式风格（其中证明是受控自然语言文本，如 Isabelle/Isar）。我们的方法结合了声明式风格的优势（能够像正常数学文本一样编写形式化证明）和过程式风格的优势（强大的自动化以及辅助塑造证明，包括确定中间步骤的陈述）。我们的方法是全新的，与之前在 Isabelle、Ssreflect 和 Matita 系统中结合过程式和声明式证明风格的方式有显著不同。我们的方法具有通用性，可以实现在任何过程式交互式定理证明器之上，无论其架构和逻辑基础如何。为了展示我们所提方法的可行性，我们在 HOL Light 交互式定理证明器之上将其完全实现为一个名为 miz3 的证明接口。该接口使用的声明式语言是 Mizar 系统语言的轻微变体，可用于任何交互式定理证明器，无论其逻辑基础如何。miz3 接口允许轻松访问 HOL Light 的全套策略和形式化库，因此具有“工业级强度”。我们的方法提供了一种将任何过程式证明自动转换为相应声明式证明的途径，且转换后的证明规模与原始证明相似。由于所有声明式系统本质上具有相同的证明语言，这为在交互式定理证明器之间移植证明提供了一条直接的途径。
引用
@article{arxiv.1201.3601,
title = {A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving},
author = {Freek Wiedijk},
journal= {arXiv preprint arXiv:1201.3601},
year = {2015}
}