younghwanjoo1608

ㅎㅇ

11 minute read


Resolution이란 최소한의 규칙을 갖는 formal proof system. 규칙 중 하나는 Cut rule. 이 규칙은 $(F \rightarrow G)$와 $(G \rightarrow H)$으로부터 $(F \rightarrow H)$를 추론(deduce)할 수 있다고 말한다.

나머지 하나는 Substitution rule의 변형 : $H$가 $F$를 subformula로 갖는 formula라고 하자. $G \equiv F$이면, $H$로부터 $H’$를 추론할 수 있다. 이때 $H’$는 $H$ 내에서 등장하는 $F$를 $G$로 치환해 얻은 formula이다.1


이외에도 많은 규칙들이 있는데, 더 적은 수의 규칙을 얻기 위해 약간 cheating을 하자. $F$와 $G$가 동치인 formula이면, $F$로부터 $G$를 추론할 수 있다. 이로부터 우리의 목표 중 하나, Equivalence problem을 해치울 수 있을 것 같다.

그런데 Substitution rule은 약간 완화시킬 여지가 있는 것 같다. 이 rule의 주 목적은 formula를 CNF로 만드는 것. Resolution에서 가장 중요한 부분은 formula가 CNF에 속하게 되면 추론에 단지 2개의 규칙만이 필요하게 된다는 점이다. 이것이 이전 Sec.의 Equivalence problem을 비롯한 다른 decision problem들의 알고리즘을 제공한다.2


Clauses

$F$가 CNF라고 하자. 그러면 $F$는 literal들의 disjuction들의 conjunction. 우리는 literal들의 disjunction을 clause(절)이라고 부른다. 편의 상 각 clause를 set으로써 나타내자. 즉,

\[ L_{1} \vee L_{2} \vee \dots \vee L_{n} \textrm{ as the set } \{ L_{1} , L_{2} , \dots , L_{n}\} \]

Literal들의 disjunction 형태를 한 formula는 이러한 set으로써 유일하게 결정된다. 그러나, 이 set이 하나의 formula를 유일하게 결정하지는 않는데, $(L_{1} \vee L_{2})$, $(L_{2} \vee L_{1})$, $(L_{1} \vee L_{2} \vee L_{2})$가 모두 하나의 set $\{ L_{1} , L_{2} \}$로 나타내어지기 때문이다. 따라서 이들 formula는 동일(identical)하지는 않으나, 동치(equivalent)이다.


Proposition 1.8.1

$C$, $D$가 clause라고 하자. $C$와 $D$가 set의 관점에서 같다면, $C \equiv D$이다.


Proof.


$C$에서 나타나는 모든 literal의 set을 $\mathcal{S}$라고 하면, $C$와 $D$는 둘 다 $\mathcal{S}$의 literal들의 disjuction으로써 동치이다. $\square$

$F$가 CNF formula이면, $F$는 clause들의 conjunction이고, $F$를 set of sets로 나타낼 수 있다. $F$에 등장하는 (set으로써 표현된) clause들을 $C_{i}$라고 하면, $F$를 set $ \{ C_{1}, \dots , C_{n} \} $로 간주할 수 있다. 예를 들어, formula $(A \vee B \vee \neg C) \wedge (C \vee D) \wedge \neg A \wedge ( \neg B \vee \neg D)$는 4개 clause들의 set $ \{ \{A, B, \neg C \}, \{C, D \}, \{ \neg A \}, \{ \neg B, \neg D \} \}$로 간주된다.


Proposition 1.8.2

$F$와 $G$를 CNF formula라고 하자. $F$와 $G$가 set의 관점에서 같다면, $F \equiv G$이다.


Proof.


Prop. 1.8.1과 같은 논리. $\square$


이 Sec. 전체에서, CNF formula들을 formula 그 자체와 clause들의 set 양쪽으로 간주한다. 이제 $F$와 $G$가 CNF formula일 때, $F \wedge G$를 $F \cup G$로 쓸 수 있게 되었다.

그러나, 이는 어디까지나 CNF에 대해서만. Disjunction이나 negation에 대해서는 마땅히 좋은 (set theoretical) 대상이 존재하지 않는다. $F \vee G$나 $\neg F$는 CNF에 속하지 않으므로, clause들의 set으로 볼 수 없다.


***

Resolvent

