명제논리에서의 논리융합

(Resolution in the Propositional Calculus)

인공지능-지능형 에이전트를 중심으로 : Nils J.Nilsson 저서, 최중민. 김준태. 심광섭. 장병탁 공역, 사이텍미디어, 2000  (원서 : Artificial Intelligence : A New Synthesis 1998), Page 245~252

1. 새로운 추론 규칙 : 논리융합

  (1) wff 로서의 절

  (2) 절에서의 논리융합

  (3) 논리융합의 정당성

2. 임의의 wff 를 절의 논리곱으로 변환하기

3. 논리융합 반박

4. 논리융합 반박 탐색 전략

  (1) 순서화 전략

  (2) 정제 전략

5. Horn 절

1. 새로운 추론 규칙 : 논리융합

(1) wff 로서의 절

앞장에서 모더스 포넌스를 포함하여 여러 가지 추론 규칙을 언급하였다. 이 중 많은 규칙들은 논리융합 (resolution) 이라는 하나의 규칙으로 통합될 수 있다. 이 장에서 사용할 논리융합은 절 (clause) 이라는 특별한 형태의 wff 에 적용될 것이며, 이제 절에 대해 정의하겠다.

우선 리터럴 (literal) 은 아톰 (양 리터럴이라 부른다) 혹은 아톰의 부정 (음 리터럴이라 부른다) 중의 하나이다. 절 (clause) 은 리터럴의 집합이다. 집합은 그 안에 있는 모든 리터럴의 논리합을 의미한다. 그러므로 절은 특별한 형태의 wff 이다. 보통 절을 논리합으로 표현하지만, 논리융합에 관련된 정의에서는 집합 표시를 이용해 나타내는 것이 더 간단하다. 예를 들어, 절 {P, Q, ￢R} (P ∨ Q ∨ ￢R 과 동치) 은 wff 이다. 비어있는 절 { } (Nil 이라고 쓰기도 한다) 는 F (값이 False 인) 와 동치이다.

(2) 절에서의 논리융합

명제논리에서의 논리융합 규칙은 다음과 같이 정리될 수 있다 : 과 ( 과 는 리터럴의 집합이고 λ 는 아톰이다) 로부터 를 추론할 수 있고 를 두 절의 논리융합식 (resolvent) 이라고 부른다. 아톰 λ 는 용해되는 아톰 (atom resolved upon) 이고 이 과정을 논리융합 (resolution) 이라고 한다.

몇 가지 예를 살펴보자.

• R ∨ P 와 ￢P ∨ Q 로 논리융합 된다. 두 절은 함의를 이용하면 ￢R ⊃ P 와 P ⊃ Q 로 나타낼 수 있다. 연결 (chaining) 이라는 추론 규칙이 이 함의들에 적용되면 ￢R ⊃ Q 가 나오며 이는 논리융합식 R ∨ Q 와 동치이다. 그러므로 연결은 논리융합의 특별한 경우이다.

• R 과 ￢R ∨ P 로 논리융합된다. 두번째 절이 R ⊃ P 와 동치이므로 모더스 포넌스 (modus ponens) 도 논리융합의 특별한 경우이다.

• P ∨ Q ∨ R ∨ S 와 ￢P ∨ Q ∨ W 는 Q ∨ R ∨ S ∨ W 로 논리융합된다. 논리융합식에는 Q 가 한번 나옴을 주시하라. 이는 결국 집합과 같다.

• P ∨ Q ∨ ￢R 과 P ∨ W ∨ ￢Q ∨ R 을 Q 에 대해 논리융합이면 P ∨ ￢R ∨ R ∨ W 가 되고, R 에 대해 논리융합하면 P ∨ Q ∨ ￢Q ∨ W 가 된다. 이 경우, ￢R ∨ R 과 Q ∨ ￢Q 모두 True 이므로, 각 논리융합식의 진리값은 True 이다. 이 예에서 우리는 Q 나 R 둘 중에 하나만을 이용하여 논리융합을 해야 하며, 둘을 동시에 사용할 수는 없다. 즉, P ∨ W 는 두 절의 논리융합식이 될 수 없다.

