标题： 证明复杂性和可行插值 显示英文标题

标题： Proof Complexity and Feasible Interpolation

摘要： 这是一篇关于命题证明复杂性的调查，旨在介绍该领域的基础知识，特别关注一种称为可行插值的方法。 这种方法用于为经典逻辑和非经典逻辑的多个证明系统构造“难以证明的定理”。 在这里，“难以证明的定理”指的是逻辑中的一个定理，其最短证明的长度相对于定理本身的长度呈超多项式增长。 为了使这篇调查更易于理解，我们仅假设对命题逻辑、模态逻辑和一阶逻辑有基本的了解，以及对计算复杂性领域中的关键概念（如类$\mathbf{NP}$和$\mathbf{PSPACE}$的定义）有基本的理解。 任何额外的概念将在需要时引入和解释。 显示英文摘要

摘要： This is a survey on propositional proof complexity aimed at introducing the basics of the field with a particular focus on a method known as feasible interpolation. This method is used to construct "hard theorems" for several proof systems for both classical and non-classical logics. Here, a "hard theorem" refers to a theorem in the logic whose shortest proofs are super-polynomially long in the length of the theorem itself. To make this survey more accessible, we only assume a basic familiarity with propositional, modal, and first-order logic, as well as a basic understanding of the key concepts in computational complexity, such as the definitions of the classes $\mathbf{NP}$ and $\mathbf{PSPACE}$. Any additional concepts will be introduced and explained as needed.