주어진 CNF formula에서, resolution은 formula가 satisfiable은지 아닌지 결정하기 위해 두 규칙을 반복해서 사용한다. 그 중 하나는 $F$의 임의의 clause가 $F$로부터 추론된다는 것. 나머지 하나는 두 clause들의 resolvent와 관련이 있다.


Definition 1.8.3

$C_{1}$, $C_{2}$가 clause라 하자. 어떤 atomic formula $A$에 대해 $A \in C_{1}$, $\neg A \in C_{2}$라고 가정하자. 그러면 clause $ R = (C_{1} - \{ A \} ) \cup (C_{2} - \{ \neg A \} ) $를 $C_{1}$과 $C_{2}$의 resolvent라고 한다.

이 상황을 도식적으로 다음과 같이 나타낼 수 있다. :

\[ C_{1} \qquad \qquad C_{2} \]

\[ \diagdown \qquad \diagup \]

\[ R \]


Example 1.8.4

$C_{1} = \{ A_{1}, \neg A_{2}, A_{3} \} $
$C_{2} = \{ A_{2}, \neg A_{3}, A_{4} \} $라고 하자.

$A_{3} \in C_{1}$이고, $\neg A_{3} \in C_{2}$이므로 $C_{1}$과 $C_{2}$의 resolvent는

\[ \{ A_{1}, \neg A_{2}, A_{3} \} \qquad \qquad \qquad \qquad \qquad \{ A_{2}, \neg A_{3}, A_{4} \} \]

\[ \diagdown \qquad \qquad \qquad \qquad \diagup \]

\[ \{ A_{1},\neg A_{2}, A_{2}, A_{4} \} \]

이다.


Example 1.8.5

두 clause의 resolvent가 유일할 필요는 없다. Ex. 1.8.4에서 $A_{3}$ 대신 $A_{2}$를 생각하면, $\neg A_{2} \in C_{1}$이고, $A_{2} \in C_{2}$이므로 $C_{1}$과 $C_{2}$의 resolvent는

\[ \{ A_{1}, \neg A_{2}, A_{3} \} \qquad \qquad \qquad \qquad \qquad \{ A_{2}, \neg A_{3}, A_{4} \} \]

\[ \diagdown \qquad \qquad \qquad \qquad \diagup \]

\[ \{ A_{1}, A_{3}, \neg A_{3}, A_{4} \} \]

이다.


다음은 resolution에 사용되는 세 추론 규칙이다.

  • $G$를 임의의 formula, $F$를 $G$에 CNF algorithm을 적용해서 얻은 CNF formula라고 하자. 그러면 $F$는 $G$로부터 추론될 수 있다.
  • $F$를 CNF formula라고 하자. $F$의 임의의 clause는 $F$로부터 추론될 수 있다.
  • $F$를 CNF formula라고 하자. $F$의 두 clause의 임의의 solvent는 $F$로부터 추론될 수 있다.


놀랍게도 propositional logic에는 이 세 규칙만으로 충분. 즉 resolution은 complete(완전)하다. 이를 보이기에 앞서 위 규칙들이 sound한지 확인하자. 첫 번째 규칙은 Prop. 1.6.9에 의해 성립. 두 번째 규칙은 $\wedge - \textrm{Sym.}$와 $\wedge - \textrm{Elim.}$에 의해 성립.


마지막 규칙만 남았다. $C_{1}$, $C_{2}$가 Ex. 1.8.4와 같다고 해 보자. 그러면 $C_{1}$는 $(\neg A_{1} \wedge A_{2}) \rightarrow A_{3}$와, $C_{2}$는 $ A_{3} \rightarrow (A_{2} \vee A_{4})$와 동치. 그러면 cut rule에 의해 이들로부터 $( \neg A_{1} \wedge A_{2}) \rightarrow (A_{2} \vee A_{4} )$가 도출되고, 이는 Ex. 1.8.4에서 얻은 resolvent와 같다. Formal proof로 나타내면,


Proposition 1.8.6

$C_{1}$, $C_{2}$를 clause,
$R$를 $C_{1}$과 $C_{2}$의 resolvent라고 하자.

그러면, $\{ C_{1}, C_{2} \} \vdash R$.


Proof.


$C_{1}$, $C_{2}$가 resolvent를 가지므로, 어떤 atomic formula $A$가 존재하여 한쪽에는 $A$가, 다른 한쪽에는 $\neg A$가 들어 있다. WLOG, $ A \subset C_{1} $, $ \neg A \subset C_{2} $라고 하자. 그러면 어떤 formula $F$, $G$에 대해 $C_{1} \equiv (A \vee F)$, $C_{2} \equiv (\neg A \vee G) $이다. formula $(F \vee G)$는 $C_{1}$, $C_{2}$의 resolvent. 이를 $R$로 둘 수 있다.

