高阶逻辑在可行性中的一些应用
摘要：基本可行泛函类具有递归论性质，自然推广了可行函数类的相应性质。我们还改进了Kapron-Cook关于基本可行泛函机器表示的结果。我们的证明基于逻辑的重要应用。我们引入了一个弱的二阶算术片段，其中二阶变量范围从N到N的函数适当地表征了基本可行泛函，并且显示它是研究基本可行泛函性质的有用工具。特别是，我们提供了一个示例，说明如何从使用非可行泛函（如二阶多项式）的数学证明中提取可行"程序"。
作者：Aleksandar Ignjatovic and Arun Sharma
论文ID：cs/0204045
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23