증명 복잡도

명제 논리의 항진식을 정해진 증명 체계 안에서 증명할 때 필요한 가장 짧은 증명의 길이를 연구한다. 쿡과 레코(Reckhow)는 1979년에, 모든 항진식에 다항 길이의 증명을 주는 증명 체계가 있는 것과 NP = coNP 가 같은 말임을 보였다. 따라서 점점 더 강한 증명 체계마다 「짧은 증명이 없는 항진식」을 찾아 나가면 NP ≠ coNP, 나아가 P ≠ NP 에 다가갈 수 있다. resolution 같은 약한 체계에서는 지수 하한이 증명되었지만, 교과서에 나오는 보통의 명제 논리 체계(프레게 체계)에 대해서는 아직 초다항 하한이 없다.