Applications of inductive definitions and choice principles to program synthesis
Applications of inductive definitions and choice principles to program synthesis
复制标题
归纳定义和选择原则在程序综合中的应用
DOI：
10.1093/acprof:oso/9780198566519.003.0008
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Seisenberger Monika
中科院分区：
文献类型：
--
作者：
Seisenberger Monika
我们描述了两种方法提取建设性的内容，从经典的证明，专注于涉及无穷序列和非建设性的选择原则的定理。第一种方法删除了对无穷序列的任何引用，并将定理转换为归纳定义的系统，另一种方法结合了哥德尔的否定和弗里德曼的A-翻译。这两种方法都解释了Higman引理及其著名的经典证明，由于纳什-威廉姆斯的案例研究。我们还讨论了一些证明理论的优化，这是至关重要的形式化和实施这项工作的交互式证明系统Minlog。
We describe two methods of extracting constructive content from classical proofs, focusing on theorems involving infinite sequences and nonconstructive choice principles. The first method removes any reference to infinite sequences and transforms the theorem into a system of inductive definitions, the other applies a combination of Gödel’s negativeand Friedman’s A-translation. Both approaches are explained by means of a case study on Higman’s Lemma and its well-known classical proof due to Nash-Williams. We also discuss some proof-theoretic optimizations that were crucial for the formalization and implementation of this work in the interactive proof system Minlog.