이제 $\{ C_{1}, C_{2} \} \vdash R$의 formal proof.

$\qquad\textrm{Premise : }\mathcal{F} \vdash (A \vee F), \mathcal{F} \vdash (\neg A \vee G)$

$\qquad\textrm{Conclusion : }\mathcal{F} \vdash (F \vee G)$

Statement Justification
1. $\mathcal{F} \vdash (A \vee F)$ $\textrm{Premise}$
2. $\mathcal{F} \cup \{ \neg A \} \vdash (A \vee F)$ $\textrm{Monotonicity}$ applied to 1
3. $\mathcal{F} \cup \{ \neg A \} \vdash \neg A$ $\textrm{Assumption}$
4. $\mathcal{F} \cup \{ \neg A \} \vdash F$ $\vee- \textrm{Elimination}$ applied to 2 and 3
5. $\mathcal{F} \cup \{ \neg A \} \vdash (F \vee G)$ $\vee- \textrm{Introduction}$ applied to 4
6. $\mathcal{F} \vdash (\neg A \vee G)$ $\textrm{Premise}$
7. $\mathcal{F} \cup \{ \neg \neg A \} \vdash (\neg A \vee G)$ $\textrm{Monotonicity}$ applied to 6
8. $\mathcal{F} \cup \{ \neg \neg A \} \vdash \neg \neg A$ $\textrm{Assumption}$
9. $\mathcal{F} \cup \{ \neg \neg A \} \vdash G$ $\vee- \textrm{Elimination}$ applied to 7 and 8
10. $\mathcal{F} \cup \{ \neg \neg A \} \vdash (G \vee F)$ $\vee- \textrm{Introduction}$ applied to 9
11. $\mathcal{F} \cup \{ \neg \neg A \} \vdash (F \vee G)$ $\vee- \textrm{Symmetry}$ applied to 10
12. $\mathcal{F} \vdash (F \vee G)$ $\textrm{Proof by Cases}$ applied to 5 and 11

$\square$

따라서, resolution으로 증명될 수 있는 모든 것들은 formal proof가 주어진다. 이제 Thm. 1.4.9에 의해 resolution은 sound. 특히 $R$이 CNF formula $F$의 두 clause에 대한 resolvent이면, $R$는 $F$의 consequence이다. 표면적으로는 resolution은 우리 formal proof system의 한 부분이지만, 지금부터 resolution이 formal proof만큼이나 강력함을 보일 것이다.


***

Completeness of Resolution

Resolution이 주어진 formula가 statisfiable인지 아닌지를 알아낼 수 있음을 보인다. 일단 그 formula가 CNF에 있다고 가정할 수 있다. 임의의 CNF formula $F$가 주어졌을 때,

$Res^{0} (F) = \{ C | C \textrm{ is a clause of } F \} $

라고 하자. 즉 이는 $F$의 모든 clause들의 set이다. 이제 각 $n>0$에 대해,

$Res^{n} (F) = Res^{n-1} (F) \cup \{ R | R \textrm{ is a resolvent of two clauses of } Res^{n-1} (F) \} $

라고 하자.

$Res^{0} (F) =F$는 finite set이므로, $F$로부터 resolvent를 사용해 유도할 수 있는 clause들은 유한하다. 그러면 언젠가는 $Res^{m} (F) = Res^{m+1} (F)$를 만족하는 $m$을 찾을 수 있게 된다.3 이제 그러한 $Res^{m} (F)$를 $Res^{\ast} (F)$라고 나타내자. 이는 $F$로부터 resolvent를 사용해 유도될 수 있는 모든 clause들의 set이다. Formula의 관점에서 보면, $Res^{\ast} (F)$는 resolvent를 사용해 유도되는 $F$의 모든 consequence들의 conjunction.


Proposition 1.8.7

$F$가 CNF formula라고 하자.
$\varnothing \in Res^{\ast} (F)$이면, $F$는 unsatisfiable이다.


Proof.


만약 $\varnothing \in Res^{\ast} (F)$이면, 어떤 $n$에 대해 $\varnothing \in Res^{n} (F)$이다.

