인공지능(AI) #6_ 분해(Resolution), 논리곱 표준형(CNF)

안녕하세요.

이번에는 분해(resolution) 증명에 대해서 알아보도록 하겠습니다.

분해 증명에 대해 이해 하기 위해, 분해(resolution), 논리곱 표준형(CNF: Conjunctive Normal Form), 분해 알고리즘에 대해서 함께 알아보겠습니다.

---

1. 분해(Resolution)

우리는 앞의 포스팅들에서 증명을 이끌어 내는데 사용할 수 있는 추리규칙에 대해서 알아보았습니다.

그러한 추리규칙들이 건전하다. 올바르다라는 점을 함께 알아보았지만 아직 부족한 한가지는, 그러한 추리규칙들을 사용하는 추리 알고리즘이 완결적인지 알아보지 않았습니다. 여기서 완결적이라는 것은, 해당 알고리즘이 도달 가능한 목표가 존재할 때, 그것을 반드시 찾아낼수 있는가에 대한 것입니다.

따라서 이번에는 분해(Resolution)라는 추리규칙을 알아보는데, 이러한 규칙을 완결적 검색 알고리즘과 함께 사용하면 완결적인 추리 알고리즘이 도출되는 것을 함께 보도록 하겠습니다.

먼저 지금까지 다루고 있던 웜푸스 세계에 분해 규칙을 바로 적용해보도록 하겠습니다.

다음 과정에서는 분해 규칙이 어떻게 사용되는지를 보여주니 간단하게 보시면 되겠습니다.

아래의 그림에서 7.4(a)에 도달하는 단계에 대해서 생각해보겠습니다.

즉, 현재 에이전트는 [2,1]에서 [1,1]로 돌아와서 [1,2]로 가고 거기서 악취(S)를 지각하지만 미풍(B)은 지각하지 않습니다.

이를 위해 우리는 지식기지에 다음과 같은 사실을 추가합니다.

R11: ~B12

R12: B12 <=> (P11 v P22 v P13)

이렇게 두개의 사실관계를 추가하면 지금까지의 지식기지는 아래와 같습니다.

   R1 : 

   R2 : 

   R3 : 

   R4 : 

   R5 : 

출처: http://doorbw.tistory.com/55?category=684964 [Tigercow.Door]

R6 : 

R7 : 

R8 : 

R9 : 

R10 : 

출처: http://doorbw.tistory.com/55?category=684964 [Tigercow.Door]

R11: ~B12

R12: B12 <=> (P11 v P22 v P13)

R1~R10에 대한 설명은 출처를 참고하시길 바랍니다.

우리는 R10을 도출했던 방식과 같이, 아래의 방식으로 [2,2]와 [1,3]에 구덩이가 없다는 것을 알 수 있습니다.

먼저 R12에서 상호조건 소거를 적용하여, (P11 v P22 v P13) => B12를 얻을 수 있습니다.

그리고 대우명제 법칙을 적용하면, ~B12 => ~(P11 v P22 v P13) 을 얻을 수 있습니다.

이후 R11으로 전건긍정을 적용하면 ~(P11 v P22 v P13) 을 얻을 수 있으며 마지막으로 이것에 드모르간 법칙을 적용하면 ~P11과 ~P22, ~P13이라는 사실을 얻을 수 있습니다.

~P11은 이미 에이전트가 알고있기 때문에 따로 지식기지에 추가하지 않고, ~P22와 ~P13을 지식기지에 추가합니다.

R13: ~P22

R14: ~P13

이제 R3에 상호조건 소거를 이용해 다음을 얻습니다.

B21 => (P11 v P22 v P31) 그리고 R5로 전건긍정을 적용하여 다음의 사실을 지식기지에 추가할 수 있습니다.

R15: P11 v P22 v P31

이제 분해규칙을 사용합니다.

R13의 리터럴, 즉 R13의 사실 ~P22과 R15의 리터럴 R22을 분해하면 다음과 같은 분해식(Resolvent)을 얻을 수 있습니다.

