离散Jordan曲线定理证明的复杂性
The Complexity of Proving the Discrete Jordan Curve Theorem
摘要：
约当曲线定理（Jordan Curve Theorem，JCT）指出，一条简单的闭合曲线将平面分成两个连通的区域。我们形式化和证明定理的背景下，网格图，在不同的输入设置，在理论界的算术，对应于小的复杂性类。理论$V^0(2)$（对应于$AC^0(2)$）证明了任何一组形成不相交环的边将网格划分为至少两个区域。理论$V^0$（对应于$AC^0$）证明了形成简单闭合曲线的任何边序列将网格划分为两个区域。因此，Hex重言式和st-连通重言式具有多项式大小的$AC^0(2)$ -Frege证明，这改进了仅适用于更强证明系统$TC^0$ -Frege的Buss的结果。
英文摘要：
The Jordan Curve Theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded arithmetic that correspond to small complexity classes. The theory $V^0(2)$ (corresponding to $AC^0(2)$) proves that any set of edges that form disjoint cycles divides the grid into at least two regions. The theory $V^0$ (corresponding to $AC^0$) proves that any sequence of edges that form a simple closed curve divides the grid into exactly two regions. As a consequence, the Hex tautologies and the st-connectivity tautologies have polynomial size $AC^0(2)$-Frege-proofs, which improves results of Buss which only apply to the stronger proof system $TC^0$-Frege.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