λ 와 ￢λ 를 논리융합하면 공절 (empty clause) 이 된다. λ 와 ￢λ 는 모순이므로 λ 와 ￢λ 로부터 F 를 추론할 수 있다. λ 와 ￢λ 를 포함하는 어떤 wff 집합도 만족시킬 수 없다. 반면에 아톰과 그의 부정 (λ ∨ ￢λ 와 같은) 을 포함하는 절은 λ 값에 관계없이 True 값을 갖는다.

(3) 논리융합의 정당성

앞에서 소개된 논리융합은 정당한 (sound) 추론 규칙이다. 즉, 과 가 둘 다 True 값을 가지면 그들의 논리융합식, 도 True 이다. 이를 증명하는 한 가지 방법은 "사례별로 추론" 을 하는 것이다. 우리는 λ 가 True 가 아니면 False 라는 것을 안다. 만일 (사례 1) λ 가 True 라고 하면 λ 는 False 이다. 그러면 절이 True 이기 위해서는 가 True 이어야 한다. 만일 (사례 2) λ 가 False 라고 하면 절이 True 이기 위해서는 이 True 여야 한다. 이 두 사례를 합치면 나 중 하나는 반드시 True 임을 알 수 있다 ; 그러므로 는 True 값을 갖는다. 진리표를 이용해도 이와 유사하게 증명할 수 있다.

2. 임의의 wff 를 절의 논리곱으로 변환하기

명제논리의 임의의 wff 는 이와 동치인 절의 논리곱으로 변환할 수 있다. 절의 논리곱으로 나타낸 wff 를 논리곱 정규형 (conjunctive normal form, CNF) 이라고 한다 (논리곱의 논리합으로 나타낸 wff 는 논리합 정규형 (disjunctive normal form, DNF) 이라고 한다). 예제를 이용하여 임의의 wff 를 CNF 로 변환하는 과정을 단계적으로 보이면 다음과 같다. 예제는 ￢(P ⊃ Q) ∨ (R ⊃ P) 이다.

    1. 함의 기호를 ∨ 를 이용하는 동치식으로 바꾸어 없앤다.

 ￢(￢P ∨ Q) ∨ (￢R ∨ P)

    2. 드모르간의 법칙을 이용하여 이중 ￢기호를 없앤다.

(P ∧ ￢Q) ∨ (￢R ∨ P)

    3. 결합 법칙과 배분 법칙을 이용하여 CNF 로 변환한다. 우선,

(P ∨ ￢R ∨ P) ∧ (￢Q ∨ ￢R ∨ P) 가 되고,

(P ∨ ￢R) ∧ (￢Q ∨ ￢R ∨ P) 가 된다.

절의 논리곱 (wff 의 CNF 형태) 은 보통 절의 집합으로 다음과 같이 표시된다 (이 집합은 절의 논리곱을 암시한다).

{(P ∨ ￢R), (￢Q ∨ ￢R ∨ P)}

다음 절차는 단계 3 에서 DNF 형태의 wff 를 CNF 형태로 바꾸는 데 유용하다. 우선 DNF 형태의 wff 를 각 논리합 인자의 리터럴이 행을 구성하는 행렬로 나타낸다. 예를 들어 DNF 형태 (P ∧ Q ∧ ￢R) ∨ (S ∧ R ∧ ￢P) ∨ (Q ∧ S ∧ P) 는 다음과 같은 행렬로 나타내어진다 :

P	Q	￢R
S	R	￢P
Q	S	P

