Resolution Theorem Proving

4. Resolution Theorem Proving

 

 

 - Resoulution by Refutation ( 반증에 의한 논리 융합)

 

 Resoulution Refutation(도출 반박) 은 사실이라고 알려진 논리와 공리를 부정하는 Goal을 설정한후, 이 것이 모순됨을 보여주어 논리가 true 임을 증명하는 방법이다. 이 증명은 아래의 순서를 따른다.

 

1) 전제나 공리를 clause form으로 둔다.

2) 증명하고자 하는것을, 부정하여 공리 집합에 추가한다.

3) 이 clause form들을 같이 도출하여, logically followed(논리적으로 따라오는) 새로운 clause 를 생성한다.

4) 증명하고자 한것을 부정한것과, 최후에 만들어진 clause를 비교하여, 이들이 empty clause를 생성하면, 증명하고자 하는

   것은 true가 된다.

 

순서만 들어서는 굉장히 햇갈릴 것이다. 하지만 우리는 2장에서 inference rule을 할때에 이미 resolution을 어떻게 사용하는지에 대해서 보았다. 그런데, 한가지 이해가 안가는 말이 있을 수 있다. Clause form 이라는게 무엇일까 ? 이는 흔히 우리들이 ∧ 와 ∨등으로 표현하는 식을 말한다. 예를들어, '말은 동물이다.' 라는 것은 horse(X) -> animal(X) 라고 쓸수 있지만, 이를 clause form으로 고치게 되면,  -horse(X) ∨ animal(X) 이다. 그렇다면 공리를 clause form으로 바꾸는 순서에 대해서 알아보겠다.

 

1) 먼저, 모든 logical connective 인 -> 와 <-> 를 제거 한다.

 

     a <-> b   =  (-a ∨  b) ∧ (-b ∨ a)

     a -> b = (-a ∨ b)

 

2) 부정으로 묶인 scope (괄호) 를 제거한다.

 

  - (a ∧ b)  = -a ∨ -b

 

3) 서로 같은 이름을 가진 변수들이 자신들의 영역에서만 고유하도록 바꿔준다.

 

  (∀X) a(X) ∨ (∀X)b(X)  =  (∀X) a(X) ∨ (∀Y)b(Y)

 

4) 모든 한정자를 왼쪽으로 옮겨서 penex normal form으로 만들어 준다.

5) skolemization을 이용해서 모든 existentail quantifier (∃) 를 없애 준다.

    (ex. ∃X horse(X) 를 skolemization 하게 되면 hore(Maxim)이 된다.

           (∀X)(∀A)(∃B)(∀C)(method(X,A,B,C)) ⇒   (∀X)(∀A)(∀C)(method(X,A,f(X,A),C))  )

6) 모든 universal quantifier를 떼어내 버린다.

7) 모든 표현을 (식) ∧ (식) 의 형태로 고친다.

8) 각각의 ∧로 구분된 식들은 하나의 clause form이 되고, 이들을 다시 rename 하여 사용한다.

 

 

아래의 예제를 보면서 이해해 보도록 하자.