분해 증명(resolution)

(A ∨ x) 와 (B ∨ ¬x) 에서 (A ∨ B) 를 끌어내는 규칙 하나만 쓰는 증명 체계다(도출이라고도 옮긴다). 논리식의 절들에서 출발해 빈 절(모순)을 끌어내면 그 식이 충족 불가능함이 증명된다. 하켄은 1985년에 「비둘기 n+1 마리를 집 n 개에 한 마리씩 넣을 수 없다」는 비둘기집 원리를 이 체계로 증명하려면 지수 길이가 필요함을 보였다. 오늘날의 SAT 풀이 프로그램이 충족 불가능 판정을 내리는 과정은 resolution 증명으로 옮길 수 있으므로, 이 하한은 그런 프로그램의 한계이기도 하다.