분해 방법

명제 논리의 의미론 수업은 타당성과 충족 가능성이 진리표로 결정 가능하다는 것을 보였는데, 그 비용은 변항이 하나 늘 때마다 두 배가 된다. 그리고 진리표 전체를 훑을 필요가 없는 방법들을 예고했다. 의미론적 귀결과 동치 수업은 모든 귀결을 하나의 충족 불가능성으로 환원했다. $\Gamma \models \varphi$일 필요충분조건은 $\Gamma \cup \{\neg\varphi\}$ 집합이 충족 불가능하다는 것이다. 표준형 수업과 그 알고리즘 수업은 모든 식에 연언형을 주었는데, 그 타당성은 한눈에 보이지만 충족 가능성은 보이지 않는다. 그렇다면, 절들의 연언의 충족 불가능성을 절 자체 위에서 작동하여 판정하는 절차가 빠져 있다. 그 절차가 분해이며, 존 앨런 로빈슨이 1965년에 마틴 데이비스와 힐러리 퍼트넘(1960)의 착상을 바탕으로 제안했다. 그것은 오늘날 수백만 개의 변항을 가진 식의 충족 가능성을 판정하는 프로그램의 핵심이다. 연역 단원의 체계(그 의미론과의 관계는 건전성과 완전성 수업과 콤팩트성 정리 수업이 다룬다)와 달리, 분해는 결론을 연역하지 않는다. 집합을 반박한다. 이 수업은 분해가 그것을 건전하고 완전하게 수행함을 증명한다.

앞선 수업들에서처럼 $p$, $q$, $r$, $s$, $t$는 변항 $v_1$에서 $v_5$까지를 가리킨다. 아래첨자 없는 문자 $v$, 그리고 $w$도 진리값 할당을 가리킨다. $V(\varphi)$ 집합은 $\varphi$의 변항들의 집합이다.

절과 절들의 집합

표준형 수업에서 떠올려 보자. 리터럴은 변항이거나 변항의 부정이며, 리터럴 $\ell$의 반대 리터럴은 $\ell^{*}$으로 쓰고, 같은 변항에 부호가 다른 리터럴이다. 서로 반대인 두 리터럴은 상보 쌍을 이룬다. 리터럴의 부정 보조정리에 따라 $v(\ell^{*}) = 1 - v(\ell)$ 관계가 모든 할당 $v$에 대해 성립한다. 거기서 절은 리터럴들의 선언이었다. 여기서는 값을 바꾸지 않는 순서와 반복은 잊고 집합만 남기는 것이 좋다.

절은 리터럴들의 유한 집합이다. 리터럴이 없는 절은 빈 절이라 하며 $\Box$로 쓴다. 할당 $v$가 절 $C$를 충족한다는 것($v \models C$로 쓴다)은 $C$의 어떤 리터럴이 값 $1$을 가진다($v$에서)는 뜻이다. 그렇지 않으면 $v$가 그것을 반박한다. 리터럴이 하나뿐인 절은 단위 절이라 한다. 한 절의 변항들은 집합 $V(C)$를 이룬다. 절들의 집합 $S$의 변항들은 집합 $V(S)$를 이루며, 이것은 앞의 것들의 합집합이다. 할당이 절들의 집합 $S$를 충족한다는 것($v \models S$)은 그 모든 절을 충족한다는 뜻이다. $S$ 집합은 어떤 할당이 그것을 충족하면 충족 가능하고, 그렇지 않으면 충족 불가능하다. 끝으로, $S$가 절들의 집합이고 $C$가 절일 때, $S \models C$ 관계는 $S$를 충족하는 모든 할당이 $C$를 충족한다는 뜻이다.

정의로부터 두 극단적 경우가 따라 나오며, 이를 확인해 두는 것이 좋다. 빈 절에는 리터럴이 없다. 따라서 그 어떤 리터럴도 $1$의 값을 가지지 않으며, 어떤 할당도 그것을 충족하지 않는다. $\Box$ 절은 충족 불가능하며, 그것을 포함하는 모든 집합도 그렇다. 반면 절들의 빈 집합에는 충족해야 할 절이 없으며, 모든 할당이 그것을 충족한다. 둘을 혼동해서는 안 된다. $\{\Box\}$ 집합은 충족 불가능하고, $\emptyset$ 집합은 모든 할당에 의해 충족된다.

상보 쌍을 포함하는 절은 항진인 절이라 한다. 그것은 아무 조건도 부과하지 않으며, 어떤 집합에서든 그 모형을 바꾸지 않고 제거할 수 있다. 절을 집합으로 쓰는 것은 표기상의 변덕이 아니다. $(p \vee q)$ 절과 $(p \vee \neg q)$ 절로부터 $p$ 절을 얻고자 하면, 선언은 $(p \vee p)$ 식을 주는데, 이것은 $p$ 식과 동치이지만 같은 식이 아니다. 집합으로는 $\{p\} \cup \{p\} = \{p\}$ 등식이 성립하며, 반복된 리터럴의 융합은 저절로 일어난다.