为依赖类型高阶逻辑添加选择公理，提升形式化证明能力。
Experiments with Choice in Dependently-Typed Higher-Order Logic
- 引入希尔伯特不定选择算子ε扩展类型系统
- 实现从依赖型高阶逻辑到普通高阶逻辑的完整翻译
- 在需选择公理的问题上验证了方法有效性
最近提出了一种名为DHOL的高阶逻辑扩展，引入依赖类型，形成强大的外延类型理论。本文提出两种将选择公理加入DHOL的方法：通过引入希尔伯特的不定选择算子ε扩展项结构；定义一种将选择项翻译为普通高阶逻辑选择的映射，并证明该翻译是完整的，且具备可靠性。最后，在一组需要选择公理的依赖型高阶逻辑问题上评估了该扩展翻译的有效性。
原文摘要 · Abstract (English)
Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert's indefinite choice operator $ε$, define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and show that the extension of the translation is complete and give an argument for soundness. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。