R16: P11 v P31

이를 표현하면, 만일 [1,1]이나 [2,2], [3,1] 중 하나에 구덩이가 있고 [2,2]에 구덩이가 존재하지 않다면 [1,1]이나 [3,1] 중에 구덩이가 있다라고 표현할 수 있습니다.

그리고 또 한번 분해규칙을 사용합니다. R1의 리터럴 ~P11과 R16의 리터럴 P11을 통해 다음과 같은 사실을 알 수 있습니다.

R17: P31

이를 표현하면 만일 [1,1]이나 [3,1] 중 하나에 구덩이가 있고 [1,1]에 구덩이가 존재하지 않다면 [3,1]에 구덩이가 존재한다라고 표현할 수 있습니다.

위의 과정에서 마지막 부분에 두 번의 분해규칙 추리가 이용되었습니다.

이러한 단계는 이제 소개해드릴 단위 분해(unit resolution) 추리 규칙의 예시 입니다.

여기서 각 l을 리터럴이라고 합니다. 그리고 li와 m은 서로 상보 리터럴(complementary literal)입니다. 즉 하나가 다른 하나의 부정인 리터럴입니다. 분해 규칙을 정리해보자면, 절(clause, 리터럴 들의 논리합) 하나와 리터럴 하나(또는 또다른 절에서의 리터럴)로부터 새로운 절을 산출하는 것입니다.

단위 분해 규칙을 다음과 같은 완전한 분해 규칙으로 일반화 할 수 있습니다.

위의 식에서 li와 mj는 서로 상보 리터럴들입니다. 이식에서 분해가 두 개의 절을 취해서 두 절의 리터럴 중 서로 상보인 리터럴들을 제외한 모든 리터럴을 담은 하나의 새 절을 산출할 수 있습니다.

다음과 같이 예를 들 수 있습니다.

좌측의 절에서 P11이라는 리터럴과 우측의 절에서 ~P12라는 리터럴은 서로 상보리터럴입니다.

따라서 이를 제외환 새로운 절, P31 v ~P22를 얻을 수 있습니다.

분해규칙에서는 인수분해(factoring)이라는 추가적인 행동이 필요합니다.

인수분해란, 리터럴의 중복된 복사본들을 제거하는 것입니다. 예를 들어 (A v B)를 (A v ~B)로 분해하면 (A v A)가 나오는데 이는 인수분해를 통해 하나의 A로 축약될 수 있습니다.

분해규칙의 건전성은 다른 절의 리터럴 mj에 상보적인 리터럴 li를 생각해보면 쉽게 확인할 수 있습니다.

분해 규칙에서 더 놀라운 사실은, 이것이 완결적인 추리 절차들이 속한 모임의 기저를 형성한다는 점입니다. 분해 기반 정리 증명기는 명제 논리의 임의의 문장 a 와 b에 대해 a|=b의 진리를 결정할 수 있습니다. 분해가 이를 어떻게 달성하는지 함께 알아보겠습니다.

2. 논리곱 표준형(CNF: Conjunctive Normal Form)

분해 규칙은 절에만 적용되는 것을 보았습니다. 즉 절들로 이루어진 지식기지와 질의에만 유관한 것으로 보입니다. 그렇다면 우리는 분해규칙으로 모든 명제 논리를 위한 완결적인 추리 절차를 얻을 수 있을까요?

그 답은, 모든 명제 논리 문장은 절들의 논리곱과 논리적으로 동치라는 것입니다.

절들의 논리곱 형태로 이루어진 문장을 가리켜 우리는 논리곱 표준형(CNF)이라고 합니다.

그럼 문장을 CNF로 변환하는 절차를 함께 보도록 하겠습니다.

B11 <=> (P12 v P21) 이라는 문장을 CNF로 변환합니다.

1. <=>을 소거합니다. 즉, a<=>b 를 (a=>b)∧(b=>a) 으로 대체합니다.

