[인공지능] 7. Propositional Logic - 3

 5) Analysis of Resolution Algorithm

 

  resolution rule은 어떤 complete한 search algorithm과 결합할 때 complete한 inference algorithm을 만들어낸다. 

PL-Resolution이 complete함을 보이기 위해서 resolution closure = RC(S)를 정의한다.

 

RC(S)란 "clause의 집합 S에 들어있는 clause와 그 clause끼리 resolution을 통해 만들어진 모든 clause들"에 또 resolution을 반복해서 적용해서 만들 수 있는 모든 clause들의 집합을 말한다. 

 

RC(S)가 유한하다는 것은 명백히 알 수 있다. 유한한 symbol들로 만들 수 있는 clause는 유한개 존재할 것이고, S를 구성하는 clause가 유한개이므로 RC(S)도 유한집합이다. 따라서 PL-resolution은 유한시간내에 항상 멈추는 알고리즘일 것이다. 

 

 

* Ground Resolution Theorem 

 : Propositional logic에서의 resolution에 관한 completeness theorem은 ground resolution theorem 이라고 부른다.

  " 만약 clause가 unsatisfiable하다면, 이 clauses의 resolution closure는 분명 empty clause를 포함할 것이다. "

만약 ground resolution theorem이 항상 사실이라면 이 말이 항상 사실일 것이고, 이 알고리즘은 complete하다고 할 수 있다.

 

(앞에서 했던 것은 empty clause를 포함한다면 unsatisfiable 하다는 것이었는데, 이제는 모든 unsatisfiable한 clause가 empty clause를 만들어낸다는 completeness에 관한 문제를 다루는 것이다)

 

이 theorem은 contrapositive, 대우명제를 증명함으로서 증명할 수 있다.

즉 원래 명제가 "S가 unsatisfiable 하다면, RC(S)는 empty clause가 있다" 였으므로

 

"RC(S)에 empty clause가 없다면 S는 satisfiable 하다" 를 증명해보자

 

S가 P1,...,Pk로 이루어져 있다고 해보자.

i=1 ~ k에 대해서

RC(S)안의 clause 중에서 ￢Pi 를 포함하고있을 때, 다른 literal들은 모두 false로 할당된 어떤 model이 있다면, Pi에 false를 할당하고, 그렇지 않으면(Pi를 포함하거나 ￢Pi를 포함하지만 앞의 literal 중에 true가 있는 경우) Pi에 true를 할당한다. 이 방법을 통해 우리는 모든 clause에 대해서 true를 만들 수 있다.

 

저 할당하는 방식을 이용하면, RC(S)안에 존재하는 모든 clause들을 true로 만드는 각 Pi의 할당값을 찾을 수 있다. 이 과정을 통해 P1,...,Pk가 적합한 truth value를 가진 RC(S)의 model을 구성할 수 있다. 

그런데 S의 각 clause 역시 RC(S)에 포함이 된다. 따라서 S를 구성하는 clause 모두가 true가 되는 경우가 존재하고, 따라서 S를 만족하는 model이 최소한 하나 생기게 되기 때문에 Satisfiable 하게 된다.

 

그림에서 보듯이 맨 처음에 not P1이 존재하면, P1에 false를 할당해준다. 그러면 P2, P3도 순서대로 쭉 할당할 수 있다. 이런식으로 쭉 할당하다 보면 모든 clause에 대해 true인 model이 만들어지게 되고, 그렇다면 S가 true가 되는 model 이기도 하다.

 

 

앗, 그러면 이 할당이 안되는 경우가 있지는 않을까?? Pi를 할당하려 하는데, 할당하게 되면 어떤 Clause가 false가 되어버리는 경우가 생기지는 않을까 의심이 된다. 자 그럼 이런 경우가 있다고 가정을 해보자.

 

Pi에 True 또는 False를 할당하였을 때 문제가 생기려면, 다음과 같은 경우여야 한다. 

(False ∨ False ∨ ... ∨ False ∨ Pi ) and (False ∨ False ∨ ... ∨ False ∨ ￢Pi )

이처럼 Pi 전 literal들엔 이미 false 값이 할당되었고, Pi와 not Pi가 동시에 만족해야 한다. 이런 경우엔 Pi에 어떤 값을 할당해도 어떤 clause는 false가 되어버린다.

근데 이런 상황이 오려면 RC(S)에 (P1 ∨ P2 ∨ ... ∨ Pi ) 라는 Clause와 (P1 ∨ P2 ∨ ... ∨ ￢Pi ) 라는 Clause가 동시에 있었어야 한다. 근데 만약 이런 Clause가 동시에 있었다면 Pi 는 resolution rule에 의해 진작에 사라져서 (P1 ∨ P2 ∨ ... ∨ Pi-1 )이라는 Clause가 존재했어야 한다. 근데 이 Clause를 탐색할 때 애초에 Pi-1까지 죄다 false로 할당하는 것은 불가능한 일이다. 그럼 애초에 여기서부터 잘못된 것이다. 만약 i-2까지가 다 False였다면 i-1은 최소한 true로 할당되어야 했다. 

