Non-Automatizability of Bounded-Depth Frege Proofs
Non-Automatizability of Bounded-Depth Frege Proofs
复制标题
有界深度弗雷格证明的非自动化性
DOI：
10.1007/s00037-004-0183-5
复制
发表时间：
1999
影响因子：
1.4
通讯作者：
T. Pitassi
中科院分区：
文献类型：
--
作者：
Maria Luisa Bonet;Carlos Domingo;Ricard Gavaldà;Alexis Maciel;T. Pitassi
摘要：在本文中，我们将展示如何扩展Bonet，Pitassi和Raz的论点，以表明有界深度的Frege证明没有可行的插值，假设Blum整数的因式分解或计算Diffie-Hellman函数足够困难。由此推论，有界深度的弗雷格是不可自动化的;换句话说，没有确定性的多项式时间算法可以输出一个简短的证明（如果存在的话）。我们的论点的一个显著特点是它的简单性。
Abstract.In this paper, we show how to extend the argument due to Bonet, Pitassi and Raz to show that bounded-depth Frege proofs do not have feasible interpolation, assuming that factoring of Blum integers or computing the Diffie–Hellman function is sufficiently hard. It follows as a corollary that bounded-depth Frege is not automatizable; in other words, there is no deterministic polynomial-time algorithm that will output a short proof if one exists. A notable feature of our argument is its simplicity.