有界深度 Frege 系统的典范对

证明系统 $P$ 的典范对是一对不相交的 NP 集合，其中一个集合是所有可满足 CNF 公式的集合，另一个是具有被某多项式界定的 $P$-证明的 CNF 公式的集合。我们给出了深度为 $d$ 的 Frege 系统之典范对的组合刻画。我们的刻画基于本文引入的、由数 $k$（亦称深度）参数化的某些博弈。我们证明深度 $d$ 的 Frege 系统的典范对多项式等价于对 $(A_{d+2},B_{d+2})$，其中 $A_{d+2}$（相应地，$B_{d+1}$）是深度 $d+1$ 的博弈，其中玩家 I（玩家 II）具有位置必胜策略。尽管该刻画以博弈表述，我们将表明这些组合结构可视为单调布尔电路的推广。特别地，深度 1 博弈本质上就是单调布尔电路。由此我们得到针对 Resolution 的单调可行插值的推广，该性质使人能将证明反驳大小下界之任务归约为单调布尔电路大小下界之证明。然而，对于 $d>1$ 的深度 $d$ 博弈，我们尚无证明其大小下界的方法。