따라서 애초에 i번째 반복은 불가능하고, 어떤 Clause가 false가 되는 일은 일어나지 않는다. 즉, S는 무조건 model을 갖는다.

 

 

정리하자면

propositional logic에서의 resolution에 대한 completeness theorem(=ground resolution theorem)은

- "clause들의 집합이 unsatisfiable, 즉 만족하는 model이 하나도 없다면, 그 clause들의 resolution closure은 무조건 empty clause를 포함한다." 라는 명제를 증명함으로서 증명될 수 있고

- 다시 이 명제를 증명하기 위해 이 명제의 대우를 증명한다. 

  "만약 closure RC(S)가 empty clause를 포함하고 있지 않으면 ,S는 satisfiable하다"

- 이 대우명제를 증명하기 위해서는 i = 1~k에 대해서 RC(S)의 clause들이 전부 참이 되도록 P1~Pk를 할당해야 한다. 이 경우 RC(S)에 있는 모든 clause들이 참이 되고, S역시 RC(S)의 clause들에 포함이 되어있으므로 S가 참이되는 model은 최소한 한 개 존재한다.

 

 

 (6) Forward/Backward Chaining Algorithms

 

 * Definite Clauses and Horn Clauses

 

  - definite clauses : disjunction으로 연결된 literal들 중에서 오직 하나만 positive이고 나머지는 negative인 clause. 

  모든 definite clause 는 premise가 positive literal들의 conjunction이고 conclusion이 single positive literal인

implication으로 나타낼 수 있다. 이러한 implication form을 사용하면 이해하기가 쉽다.

 

 - single positive literal 하나로 이루어진 sentence를 fact라고 부른다.

 - positive literal이 하나도 없는 Clause는 goal clauses이다

 

 - Horn clause는 positive인 literal이 하나 이하인 clause를 말한다. 즉 horn clause에서 positive가 1개 있으면 definite clause, 0개 있으면 goal clause이다. Horn clause는 resolution 하에 closed 되어 있다. 무슨소리냐 하면, resolution을 아무리 열심히 해도 또 다시 horn clause가 나온다는 이야기 이다. Horn form 에서는 premise를 body라고 부르고, conclusion을 head라고 부른다.

 

- Horn clauses로 나타낸 inference에서 우리는 'forward-chaining'과 'backward-chaining' 알고리즘을 사용할 수 있다. 두 알고리즘 모두 각각의 추론 단계들이 명확하고 사람들이 따라하기 쉽다는 점에서 매우 natural하다.

또한 Horn clauses를 통해 entailment 여부를 결정하는 것은 KB 크기에 대해 linear한 시간 안에 수행된다.

 

 

 

 Definite Cluase의 예시를 보자. ￢P ∨ ￢Q ∨ R 이 있을 때 이 친구는 ￢(P∧Q) ∨ R로 나타낼 수 있고, 이는 다시 P∧Q ⇒ R 로 나타낼 수가 있다.

 

 Goal Clause도 마찬가지다.  ￢P ∨ ￢Q라는 goal clause가 있을 때,  ￢P ∨ ￢Q =  ￢P ∨ ￢Q  ∨ False 이므로 ￢(P∧Q) ∨ False로 나타낼 수 있고, P∧Q ⇒ False라는 implecation으로 나타낼 수가 있다.

 

 

 

 ① Forward-Chaining Algorithm 

 - forward-chaining algorithm은 KB에 있는 알려진 fact(positive literal 한 개짜리)에서 시작한다. 

 - Forward-chaining algorithm은 inference를 horn clause로 나타낼 수 있다는 얘기고, 즉 KB에는 horn clause가 포함된다. 그리고 이 KB에 있는 horn clause들은 전부 implication 형태로 바꾸어 줄 수 있다.

 - implication에서 모든 premise들이 참임을 알고 있다면, conclusion을 known facts 집합에 새로 추가한다. 

 - 이런 과정을 query q가 fact로 추가되거나, 더 이상 추가할 fact가 없을 때까지 반복한다.

 

보면, 우선 제일 먼저 fact인 A와 B에서 시작한다. 그리고 KB안의 Horn clause를 본다. A와 B가 모두 참이므로 아래에서 세번째 명제의 premise가 모두 참이다. 그러면 conclusion인 L을 known facts 집합에 추가한다. 이 과정을 반복한다.

알고리즘을 살펴보자. 이 알고리즘은 KB와 Q quary를 input으로 받아서 이 KB가 q를 entail 하는지를 반환해주는 함수이다. 

 