이제 각 행에서 하나의 리터럴을 선택하여 논리합으로 만든다. 이 예에서는 P ∨ R ∨ P 가 하나의 선택이 될 수 있다. 이런 가능한 선택을 모두 한다. 각 선택은 절에 해당하며 이 모든 절의 논리곱을 취하면 초기 wff 의 CNF 형태가 된다. 몇몇 절들은 단순화시킬 수 있다. 예를 들어 P ∨ R ∨ P 는 P ∨ R 로 간단해진다. 몇몇 절들은 삭제할 수도 있다. 예를 들어 P ∨ ￢P ∨ Q 는 항상 True 이므로 삭제할 수 있다. 또한 어떤 절이 다른 절에 의해 포함되는 (subsumed) 경우에도 이 절을 삭제할 수 있다 ( 에 있는 리터럴이 에 있는 리터럴 집합의 부분 집합일 때, 절 은 절  를 포함한다 (subsumes) 고 한다). 예를 들어, P ∨ R 은 P ∨ R ∨ Q 와 P ∨ R ∨ S 를 포함한다.

3. 논리융합 반박

우리는 이미 논리융합이 정당한 추론 규칙임을 보았다. 즉, 가 하나의 절일 때 는 를 함의한다. 그러나 논리융합은 완전하지는 않다. 예를 들어, P ∧ R P ∨ R 이지만, {P, R} 집합에는 아무 것도 용해되어 없어질 것이 없으므로 {P, R} 로부터 논리융합 방법을 이용하여 P ∨ R 을 추론할 수는 없다. 그러므로 논리융합 방법을 사용하여 모든 논리적 귀결을 알아낼 수는 없다. 그러나 P ∨ R 의 부정이 집합 {P, R} 과 일치하지 않는다는 것은 논리융합으로 보여줄 수 있다. 즉, 모순에 의한 증명으로 P ∧ R P ∨ R 을 입증할 수 있다.

이 과정을 설명하기 위해 P ∨ R 을 부정하면 ￢P ∨ ￢R 이다. 집합으로 표시하면 {￢P, ￢R} 이 된다. 이 절들이 P ∧ R 과 일치하지 않음을 보이기 위해 P 와 R 을 집합에 더하면 {￢P, ￢R, P, R} 이 된다. 이 집합의 구성 아톰들을 논리융합하면 공절이 만들어지며, 이는 모순을 의미한다. 그러므로 우리는 P ∧ R 로부터 P ∨ R 을 간접적으로 입증할 수 있다.

일반적으로 wff 의 집합 Δ 으로부터 임의의 wff 를 증명하기 위한 논리융합 반박 (resolution refutation) 은 다음과 같이 진행된다.

1. Δ 에 있는 wff 들을 절 형태 (clause form), 즉 절의 논리곱 집합의 형태로 바꾼다.

2. 증명하고자 하는 의 부정을 절 형태로 바꾼다.

3. 1 과 2 단계의 결과인 절들을 하나의 집합 Γ 으로 합친다.

4. Γ 에 있는 절에 논리융합을 적용하여 결과를 Γ 에 넣는 작업을 더 이상 추가될 논리융합식이 없거나 공절이 나올 때까지 반복한다.

다음 결과를 증명 없이 언급만 하겠다.

• 논리융합 반박의 완전성 (completeness) : 이면 논리융합 반박에 의해 공절이 생성된다. 그러므로 명제 논리융합은 반박 완전 (refutation complete) 하다고 한다.

• 논리융합 반박에 의한 명제논리의 결정성 (decidability) : 만일 Δ 가 절의 유한집합이고 이면 논리융합 반박 과정은 공절을 생성하지 않고 종료된다.

앞장의 블록 들기 예제에서 논리융합 반박을 이용하여 추론을 수행할 수 있다. wff 의 집합 Δ 이 다음과 같이 주어졌다.

1. BAT_OK

2. ￢MOVES

3. BAT_OK ∧ LIFTABLE ⊃ MOVES

3 번 wff 의 절 형태는 다음과 같다.

4. ￢BAT_OK ∨ ￢LIFTABLE ⊃ MOVES

