一种关于高效命题推理极限的新方法：基础，算法和近似

Propositional reasoning, and specifically the task of demonstrating unsatisfiability of propositional formulas is among the most important problems in computer science as well as in hardware and software validation, automated reasoning and artificial intelligence. Accordingly, understanding the complexity of this problem is central to computer science, computational complexity and logic. The proposed project is aimed to significantly advance our understanding of the limits of efficient reasoning, emphasizing its interplay with efficient computation. We intend to introduce novel connections between propositional proofs, approximation theory, refutations algorithms, algebraic complexity and pure algebra in order to establish new methods for estimating the efficiency of different frameworks of reasoning, and to strengthen our understanding of the connections between efficient computation and efficient provability. Our suggested approaches are: o Algebraic approaches: Exploring new connections between polynomial identity algebras, matrix algebras, and lower bounds on proofs establishing polynomial identities. We aim at giving a new approach for achieving strong (super-polynomial) lower bounds on arithmetic proofs (this can be seen as a first step for proving propositional proofs lower bounds-the fundamental open problem of proof complexity). oApproaches based on inapproximability results: Exploring new connections between the impossibility of establishing approximation algorithms for certain problems and the impossibility of having short refutations for random 3CNF instances. With the intention to lead to conditional lower bounds on strong proof systems and new lower bounds on random instances for weaker proof systems. o Refutation algorithms for random instances: Exploring new connections between refutation algorithms, the feasible interpolation property and automatizability of propositional proofs, for random instances. oApproximate reasoning approaches: Developing natural frameworks and concepts for understanding different propositional reasonings and proof-generation algorithms under approximations. The project is intended as a basic research project and its senior participants have a proven expertise in the foundations of computer science, computational complexity, propositional proof complexity, logic, combinatorics and artificial intelligence. The PI and his students have already conducted successful preliminary research in most of the above directions. All the senior participants have extensive international collaboration with world-leading scientists, and the proposed project will lead to further international cooperation for both the group's faculty and students. For the group's webpage see: http://iiis.tsinghua.edu.cn/?tzameret/lab/index.html

命题推理，更确切地说，阐明命题公式的不可满足性，是计算机科学、软硬件验证、自动推理以及人工智能领域最重要的问题之一。实际上，充分理解命题推理的复杂性对于计算机科学的各个相关领域都是十分重要的。 本项目旨在增进我们对高效推理极限的理解，并试图挖掘其与高效计算间的新关系。我们希望通过引入命题证明、近似理论、反驳算法、代数复杂性及纯代数的新关联，去建立估算不同推理框架效率的新方法，并加深我们对高效计算和高效证明之间关联的理解。我们特别关注如何在各种证明系统(即推理框架)下,给出命题推理长度下界的证明。 我们计划采用的下列方法： ? 代数方法; ? 基于不可近似性结论; ? 基于随机实例的反驳算法; ? 近似推理的方法。 本项目是一项基础性研究，组员由计算机基础科学、计算复杂性、逻辑学、组合学和人工智能领域的资深专家组成。

命题推理，更确切地说，阐明命题公式的不可满足性，是计算机科学、软硬件验证、自动推理以及人工智能领域最重要的问题之一。充分理解命题推理的复杂性对于计算机科学的各个相关领域都是十分重要的。本项目增进了我们对高效推理极限的理解，并试图挖掘其与高效计算间的新关系。我们通过引入命题证明、近似理论、反驳算法、代数复杂性及纯代数的新关联，去建立估算不同推理框架效率的新方法，并加深我们对高效计算和高效证明之间关联的理解。我们特别关注如何在各种证明系统(即推理框架)下，给出命题推理长度下界的证明。我们计划采用的下列方法：代数方法、基于不可近似性结论、基于随机实例的反驳算法、近似推理的方法，研究并证明了常数深度阈值下电路构成的证明系统中的随机3合取范式的反驳有一个多项式大小的上界（被称为阈值逻辑或者TC0-Frege）；给定一个短反驳的反驳系统P，解决P插值问题的高效算法也能提供一个有cn^1.4个子句的3合取范式的高效确定反驳算法；用新的非交换公式的命题积分的描述方法，将在非可交换IPS中的证明简单的描述为一个单独的可写作非可交换公式的非可交换多项式；证明了矩阵标识的证明系统复杂度存在下界。

内容获取失败，请点击重试