$\varnothing$은 clause가 아니므로, $\varnothing \notin Res^{0} (F)$. 따라서 어떤 $m$에 대해 $\varnothing \notin Res^{m} (F)$이고 $\varnothing \in Res^{m+1} (F)$이다. 이때 $\varnothing$은 $Res^{m+1} (F)$의 두 clause의 resolvent. 그런데 $\varnothing$은 오로지 atomic $A$에 대해 $\{ A \}$와 $\{ \neg A \}$의 resolvent로써만 얻을 수 있다. $\{ A \}$와 $\{ \neg A \}$는 둘 다 $Res^{m} (F)$에 들어 있다.

Prop. 1.8.6에 의해 $A$와 $\neg A$는 $F$의 consequence이다. 이로부터 $A \wedge \neg A$가 $F$의 consequence이고, $F$는 unsatisfiable. $\square$


Example 1.8.8

Formula $F$가
\[ \{ A, B, \neg C \}, \{\neg A\}, \{ A, B, C \}, \{ A, \neg B \} \} \]
라고 하자. $F$가 unsatisfiable임을 resolution으로부터 보이고자 한다.

$F$의 clause들을 순서대로 $C_{1}, C_{2}, C_{3}, C_{4}$라고 쓰자. 그러면

\[ C_{1} \qquad \qquad \qquad \qquad C_{3} \qquad \qquad \qquad \]

\[ \qquad \diagdown \qquad \qquad \diagup \qquad \qquad \qquad \]

\[ \qquad \qquad \{A, B \} \qquad \qquad \qquad C_{4} \]

\[ \qquad \qquad \qquad \qquad \diagdown \qquad \qquad \diagup \qquad \]

\[ C_{2} \qquad \qquad \qquad \qquad \{ A \} \qquad \qquad \qquad \]

\[ \qquad \diagdown \qquad \qquad \diagup \qquad \qquad \qquad \]

\[\qquad \varnothing \qquad \qquad \qquad\]

이로부터 $\{A, B \} \in Res (F)$, $\{A \} \in Res^{2} (F)$, $\varnothing \in Res^{3} (F)$임을 알 수 있다. Prop.1.8.7에 의하여 $F$는 unsatisfiable.


이를 two-column proof로 나타내면 다음과 같다.

Consequence of $F$ Justification
$C_{1}$ Clause of $F$
$C_{3}$ Clause of $F$
$\{A, B \}$ Resolvent of $C_{1}$ and $C_{3}$
$C_{4}$ Clause of $F$
$\{A \}$ Resolvent of $\{A, B \}$ and $C_{4}$
$C_{2}$ Clause of $F$
$\varnothing$ Resolvent of $\{A \}$ and $C_{2}$


이제 Prop. 1.8.7의 역을 생각하자. $F$가 CNF formula라고 하자. $F$가 unsatisfiable이면, $\varnothing \in Res^{\ast} (F)$인가? 답은 Yes. Unsatisfiablity를 보이기 위해선 resolution만 있으면 된다!

위 Ex.1.8.8에서 보았듯이, 증명의 “Justification” column에는 단 2개의 option만이 존재한다. Clause가 주어져 있거나, 혹은 이미 이전에 유도된 두 clause의 resolvent이거나.


Proposition 1.8.9

$F$가 CNF formula라고 하자.
$F$는 unsatisfiable이면, $\varnothing \in Res^{\ast} (F)$이다.


Proof.


$F= \{C_{1}, \dots C_{k} \}$라고 하자. 각 $C_{i}$에는 tautology가 없다고 가정한다. (만일 tautology가 존재하는 clause가 있다면, 그 녀석만 내다 버리고 나머지로부터 $\varnothing$을 도출해내면 된다).

Induction을 사용. $F$에 등장하는 atomic formula의 수를 $n$이라 하자.


[Base Step] $n=1$이라고 하자. $F$에는 오직 하나의 atomic formula $A$만이 나타난다. 그러면 $F$의 clause는 세 가지 가능성이 존재. 각 $C_{i}$는 $\{ A\}, \{\neg A\}$ 또는 $\{ A, \neg A\}$. 마지막은 tautology이므로 가정에 의해 $F$의 clause가 아니다. 따라서 $F$에 존재하는 clause는 $\{ A\}$와 $ \{\neg A\}$뿐.

따라서 세 가지 가능성이 있는데, $F=\{ \{A\}\}$, $F=\{ \{\neg A\}\}$ 또는 $F=\{ \{A\}, \{\neg A\}\}$. 첫 두 경우는 satisfiable이므로, $F$는 $\{ \{A\}, \{\neg A\}\}$여야만 한다. 명백히 $\varnothing \in Res^{\ast} (F)$.