증명하고자 하는 wff 의 부정은 다음과 같은 절이 된다.

5. LIFTABLE

이제 논리융합을 이용하여 다음과 같은 순서로 절을 생성한다.

6. ￢BAT_OK ∨ MOVES (5 와 4 를 논리융합)

7. ￢BAT_OK (6 과 2 를 논리융합)

8. Nil (6 과 1 을 논리융합)

이 논리융합 과정을 그림 1 과 같이 반박트리를 이용하여 나타낼 수 있다.

그림 1  논리융합 반박트리

4. 논리융합 반박 탐색 전략

논리융합 반박 과정은 "공절이 나올 때까지 논리융합을 수행한다" 로 간단하게 표현될 수 있긴 하지만 어떤 논리융합을 먼저 수행할까 결정하는 것은 매우 중요한 문제이다. 또한 어떤 논리융합은 아예 수행될 필요도 없다. 이 절에서는 이 문제에 대해 다루겠다.

(1) 순서화 전략

논리융합이 어떤 순서로 진행되어야 하는가? 이 질문은 상태공간 탐색에서 어떤 노드를 확장할 것인가에 대한 질문과 유사하다. 여러 가지 순서화 전략 (ordering strategy) 들이 제안되었는데 예를 들어 깊이우선 (depth-first) 혹은 너비우선 (breadth-first) 방법들을 정의할 수 있다. 우선 몇 가지 정의를 하자. 증명하고자 하는 절의 부정을 포함한 초기 절들을 0 번째 레벨 논리융합식이라 하자. i + 1 번째 레벨 논리융합식은 i 번째 레벨의 논리융합식과 j ≤ i 인 j 번째 레벨 논리융합식의 논리융합으로 만들어진 식이다. 너비우선 방식은 첫번째 레벨의 모든 논리융합식을 생성하고 나서 두번째 레벨의 모든 식을 생성하는 순서로 진행하는 방식이다.

깊이우선 방식은 우선 첫번 레벨의 모든 논리융합식을 생성하고 이것과 첫번 레벨 혹은 0 번째 레벨의 절을 논리융합하여 두번째 레벨의 논리융합식을 생성하는 순서로 진행하는 방식이다. 깊이 제한이 있는 경우에는 되추적 (backtracking) 방법이 이용될 수 있다. 이 책의 뒷부분에서 깊이우선 논리융합의 응용에 대해 다룰 것이다.

논리융합의 부분적인 순서를 정하기 위하여 많이 사용되는 전략을 단일 선호 (unit-preference) 전략이 있다. 이 방법에서는 단일 리터럴로 구성된 절이 적어도 하나 포함되는 논리융합을 선호한다. 이러한 절을 단일 절 (unit clause) 이라고 한다. 그림 1 의 예는 단일 선호 전략을 위배하지 않는다 (즉, 반박트리에서의 어떤 논리융합도 단일하지 않은 두 절 사이에 일어나지 않는다).

(2) 정제 전략

정제 전략 (refinement strategy) 은 절이 논리융합되는 순서에 대한 것이 아니고, 어떤 특정한 종류의 논리융합만을 허용하는 것이다 (모두는 아니지만). 이러한 제한을 일부 가해도 논리융합 반박은 완전하다.

지지 집합

(a) 절 가 과 어떤 다른 절의 논리융합식일 때 혹은 (b) 절 가 의 자식과 어떤 다른 절의 논리융합식일 때 는  의 후손 (descendant) 이라고 한다. 만일 가  의 후손이면 은  의 조상 (ancestor) 이다. 증명하려고 하는 정리를 부정하여 만든 절과 그 절의 후손들을 지지 집합 (set of support) 이라고 한다.

지지 집합 전략은 논리융합되는 절 중의 하나는 반드시 지지 집합의 아톰이 되도록 하는 것이다. 그림 1 의 논리융합 반박 과정이 바로 지지 집합의 제약조건을 만족하는 예이다.