(B11 => (P12 v P21)) ∧ ((P12 v P21) => B11)

2. =>를 제거합니다. 즉, a=>b를 ~a v b로 대체합니다.

(~B11 v (P12 v P21)) ∧ (~(P12 v P21) v B11)

3. CNF에는 ~이 리터럴에만 있어야합니다. 이를 위해 아래의 세개 방식 중 적절한 것을 적용하여 ~을 괄호 안으로 옮깁니다.

지금의 예에서는 세번째 규칙을 한번만 적용하면 됩니다.

(~B11 v P12 v P21) ∧ ((~P12 ∧ ~P21) v B11)

4. 이제 ∧, v 연산자와 리터럴들로 이루어진 부분들이 중첩된 형태의 문장이 나왔습니다. 이제 분배법칙을 적용해서 v를 ∧에 대해 적절히 분배합니다.

(~B11 v P12 v P21) ∧ (~P12 v B11) ∧ (~P21 v B11)

이렇게 해서 원래의 문장이 세개의 절의 논리곱 형태로 된 CNF로 변환되었습니다.

이전보다 언어로써 표현하기는 힘들지만 완결적인 분해 절차의 입력으로써 사용될 수 있습니다.

3. 분해 알고리즘(Resolution algorithm)

분해 규칙에 기초한 추리 절차들은 이전 포스팅에서 소개드렸던 귀류법(모순에 의한 증명)의 원리를 이용합니다.

즉, (KB∧~a)가 만족 불가능임을 보임으로써 KB|=a가 참임을 증명합니다.

분해 알고리즘은 다음 사진과 같습니다.

위의 알고리즘은 우선 (KB∧~a)를 CNF로 변환합니다. 그리고 그 CNF의 절들에 대해서 분해 규칙을 적용합니다. 상보 리터럴을 담은 각 쌍을 분해해서 제외한다음 새 절을 산출하고 그것을 절들의 집합에 추가합니다. 절들의 집합에는 중복이 허용되지 않습니다. 그러한 과정을 반복하면서 다음 두 조건 중 하나가 만족할 때 결과를 출력합니다.

- 추가할 수 있는 새로운 절이 더이상 없다. 이 경우 KB는 a를 함축하지 않습니다.

- 두 개의 절이 빈 절로 분해된다. 이 경우 KB는 a를 함축한다.

이 때, 빈 절이라는 것은 성분이 하나도 없는 논리합으로써 False와 동치입니다. 즉, (KB∧~a)에 대해 False이기에 KB는 a를 함축하는 것입니다. P와 ~P처럼 서로 상보적인 단위 절을 분해한다면 빈 절이 발생합니다.

그럼 위의 분해 절차를 웜푸스 세계에 적용해 보도록 하겠습니다.

에이전트가 [1,1]에 있을 때에는 미풍을 지각하지 못합니다. 따라서 이웃 칸에는 구덩이가 있을 수 없습니다. 이를 나타내는 지식기지는 다음과 같습니다.

KB = R2 ∧ R4 = (B11 <=> (P12 v P21)) ∧ ~B11

이제 위의 지식기지를 통해 ~P12라는 문장 a를 증명하려고 합니다. (KB∧~a)를 CNF로 변환하면 위의 그림 중 상단의 4개의 절이 나옵니다. 그리고 그 아래의 절들은 상단 절들의 쌍들을 분해한 결과입니다. 그리고 P12과 ~P12 를 분해하면 빈 절이 나오게 됩니다 이를 통해 KB는 a, 즉 ~P12를 함축합니다.

---

이렇게 해서 분해라는 추리규칙과 논리곱 표준형, CNF를 중심으로 알아보았습니다.

다음 포스팅에서는 전방연쇄와 후방 연쇄에 대해 알아보도록 하겠습니다.

궁금하거나 내용에 대한 피드백언 언제든지 댓글을 남겨주세요.