[Induction Step] 이제 $F$가 atomic subformula $A_{1}, \dots A_{n+1}$를 갖는다고 하자. $A_{1}, \dots A_{n}$만이 사용된 임의의 unsatisfiable formula $G$에 대해 $\varnothing \in Res^{\ast} (G)$라고 가정하자. 다음 formula를 정의한다.

$\tilde{F_{0}}=$ $\neg A_{n+1}$을 포함하지 않는 $F$의 모든 clause $C_{i}$의 conjunction,
$\tilde{F_{1}}=$ $A_{n+1}$을 포함하지 않는 $F$의 모든 clause $C_{i}$의 conjunction.

이들은 CNF formula. Set의 관점에서 보면

\[ \tilde{F_{0}} \cup \tilde{F_{1}} =F\]


실제로 $F$의 clause $C_{i}$가 $\tilde{F_{0}} \cup \tilde{F_{1}} $에 속하지 않는다면 $C_{i}$는 $A_{n+1}$과 $\neg A_{n+1}$을 동시에 포함하고, $C_{i}$는 tautology가 되어 가정에 반하게 된다. 따라서 $ \tilde{F_{0}} \cup \tilde{F_{1}} $와 $F$는 같은 clause를 포함한다.

$F_{0} = \{ C_{i} - \{A\_{n+1} \} | C_{i} \in \tilde{F_{0}} \}$,
$F_{1} = \{ C_{i} - \{\neg A\_{n+1} \} | C_{i} \in \tilde{F_{1}} \}$

라고 하자.

즉 $F_{0}$는 $\tilde{F_{0}}$의 각 clause에서 $A_{n+1}$를 떼 내서 만들어지며, $F_{1}$은 $\tilde{F_{1}}$의 각 clause에서 $\neg A_{n+1}$를 떼 내서 만들어진다.4

$A_{n+1}$는 $0$ 또는 $1$의 진릿값을 가지므로, $F \equiv F_{0} \vee F_{1}$이다. $F$가 unsatisfiable이므로, $F_{0}$와 $F_{1}$은 각각 unsatisfiable이다. Formula $F_{0}$와 $F_{1}$은 atomic formula $A_{1}, \dots A_{n}$만이 사용되었다. Induction hypothesis에 의해, $\varnothing \in Res^{\ast} (F_{0})$, $\varnothing \in Res^{\ast} (F_{1})$이다.

$F_{0}$으로부터 $\varnothing$을 유도할 수 있으므로, $\tilde{F_{0}}$로부터 $\varnothing$ 또는 $A_{n+1}$ 중 하나를 유도할 수 있다.5 마찬가지로 $\tilde{F_{1}}$로부터 $\varnothing$ 또는 $\neg A_{n+1}$ 중 하나를 유도할 수 있다. 만약 $\tilde{F_{0}}$로부터 $A_{n+1}$을, $\tilde{F_{1}}$로부터 $\neg A_{n+1}$를 유도할 수 있으면, $\varnothing$을 $\tilde{F_{0}} \cup \tilde{F_{1}} $로부터 유도할 수 있다. $F=\tilde{F_{0}} \cup \tilde{F_{1}} $이므로, $\varnothing \in Res^{\ast} (F)$를 얻는다. $\square$


Example 1.8.10

$n=2$라고 하자. 그러면 $A_{n+1}$는 $A_{3}$.

$F= \{ \{A_1, A_3 \}, \{A_2\}, \{\neg A_1, \neg A_2, A_3 \}, \{\neg A_2, \neg A_3 \} \}$라고 하자. 그러면,

$\tilde{F_0}= \{ \{A_1, A_3 \}, \{A_2\}, \{\neg A_1, \neg A_2, A_3 \} \}$
$\tilde{F_1}= \{ \{A_2\}, \{\neg A_2, \neg A_3 \} \}$

따라서,

$F_0= \{ \{A_1 \}, \{A_2\}, \{\neg A_1, \neg A_2 \} \}$
$F_1= \{ \{A_2\}, \{\neg A_2\} \}$

이제 $F$는

$\tilde{F_{0}} \cup \tilde{F_{1}} = (A_1 \vee A_3) \wedge (A_2) \wedge (\neg A_1 \vee \neg A_2 \vee A_3) \wedge (\neg A_2 \vee \neg A_3) $


