Resolution Inference Rule, Conversion to CNF, Resolution Algorithm

Properties of Search-Based Theorem Proving Algorithms

- Sound?

• Yes. 적용하는 inference rule 들이 sound 하기 때문이다.

- Complete?

• inference rule 들이 매우 많은데 어떤 것을 사용할 지 알 수 없기 때문에 증명하기가 어렵다.

- 따라서 연구자들은 inference rule 을 하나만 사용하는 알고리즘을 고안했다. 그리고 그 알고리즘이 complete 한 것을 증명하였다. -> resolution (하나의 inference rule)

 

 

 

The Resolution Inference Rule

- Unit resolution rule

• dnl1...lk 는 unit literal 이고, m은 단위 literal 일 때, 
• l1 v ... v li-1 v li+1 v ... v lk 는 참이다. 이때 li 는 없는데 li와 m은 complementary literal 관계이다. ) 

 

- Full resolution rule

• 입력으로 들어온 literal 두개가 모두 literal 의 disjunction 이다. 
• li 와 mj 는 complementary 일 때, 이 둘을 제외한 것들의 or 연산이 참이다.

- 예)

• P1,1 과 ㄱP1,1 이 complementary 하기 때문에, 이 둘을 제외한 P3,1 V ㄱ P2,2 는 참이다.

-> sound 하다. P1,1 과 ㄱP1,1 은 complementary 하므로 둘 중 하나는 무조건 false 인데, P1,1 V P3,1 과 ㄱP1,1 V ㄱP2,2 는 참이기 때문에, 즉 P3,1 과 ㄱP2,2 둘 중 적어도 하나가 참이여야 한다. 따라서 밑은 항상 참이다.

 

 

 

Completeness of the Resolution Inference Algorithm

- Caluses (절)

• literal 들의 disjunction (or)
• P1,2 V ㄱP2,1

- Conjunctive normal form (CNF)

• clauses 들의 Conjunction

• 

  

- resolution inference rule 은 CNF 에만 적용이 된다.

위와 같은 unit resolution rule 은 input 으로 두 개의 참인 clause 가 들어온다. 따라서 이는

다음과 같이 CNF 로 표현될 수 있다. 

-> 따라서 resolution inference 를 사용하려면 모든 문장들을 CNF 로 변환해야 한다.

 

 

Conversion to CNF

 

 

Resolution Algorithm

- KB |= a 를 보이기 위해서 KB ∧ ㄱa 가 unsatisfiable 한 것을 보이면 된다. (모순에 의한 증명)

- CNF 는 clause 들의 집합이므로, 우리는 초기의 clause 집합을 가지고 있는 것이다.

- clause 들에 대해서 가능한 resolution rule 을 적용하고, 새로운 clause 가 만들어진다면 clause 집합에 추가하게 된다.

- 이러한 과정을 다음까지 반복한다.

• 새로운 clause 가 더 이상 만들어지지 않는 경우 -> KB 는 a 를 entail 하지 않는다.
• 두 개의 cluase 가 빈 clause 를 만든 경우 -> KB는  a를 entail 한다.
  • ex) P 와 ㄱP 같은 두 개의 complementary literal 에 의해 Empty clause 가 만들어진다. -> 알고리즘을 종료하고 Yes 를 대답해낸다.

- 예)