지지 집합 전략은 반박 완전 (refutation complete) 하다 [Chang & Lee 1973, p.110]. 즉, 만족시킬 수 없는 집합에 대해 지지 집합 논리융합을 수행하면 결국 공절이 생성된다.

선형 입력

선형 입력 (linear input) 전략은 논리융합되는 절 중 적어도 하나는 초기 절들의 집합 (증명하려는 wff 의 부정을 포함한) 에 속한 아톰이 되도록 하는 것이다. 그림 1 의 논리융합 반박은 선형 입력 전략도 만족하는 것이다.

다음의 모순되는 절의 집합 예에서 알 수 있는 것처럼 선형 입력 전략은 반박 완전하지는 않다.

{P ∨ Q, P ∨ ￢Q, ￢P ∨ Q, ￢P ∨ ￢Q}

이 절들은 모델이 없으므로 논리융합 반박이 존재한다. 이 절들에 대해 논리융합 반박이 존재하지만 선형 입력 반박이 가능하지 않음을 보이는 것은 연습문제로 남긴다.

조상 여과

조상 여과 (ancestry-filtering) 전략은 논리융합되는 절 중 적어도 초기 절들의 집합에 속한 아톰이거나, 논리융합되고 있는 다른 절의 조상이어야 한다는 것이다. 조상 여과 전략은 반박 완전하다 [Luckham 1970].

5. Horn 절

절의 형태 중에서 AI 및 여러 컴퓨터 과학 분야에서 중요하게 다루어지는 특수한 형태가 있다. Horn 절은 최대 1 개의 양 리터럴만을 갖는 형태의 절이다.

다음은 Horn 절의 형태이다.

P, ￢P ∨ Q, ￢P ∨ ￢Q, ￢Q ∨ R, ￢P ∨ R

이와 같은 형태의 절은 논리학자 Alfred Horn [Horn 1951] 에 의해 처음 연구되었다.

Horn 절에는 3 가지 형태가 있다.

• 단일 아톰 (atom) - "사실" 이라고 한다.

• 함의 (implication) - 전제부 (antecedent) 는 양 리터럴의 논리곱으로 이루어지고 결론부 (consequent) 는 단일 양 리터럴로 이루어진 형태 - "규칙" 이라고 한다.

• 음 리터럴의 집합 - 전제는 양 리터럴의 논리곱으로 이루어지고 결론은 비어 있는 함의의 형태이다. 증명해야 할 wff 가 양 리터럴로 이루어져 있을 때 이 wff 를 부정하면 이런 형태가 얻어진다. 이와 같은 절을 "목표 (goal)" 라고 한다.

위 세 가지 형태의 Horn 절에 대한 각각의 예를 들면, P, P ∧ Q ⊃ R, P ∧ Q ⊃ 등이 된다.

명제논리의 Horn 절에 대한 중요한 사실은 선형 시간 연역 알고리즘이 존재한다는 것이다 [Dowling & Gallier 1984]. 직관적으로 비 Horn 절의 추론이 NP-hard 인 이유는 P ∧ Q 와 같은 양 리터럴의 논리합을 증명하려면 P 혹은 Q 를 증명해야 하는 것과 같이 여러 가지 경우를 고려해야 하기 때문이다. Horn 절에는 양 리터럴의 논리합이 존재하지 않는다.

Horn 절로 된 규칙과 사실로부터 목표를 증명하기 위한 시스템은 일반적으로 추론 순서에 대한 정보를 시스템에 제공하기 위하여 사실과 규칙을 특정한 순서로 배열하고, 각 규칙이나 목표에 있는 리터럴을 어떤 특정한 순서로 배열한 다음, 이 순서에 기반을 두고 깊이우선 방식으로 증명을 탐색한다. 이러한 과정은 술어논리 (predicate calculus) 에서 더 자세히 다룰 것이다.