만일 우리가 $A_3$의 진릿값을 $0$으로 알고 있다면, 이는

$(A_1 \vee 0) \wedge (A_2) \wedge (\neg A_1 \vee \neg A_2 \vee 0) \wedge (1)$이고, 이는 $F_{0}$과 동치.

반면에 $A_3$의 진릿값을 $0$으로 알고 있다면,

$(1) \wedge (A_2) \wedge (1) \wedge (\neg A_2 \vee 0)$이고, 이는 $F_{1}$과 동치.


이것이 Satisfiability problem의 알고리즘을 제공한다. 임의의 formula $G$에 대해, CNF algorithm으로 $G$와 동치인 CNF formula $F$를 찾을 수 있다. Finite set $Res^{\ast} (F)$를 계산한다. 만약 $\varnothing \in Res^{\ast} (F)$이면 알고리즘은

\[G \textrm{ is not satisfiable.} \]

이라고 결론짓고, 그렇지 않으면

\[G \textrm{ is satisfiable.} \]

이라고 결론을 내린다. Prop. 1.8.7과 Prop. 1.8.9에 의해 이 알고리즘은 잘 작동한다.


그러나 이 알고리즘은 필연적으로 빠르지 않은데, 이 decision problem의 polynomial-time 알고리즘이 아직 알려지지 않았기 때문. 그러나 어떤 경우에서는 이 알고리즘이 빠른 결론에 도달하도록 만들어주기도 한다. $F$가 unsatisfiable이면 우리는 $Res^{\ast} (F)$를 모조리 계산할 필요가 없다. $\varnothing$이 빨리 등장할수록 그것이 satisfiable이 아니라는 걸 바로 알 수 있으니까. 그러나 $F$가 satisfiable이면, 차라리 진리표가 더 빠르다. 진릿값이 $1$이 나올 때까지 찾으면 되니까.

자, 이제 이번 Sec.의 메인 결과. 다음 정리는 Completeness theorem for propositional logic의 finite version.


Theorem 1.8.11

$F, G$가 propositional logic의 formula,
$H$가 formula $F \wedge \neg G$에 CNF algorithm을 적용하여 얻은 CNF formula라고 하자.

TFAE:

  1. $F \models G$
  2. $\{ F \} \vdash G$
  3. $\varnothing \in Res^{\ast} (H)$


Proof.


[(2) $\Rightarrow$ (1)] Thm. 1.4.9.

[(1) $\Rightarrow$ (3)] Prop. 1.8.9.

[(3) $\Rightarrow$ (2)] Prop. 1.6.9에 의해 $\{F \wedge \neg G \} \vdash H $이다. $\wedge - \textrm{Intro.}$에 따르면 $\{F, \neg G \} \vdash F \wedge \neg G $이고, 이로부터 $\{F, \neg G \} \vdash H$를 얻는다.

$\varnothing \in Res^{\ast} (H)$이므로, atomic formula $A$가 존재하여 $\{ A \}$와 $\{ \neg A \}$ 둘 다 $Res^{\ast} (H)$ 안에 있어야 한다. [Prop. 1.8.6]((#proposition-186)에 의해 $\{ H\} \vdash A, \{ H\} \vdash \neg A $이다. 따라서 $\{F, \neg G \} \vdash A$와 $\{F, \neg G \} \vdash \neg A$가 모두 성립. Proof by contradiction에 의해, $\{ F \} \vdash \neg \neg G$를 얻는다. 마지막으로 double negation에 의해 $\{F \} \vdash G$. $\square$


  1. 즉, [Thm. 1.5.4](http://younghwanjoo1608.github.io/logics/prl1.5/#theorem-154)를 추론 규칙으로 간주하겠다는 것. ↩

  2. 또한, propositional logic의 [Completeness Theorem](https://younghwanjoo16081608.tistory.com/35#1.9.4) 증명에 한 발짝 다가갈 수 있게 해 준다. ↩

  3. 더 이상 resolvent를 얻을 수 없게 된다는 뜻. ↩

  4. 또는, $F$ 내의 $A\_{n+1}$을 contradiction으로 대체하면 $F\_{0}$을, tautology로 대체하면 $F\_{1}$를 얻을 수 있다. ↩

  5. $F\_{0}$의 각 clause에서 $\\{A\_{n+1} \\}$를 다시 복원시킨다. ↩

You may also enjoy