相对化命题演算
Relativized Propositional Calculus
摘要：
定义并比较了相对化命题演算的证明系统。
英文摘要：
Proof systems for the Relativized Propositional Calculus are defined and compared.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
相关论文
关于P与NP的思考
Considerations on P vs NP
为了证明问题的P不同于NP类，我们考虑了命题演算公式的可满足性问题，这是一个NP完全问题。证明了对每个搜索算法A，存在一个包含命题演算公式的集合E（A），每个命题演算公式都要求算法A用非多项式时间找到满足它的命题字母的真值，并且E（A）的大小是n的指数函数，这使得在多项式时间内检测这些公式是不可能的.因此，可满足性问题不具有多项式复杂度
cs.CCcs.LO
将命题证明刻画为非交换公式
Characterizing Propositional Proofs as Non-Commutative Formulas
每个布尔重言式都有一个简短的命题演算证明吗？这里，命题演算（即弗雷格）证明是从一组公理开始并使用一组固定的合理推导规则推导新的布尔公式的证明。在弗雷格证明上建立任何超多项式大小的下限（就证明公式的大小而言）是证明复杂性中的一个主要开放问题，也是复杂性理论中少数基本困难问题之一。另一方面，非交换算术公式构成了一个相当弱的计算模型，早在1991年，Nisan [Nis 91]就已经证明了它的指数大小下界，他使用了一个特别透明的论点。在这项工作中，我们表明，弗雷格下界实际上遵循相应的大小下界的非交换公式计算某些多项式（和这种下界的非交换公式必须存在，除非NP=coNP）。更确切地说，我们证明了重言式$T$与非交换多项式$p$之间的自然关联，使得：如果$T$具有多项式大小的弗雷格证明，则$p$具有多项式大小的非交换算术公式;相反，当$T$是DNF时，如果$GF(2)$具有多项式大小的非交换算术公式，则$T$具有准多项式大小的弗雷格证明。
cs.CCmath.LO
非交换公式的代数证明
Algebraic Proofs over Noncommutative Formulas
我们研究了代数命题证明系统与非交换公式操作的可能配方。我们观察到，一个简单的公式产生了至少像弗雷格一样强大的系统-产生了一种语义方式来定义一个Cook-Reckhow（即，多项式验证）代数模拟弗雷格证明，不同于[BIKPRS 96，GH 03]。然后，我们转向一个明显较弱的系统，即多项式演算（PC），其中多项式被写为有序公式（PC over ordered formulas，简称）：有序多项式是一个非交换多项式，其中每个单项式中的乘积的顺序都是变量的固定线性顺序;如果由每个子公式计算的多项式是有序的，则代数公式是有序的。我们表明，PC有序公式是严格强于决议，多项式演算和多项式演算与决议（PCR），并承认多项式大小反驳鸽子洞原则和Tseitin的公式。最后，我们提出了一种方法，建立下界PC上的顺序公式证明，和相关的系统，根据非交换公式的下界的性质。这项工作背后的动机是开发技术，将秩参数（类似于代数电路复杂性中使用的）建立命题证明的下限。
cs.CC
有限模型理论与证明复杂性的再认识：无选择多项式时间中的图的区分与扩展多项式演算
Finite Model Theory and Proof Complexity revisited: Distinguishing graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus
本文扩展了以前的工作，从有限模型理论和命题/代数证明系统的逻辑之间的连接。我们表明，如果所有的非同构图在一个给定的图类中可以区分在逻辑无选择多项式时间计数（CPT），那么他们也可以区分在有界度扩展多项式演算（EPC），和反驳有大致相同的大小的CPT-语句的资源消耗。这使得转移EPC的CPT的下限，从而构成了一个新的潜在的方法，更好地了解CPT的限制。图同构问题的PTIME实例的超多项式EPC下界将CPT与PTIME分离，从而解决有限模型理论中的一个主要公开问题。进一步，利用我们的结果，我们提供了一个模型理论证明有界次数多项式演算和有界次数扩展多项式演算的分离。
cs.CCcs.LO
近距离观察一些最近的证明压缩相关的索赔
A Closer Look at Some Recent Proof Compression-Related Claims
Gordeev和Haeusler [GH 19]认为，极小命题逻辑的每个重言式$ρ$都可以用$|ρ|$中的大小多项式的自然演绎来证明.这建立在Hudelmaier [Hud93]的工作之上，该工作为直觉主义命题逻辑找到了类似的结果，但对于该结果，只有证明的高度是多项式有界的，而不是整体大小。他们通过将Hudelmaier的微积分中的证明转换为Prawitz的自然演绎系统中的等价树型证明，然后将树型证明压缩为等价的DAG型证明，使得高度和基础上的多项式约束意味着整体大小上的多项式约束。然而，我们的论文观察到，这种构造只在最小蕴涵逻辑上进行，我们证明它比他们声称结果的最小命题逻辑弱（见4.2节）。简单地扩展用于覆盖最小命题逻辑的逻辑系统不足以恢复论文的结果，因为它会完全破坏对证明主要结果至关重要的一些定理的证明。在很大程度上依赖于他们的上述工作，Gordeev和Haeusler [GH 20]声称建立NP=PSPACE。论证集中依赖于最小命题逻辑中证明大小的多项式界。由于我们证明了这个界限并没有被他们正确地建立起来，他们所谓的证明并没有正确地建立NP=PSPACE。
cs.CCcs.LO
迈向 QBF 中的统一认证
Towards Uniform Certification in QBF
本文提出一种新技术，将策略提取与局部论证相结合，证明扩展 QBF Frege 可 p-模拟多种子句证明系统，从而支持 QBF 求解中的统一认证。
cs.CCcs.LO
更多相关论文收起更多论文
基于原子流和阈值公式的深度推理中的拟多项式规范化
Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
Jeanábek表明，在深度推理中，经典命题逻辑证明中的切割可以在准多项式时间内消除。证明是间接的，它依赖于Atserias，Galesi和Pudlák关于单调微积分的结果以及该系统与无割深度推理证明之间的对应关系。本文给出了Jeábek结果的一个直接证明：给出了经典命题逻辑在深度推理中的一个拟多项式时间截消过程。主要的新成分是使用了一种称为原子流的深层推理证明的计算跟踪，它既非常简单（它们只跟踪结构规则，而忘记了逻辑规则），又足够强大，可以忠实地表示切消过程。
cs.CCcs.LO
