用IZF从构造性HOL证明中抽取程序<br>语义
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> Semantics
摘要：
丘奇的高阶逻辑是有影响的证明助手-- HOL和PVS的基础。Church的逻辑有一个简单的集合论语义，使其可信和可扩展。我们因素HOL到一个建设性的核心加上公理的排中律和选择。我们同样的因素标准集理论，ZFC，到一个建设性的核心，IZF，公理排除中间和选择。然后，我们提供了标准的集合论语义，这样的方式，建设性的核心HOL映射到IZF。我们使用的析取，数值存在性和长期存在的IZF属性提供了一个程序提取能力，从证明建设性的核心。我们可以用两种不同的方式实现析取和数值存在性：一种是使用Rathjen对IZF的可实现性，另一种是使用Moczydlowski对IZF的一个新的直接弱归一化结果。后者也可以用于术语存在属性。
英文摘要：
Church's Higher Order Logic is a basis for influential proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. We factor HOL into a constructive core plus axioms of excluded middle and choice. We similarly factor standard set theory, ZFC, into a constructive core, IZF, and axioms of excluded middle and choice. Then we provide the standard set-theoretic semantics in such a way that the constructive core of HOL is mapped into IZF. We use the disjunction, numerical existence and term existence properties of IZF to provide a program extraction capability from proofs in the constructive core. We can implement the disjunction and numerical existence properties in two different ways: one using Rathjen's realizability for IZF and the other using a new direct weak normalization result for IZF by Moczydlowski. The latter can also be used for the term existence property.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
