Relativized Propositional Calculus
定义并比较了相对化命题演算的证明系统。
2012-03-09 cs.CC
Semi-Algebraic Proof Systems for QBF
本文针对量化布尔公式（QBF）提出类似命题半代数系统的新证明系统，结合QBF策略提取与命题证明复杂性技术，得到强下界及系统分离结果，且不受命题硬度影响。
2025-11-11 cs.CC cs.LO math.LO
On Counting Propositional Logic
我们研究计数命题逻辑作为命题逻辑与计数量词的扩展。我们证明，基本的决策问题的复杂性完全匹配瓦格纳的计数层次的适当水平，而且由此产生的逻辑承认一个令人满意的证明理论治疗。从后者，一个类型系统中的概率演算的Curry-Howard对应的精神，显示了潜在的计数命题逻辑作为一个有用的工具，在几个领域的理论计算机科学。
2021-06-03 cs.CC cs.LO cs.PL
Characterizing Propositional Proofs as Non-Commutative Formulas
每个布尔重言式都有一个简短的命题演算证明吗？这里，命题演算（即弗雷格）证明是从一组公理开始并使用一组固定的合理推导规则推导新的布尔公式的证明。在弗雷格证明上建立任何超多项式大小的下限（就证明公式的大小而言）是证明复杂性中的一个主要开放问题，也是复杂性理论中少数基本困难问题之一。另一方面，非交换算术公式构成了一个相当弱的计算模型，早在1991年，Nisan [Nis 91]就已经证明了它的指数大小下界，他使用了一个特别透明的论点。在这项工作中，我们表明，弗雷格下界实际上遵循相应的大小下界的非交换公式计算某些多项式（和这种下界的非交换公式必须存在，除非NP=coNP）。更确切地说，我们证明了重言式$T$与非交换多项式$p$之间的自然关联，使得：如果$T$具有多项式大小的弗雷格证明，则$p$具有多项式大小的非交换算术公式;相反，当$T$是DNF时，如果$GF(2)$具有多项式大小的非交换算术公式，则$T$具有准多项式大小的弗雷格证明。
2015-09-11 cs.CC math.LO
Information in propositional proofs and algorithmic proof search
我们从证明复杂性的角度研究（非正式）证明搜索问题：是否有一个最佳的方法来搜索命题证明？我们注意到，对于任何固定的证明系统，存在一个时间最优的证明搜索算法。利用经典的证明复杂性的反射原理的结果，我们证明了一个时间最优的证明搜索算法存在不限制证明系统当且仅当一个p-最优证明系统存在。为了精确地描述单个公式所需的时间证明搜索算法，我们引入了一种新的基于算法信息概念的证明复杂性度量。特别地，对于证明系统$P$，我们附加{ \bf信息效率函数} $i_P(τ)$，将重言式分配给自然数，并且我们表明：- $i_P(τ)$表征任何$P$证明搜索算法必须在$τ$上使用的时间，并且对于固定的$P$，存在这样的信息最优算法，-证明系统是信息效率最优的当且仅当它是p最优的，- 对于不可自动化的系统$P$，存在具有短证明但具有大信息测度$i_P(τ)$的公式$τ$。我们隔离和激励的问题，建立无条件的超对数下限$i_P(τ)$没有超多项式大小的下限是已知的。我们还指出了新的措施与其他证明搜索的证明复杂性的一些主题的连接。
2021-09-05 cs.CC math.LO
Proof complexity of systems of (non-deterministic) decision trees and branching programs
本文研究命题证明系统中的行序列的决策树或分支程序-确定性和非确定性。系统LDT和LNDT是命题证明系统，其中线表示确定性或非确定性决策树。分支程序被建模为决策dags。将扩展添加到LDT和LNDT给出系统eLDT和eLNDT，其中行分别表示确定性和非确定性分支程序。确定性和非确定性分支程序分别对应于对数空间（L）和非确定性对数空间（NL）。因此系统eLDT和eLNDT是用（非一致）L和NL属性推理的命题证明系统。本文的主要结果是仿真和非仿真结果的树型和dag样的证明系统LDT，LNDT，eLDT，和eLNDT。并与Frege系统、常深度Frege系统和扩展Frege系统作了比较
2019-10-18 cs.CC cs.LO math.LO
On optimal heuristic randomized semidecision procedures, with application to proof complexity
（p-）最优命题证明系统的存在性是（证明）复杂性中的一个主要公开问题;许多人猜测这样的系统不存在。Krajicek和Pudlak（1989）证明了这个问题等价于存在一个算法，这个算法在所有的命题重言式上都是最优的。Monroe（2009）最近给出了一个猜想，暗示这样的算法不存在。我们表明，在错误的存在下，这样的最佳算法确实存在。这个概念的动机是启发式算法的概念。也就是说，我们允许算法声称少量的假“定理”（根据任何采样分布的非重言式）和错误的有界概率在其他输入。我们的结果也可以被看作是存在的最佳证明系统在一类证明系统通过推广自动化证明系统。
2010-02-03 cs.CC cs.LO
Comments on Beckmann's Uniform Reducts
Arnold Beckmann将命题证明系统f的一致约简定义为那些有界算术公式的集合，这些算术公式的命题翻译具有多项式大小的f-证明。证明了f + Extended Frege的一致约简包含所有真有界算术公式当且仅当f + Extended Frege模拟了所有证明系统。
2006-01-23 cs.CC
Proof Complexity and the Kneser-Lovász Theorem
我们研究了一类命题公式的证明复杂性，这些公式表达了一个被称为Kneser-Lovász定理的组合原理。这是一个命题重言式族，由一个非负整数参数$k$索引，它推广了鸽子洞原理（为$k=1$获得）。我们表明，对于所有固定的$k$，$2^{Ω(n)}$下界分辨率的复杂性和指数下界有界深度弗雷格证明。这些结果甚至适用于更严格的一类公式编码Schrijver的加强Kneser-Lovász定理。另一方面，对于$k=2,3$（Kneser-Lovász定理的组合证明是已知的）的情况下，我们给出多项式大小的弗雷格（$k=2$），分别扩展弗雷格（$k=3$）的证明。本文最后简要宣布了Kneser-Lovász定理一般情况下证明复杂性的结果（在随后的工作中提出）。
2018-05-15 cs.CC cs.LO
Learning algorithms versus automatability of Frege systems
University of Oxford（牛津大学）
我们连接学习算法和算法自动证明搜索命题证明系统：对于每一个足够强，良好的命题证明系统$P$，我们证明以下语句是等价的，1。可证明的学习：$P$有效地证明了均匀分布上的次指数规模电路在成员查询下是可学习的。2.可证明的自动化能力：$P$有效地证明了$P$是可自动化的非均匀电路上的命题公式表示的p-大小电路下界。在这里，$P$是足够强大和良好的行为，如果我。三. holds：I. $P$ p-模拟了Jeanábek的系统$WF$（它通过满射弱鸽子洞原理加强了扩展弗雷格系统$EF$）; II. $P$满足标准证明系统的一些基本性质，这些证明系统p-模拟$WF$ ; III. $P$有效地证明了对于某些布尔函数$h$，$h$对于次指数规模的电路是平均困难的。例如，如果III。对于$P=WF$成立，则第1项和第2项对于$P=WF$是等效的。如果存在一个函数$h\in NE\cap coNE$，它对于大小为$2^{n/4}$的电路平均来说是困难的，对于每个足够大的$n$，则存在一个满足性质I的显式命题证明系统$P$。三、即第1项和第2项的等价性适用于$P$。
2021-11-20 cs.CC cs.LG cs.LO
Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
Jeanábek表明，在深度推理中，经典命题逻辑证明中的切割可以在准多项式时间内消除。证明是间接的，它依赖于Atserias，Galesi和Pudlák关于单调微积分的结果以及该系统与无割深度推理证明之间的对应关系。本文给出了Jeábek结果的一个直接证明：给出了经典命题逻辑在深度推理中的一个拟多项式时间截消过程。主要的新成分是使用了一种称为原子流的深层推理证明的计算跟踪，它既非常简单（它们只跟踪结构规则，而忘记了逻辑规则），又足够强大，可以忠实地表示切消过程。
2016-05-02 cs.CC cs.LO
Uniform, Integral and Feasible Proofs for the Determinant Identities
为了提供尽可能弱的公理化假设，在此基础上发展基本线性代数，我们给出了Hrubes-Tzameret [SICOMP'15]中关于$GF(2)$上行列式恒等式的简短命题证明的统一和完整版本.具体来说，我们证明了整数的行列式函数和凯莱-汉密尔顿定理的乘法证明有界算术理论$\mathbf{VNC}^2$，后者是一个一阶理论对应的复杂性类$\mathbf{NC}^2$组成的问题可解决的多项式大小的电路和$O(\log ^2 n)$ -深度的统一家庭。这也建立了整数上的基本行列式恒等式的均匀多项式大小的$\mathbf{NC}^2$ -弗雷格证明的存在性（以前的命题证明只在二元域上成立）。
2018-11-10 cs.CC cs.LO math.LO
Kernelization, Proof Complexity and Social Choice
我们展示了核化和数据简化的概念从参数化复杂性到证明复杂性的应用：具体来说，我们证明了参数化问题的数据简化规则的存在性（a）。小长度减速链，和（b）.小尺寸（扩展）弗雷格证明证明的合理性减少步骤意味着存在的次指数大小（扩展）弗雷格证明的命题形式化的给定问题。我们应用我们的结果来推断存在的次指数弗雷格和扩展弗雷格证明各种问题。改进了Aisenberg等人（ICALP 2015）的早期结果，我们证明了表达Kneser-Lovász定理（更强形式）的命题公式对于参数k的每个常数值都有多项式大小的Frege证明。以前只知道拟多项式的界（并且只知道普通的Kneser-Lovász定理）。我们的框架的另一个值得注意的应用是不可能的结果在计算社会选择：我们表明，对于任何固定数量的代理，命题翻译的箭头和Gibbard Satterthwaite不可能定理有次指数大小的弗雷格证明。
2021-04-28 cs.CC cs.DS cs.GT
Towards Uniform Certification in QBF
本文提出一种新技术，将策略提取与局部论证相结合，证明扩展 QBF Frege 可 p-模拟多种子句证明系统，从而支持 QBF 求解中的统一认证。
2024-02-12 cs.CC cs.LO
Proofs, Circuits, and Communication
我们调查下界的复杂性理论，已通过新发现的命题证明复杂性，布尔电路复杂性，查询/通信复杂性之间的相互联系。我们主张总搜索问题（TFNP）的理论作为这些连接的统一语言，并讨论如何从这个角度提出了一个整体方案，进一步研究。
2022-02-17 cs.CC
Proof Complexity and Feasible Interpolation
本文综述命题证明复杂性基础，重点介绍可行插值方法及其在构造经典与非经典逻辑证明系统中超多项式长度困难定理方面的应用。
2025-05-05 cs.CC math.LO
On proof theory in computational complexity: overview
在[GH1]和[GH2]（也见[GH3]）中，我们给出了等式NP = coNP = PSPACE的充分证明。这些结果已经得到了新的证明理论树到dag压缩技术，适合Prawitz的自然演绎（ND）的命题最小逻辑加上相应的Hudelmaier的无割演算。在本文中，我们提出了一个概述我们的证明。
2022-01-09 cs.CC
Algebraic Proofs over Noncommutative Formulas
我们研究了代数命题证明系统与非交换公式操作的可能配方。我们观察到，一个简单的公式产生了至少像弗雷格一样强大的系统-产生了一种语义方式来定义一个Cook-Reckhow（即，多项式验证）代数模拟弗雷格证明，不同于[BIKPRS 96，GH 03]。然后，我们转向一个明显较弱的系统，即多项式演算（PC），其中多项式被写为有序公式（PC over ordered formulas，简称）：有序多项式是一个非交换多项式，其中每个单项式中的乘积的顺序都是变量的固定线性顺序;如果由每个子公式计算的多项式是有序的，则代数公式是有序的。我们表明，PC有序公式是严格强于决议，多项式演算和多项式演算与决议（PCR），并承认多项式大小反驳鸽子洞原则和Tseitin的公式。最后，我们提出了一种方法，建立下界PC上的顺序公式证明，和相关的系统，根据非交换公式的下界的性质。这项工作背后的动机是开发技术，将秩参数（类似于代数电路复杂性中使用的）建立命题证明的下限。
2010-08-01 cs.CC
On the existence of strong proof complexity generators
本文研究是否存在对所有命题证明系统都困难的证明复杂性生成器，提出 $\igvee$-困难性概念，证明特定 gadget 生成器为 $\igvee$-最困难，并在电路复杂度假设下证明该猜想对所有可行无限 NP 集合成立。
2023-11-09 cs.CC cs.LO math.LO
Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
我们提出并研究了一个框架，在这个框架中，人们可以提出基于替代的证明长度的下界在证明系统中的量化布尔公式。这个框架中的一个关键概念是证明系统集成，它（本质上）是一个证明系统的序列，对于每个证明系统，可以在多项式层次结构中执行证明检查。我们介绍了一个证明系统合奏称为放松QU-RES的基础上建立的证明系统QU-resolution。我们的主要结果包括一个指数分离的树形和一般版本的放松QU-RES，和一个指数下限放松QU-RES，这些都是类似的经典结果命题证明的复杂性。
2016-02-18 cs.CC
Generating Matrix Identities and Proof Complexity
受证明复杂性的基本下界问题的启发，我们开始研究矩阵恒等式作为强证明系统的硬实例。域$\mathbb{F}$上的$d \times d$矩阵的矩阵恒等式是$\mathbb{F}$上的非交换多项式$f(x_1,\ldots,x_n)$，使得$f$在每个$d \times d$矩阵对其变量的赋值上为零。我们专注于算术证明，这是证明的多项式恒等式运算算术电路和其公理是多项式环公理（这些证明作为一个代数模拟的扩展弗雷格命题证明系统，并在$GF(2)$，他们正式构成一个子系统的扩展弗雷格[HT12]）。我们引入了一个强度递减的证明系统的算术证明，其中$d$第th级是一个健全的和完整的证明系统，证明$d \times d$矩阵恒等式（在一个给定的字段）。对于每一级$d>2$的层次结构中，我们建立了一个证明大小的下界在矩阵单位证明的变量的数量：我们显示了一个家庭的矩阵单位$f_n$与$n$变量的存在，这样的任何证明$f_n=0$需要$Ω(n^{2d})$行的数量。下界参数使用了多项式恒等式代数理论的基本结果以及[Hru 11]中参数的推广。然后，我们开始研究矩阵恒等式作为（完整）算术证明的硬实例。我们提出了两个apturtures，一个关于非交换算术电路的复杂性和其他有关证明的复杂性，根据指数大小的下界算术证明（在算术电路的大小证明的身份）举行。最后，我们讨论了我们的方法，如扩展弗雷格强命题证明系…
2014-09-03 cs.CC
A limitation on the KPT interpolation
该研究证明了Pich和Santhanam提出的KPT定理变体在证明难以区分的NP集不相交的证明系统中存在局限性。
2020-08-11 cs.CC math.LO
Case Study of the Proof of Cook's theorem - Interpretation of A(w)
库克定理通常表示为任何多项式时间可验证的问题都可以归结为SAT问题。Cook定理的证明在于构造一个命题公式A（w）来模拟TM的计算，并且这样的A（w）被称为CNF来表示一个多项式时间可验证的问题w.本文通过一个非常简单的例子研究了A（w），证明了A（w）只是CNF的一个表象，而不是一个真正的逻辑形式。本文的案例研究表明，Cook定理中存在着乞讨问题.
2019-04-30 cs.CC
Resolution Lower Bounds for Refutation Statements
对于任何不可满足的CNF公式，我们给出了一个命题陈述的归结反驳的大小的指数下界，该公式有一个归结反驳。我们描述了三个应用程序。(1)（Atserias，Müller 2019）中的一个开放性问题是，上述陈述的某种自然命题编码是否难以解决。我们给出了一个指数大小的下界。(2)我们展示了反射原理的指数分辨率大小下限，从而改进了（Atserias，Bonet 2004）中的结果。(3)我们提供了CNF的新例子，它以指数方式将Res（2）与Resolution分离（这两个证明系统的指数分离最初在（Segerlind，Buss，Impagliazzo 2004）中得到证明）。
2019-05-29 cs.CC math.LO