먼저 count는 c번째 Clause의 premise에서 참/거짓 여부를 모르는 symbol의 수를 말한다. 처음엔 그냥 c의 premise에 있는 symbol값으로 초기화를 해준다. 

inferred는 모든 symbol에 대해서 해당 proposition symbol이 true 인지 아닌지를 저장하는 table이다. 처음엔 전부 false로 초기화해준다.

agenda는 fact들의 집합(queue)으로, 처음엔 KB에서 true인 fact들로 초기화를 해준다.

 

agenda가 empty할 때까지 다음 반복문을 수행한다.

 

p의 값에는 agenda에 가장 먼저 들어갔던 symbol이 pop되어 나온다. 즉 p는 어떠한 fact 값이다                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        

  만약 p=q이면, 즉 찾고자하는 query가 agenda에 존재하면 entail하는 것이므로 true를 리턴한다.

만약 p에 대해 inferred[p], 즉 p의 진리값이 false이면 값을 true로 바꿔주고 (agenda에 있었으므로 당연히 true인 값이다) p가 premise로 들어있는 KB의 clause c에 대해서 count[c]를 하나씩 감소시켜준다.

  그렇게 하면 p를 premise로 가지고 있는 여러 clause들에서 p의 값은 true라는 것을 알게 되어 봐야 할 clause가 하나 줄어드는 것이다. 

  만약 count[c]가 0이 되면, 즉 c의 premise가 모두 참이라면 agenda에 c의 결론을 넣어준다.

반복문이 종료되어 모든 fact를 다 검사해봤는데 알고리즘이 끝나지 않았다면, KB는 q를 entail하지 않는다는 것이므로 false를 return한다. 

 

 

 - Analysis

 

 : forward chaining은 결국 modus ponens의 활용이므로 당연히 sound하다.

  또한 모든 entailed atomic sentence가 도출되므로 complete하기도 하다. 

 

  inferred table의 마지막 상태를 생각을 해보자. 그 table에는 모~든 symbol의 T/F값이 정의되어 있을 것이다. fact에 추가된 symbol은 true이고 , 추가되지 않은 symbol은 false이겠지?

우리는 이 t/f들이 나열된 table 을 하나의 logical model이라고 생각할 수 있다. 원래 KB안에 있던 모든 definite clause는 이 model에서 true이다. 따라서 이 logical model은 KB의 model이기도 하다. 

 

  자 이 Logical model이 KB의 model 이라는 사실을 증명하기 위해서는 귀류법을 쓸 수 있다. 원래 명제의 opposite은, 이 model에서 KB의 어떤 clause (a1 ∧ ... ∧ ak ⇒ b) 가 false라는 것이다. (원래 KB안의 clause는 model에서 전부 true여야 하므로 이 명제의 반대는 하나라도 false인 clause가 있다는 이야기이다) 

  이 명제가 성립하려면 a1.... ak는 true이고 b는 false여야 한다. 그런데 이미 우리 알고리즘은 fixed point 에 도달했고, 알고리즘이 돌아가며 fixed point에 도달하는 과정에서 a1부터 ak가 모두 true였다면 b가 이미 fact로 추가되었어야 했기 때문에 모순이 생긴다.

 

따라서 logical model은 KB의 model이다. 즉, inferred된 모든 atomic sentences는 전부 KB를 만족하는 KB의 model이기 때문에, KB가 이 model에 있는 모든 atomic sentence들을 entail한다. 그러므로 모든 entailed atomic sentence q는 이 알고리즘에 의해서 반드시 추론되어야 한다. 따라서 Complete하다.

 

(query q를 만족하는 model 집합에 KB의 model 집합이 부분 집합으로 속해있다)

 

 

 ② Backward-Chaining Algorithm

  : 말 그대로 query에서부터 찾아 내려가는 방식. 

 

 - 만약 query q가 true라면 더이상의 작업이 불필요하다. 그저 true로 끝. 그렇지 않으면 conclusion이 q인 KB 안에 있는 implication을 찾아낸다. 그리고 그 implication의 premise가 true인지를 고민해본다. 알려져있다면 그걸 바탕으로 q를 추론하면 되고, 그렇지 않다면 premise를 구성하는 symbol에 대해서 또 다시 barckward chaining 으로 t/f 여부를 판단한다. 

 

 - 이 문제를 풀 때 AND-OR 그래프를 적용하면, 이 알고리즘은 AndOrGraphSearch 알고리즘과 완전히 같아진다.

 - forward chaining처럼 이 알고리즘 역시 linear time에 수행된다. 심지어 forward보다 더욱 빠르다. 왜냐면 알고 싶어하는 값과 관련된 fact들만 찾아나가면 되기 때문이다.

 - backward chaining은 goal-directed reasoning의 한 형식이다. 즉 goal에서 시작한다.