Development of Grapy Theoretical Analysis for Proof Complexity

NP对coNP问题是理论计算机科学中的一个基本开放问题。研究证明复杂性是解决这一问题的主要途径。在以往的工作中，已经做了很多的研究，证明系统的布尔函数，但我们研究的证明复杂性，通过图演算，主要是Hajos演算。得到了证明系统的复杂性与图演算的复杂性之间的关系。此外，我们可以实现一个枚举算法生成非3-着色图。该算法模拟了平面图Hajos演算的一部分。

NP versus coNP problem is one of the fundamental open problems intheoretical computer science. To study proof complexity is the main approach to resolve this problem. In previous works, many researches have been done on proof systems for Boolean functions, but we studied proof complexity via graph calculus, mainly Hajos Calculus. We obtained the relationship between the complexity of proof systems and that of graph calculus. Moreover, we can implement an enumeration algorithm generating non-3-colorable graphs. This algorithm simulates a part of Hajos Calculus for planar graphs.