一个无量词的字符串理论用于ALOGTIME推理
摘要：一个适用于形式化ALOGTIME推理的无量词的字符串理论T\_1的定义是本研究的主要贡献。在描述基于字符串而不是数字的复杂度类ALOGTIME的新的、简单的代数特征L\_1之后，定义了T\_1理论（基于L\_1），并给出了T\_1的详细形式化发展。然后，将T\_1的定理转化为具有均匀多项式大小的Frege证明的命题永真式的系列，并且显示了T\_1证明了特定Frege系统F的正确性，并且F被证明能够在T\_1中可证明地p-模拟任何可以在T\_1中证明正确性的证明系统。最后，将T\_1与文献中的其他ALOGTIME推理理论进行了比较。据我们所知，这是第一个将基本对象定义为字符串而不是数字的ALOGTIME推理的形式化理论，并且是第一个无量词的理论，具有直接给出某个Frege系统的正确性的证明（在一阶理论的情况下，Arai首次给出了这样的证明）。此外，我们给出的T\_1定理的命题转化的多项式大小的Frege证明要比其他理论简单得多，我们对T\_1中特定F系统的正确性的证明也是如此。加上T\_1的递归方案、公理和规则的简单性，这些事实表明T\_1是可用于ALOGTIME推理的最自然的理论之一。
作者：Franc{c}ois Pitt
论文ID：cs/0702160
分类：Computational Complexity
分类简称：cs.CC
提交时间：2007-05-23