First Order Logic (1차 술어 논리)(Resolution by refutation) Marcus

- 1차 술어 논리는 형식 언어로 일반적으로 술어 논리로 부르기도 한다. 명제 논리를 보다 강력하게 확장한 것이다.

- 장점

비교적 적은 수의 primitives만을 포함하고 있어도 명제 논리에 비해 매우 풍부한 표현력을 자랑한다.

- 단점

Knowledge는 complete해야 한다.

Knowledge는 일관성이 있어야 한다. (지식들 간의 conflict가 없어야 한다)

Knowledge base는 monotonic하게 증가하여야 한다.

- A Predicate Logic Example

1. Marcus was a man

Man(Marcus)

2. Marcus was a Pompeian

Pompeian(Marcus)

3. All Pompeians were Romans

∀x: Pompeian(x) → Roman(x)

4. Caesar was a ruler

Ruler(Caesar)

5. All Romans were either loyal to Caesar or hated him

∀x: Roman(x) → Loyalto(x, Caesar) ∨ Hate(x, Caesar)

6. Everyone is loyal to someone

∀x: ∃y: Loyalto(x, y)

7. People only try to assassinate rulers they aren't loyal to

∀x: ∀y:Person(x) ∧ Ruler(y) ∧ Tryassassinate(x, y) → ￢Loyalto(x, y)

8. Marcus tried to assassinate Caesar

Tryassassinate(Marcus, Caesar)

9. All men are people

∀x: Man(x) → Person(x)

- A Resolution Proof

1. Man(Marcus)

2. Pompeian(Marcus)

3. ￢Pompeian(x1) ∨ Roman(x1)

4. Ruler(Caesar)

5. ￢Roman(x2) ∨ Loyalto(x2, Caesar) ∨ Hate(x2, Caesar)

6. Loyalto(x3, y2)

7. ￢Man(x4) ∨ ￢Ruler(y1) ∨ ￢Tryassassinate(x4, y1) ∨ ￢Loyalto(x4, y1)

8. Tryassassinate(Marcus, Caesar)

- A Resolution Proof

5, 3, 2, 7, 1, 4, 8

---

- Updated at 2019-03-25 

위 전개 방식에 대한 설명이 부족하여 추가함

- CWA을 가정했을 때 참/거짓 둘 중 하나님

증명하고자 하는 hate(Marcus, Caesar) 라는 사실이 있다는 것을 추론하여 참을 증명하거나,

반대로 ￢hate(Marcus, Caesar)라는 사실이 없다는 것을 추론하여 참을 증명하면 됨. 

따라서 시작은 hate(Marcus, Caesar)의 부정인 ￢hate(Marcus, Caesar)을 상쇄하여 추론함

1단계 : ￢hate(Marcus, Caesar) + ⑤ ￢Roman(x) ∨ Loyalto(x, Caesar) ∨ Hate(x, Caesar)

=> hate가 서로 상쇄되어 x는 Marcus가 되고 제거됨

=> ￢Roman(Marcus) ∨ Loyalto(Marcus, Caesar)

2단계 : ￢Roman(Marcus) ∨ Loyalto(Marcus, Caesar) + ③ ￢Pompeian(x) ∨ Roman(x)

=> Roman이 서로 상쇄되어 x는 Marcus가 되고 제거됨

=> ￢Pompeian(Marcus) ∨ Loyalto(Marcus, Caesar)

3단계 : ￢Pompeian(Marcus) ∨ Loyalto(Marcus, Caesar) + ② Pompeian(Marcus)

=> Pompeian가 서로 상쇄되어 제거 됨

=> Loyalto(Marcus, Caesar)

4단계 : Loyalto(Marcus, Caesar) + ⑦ ￢Person(x) ∨ ￢Ruler(y) ∨ ￢Tryassassinate(x, y) ∨ ￢Loyalto(x, y)

=> Loyalto이 서로 상쇄되어 x는 marcus가 되고 y는 Caesar가 되고 제거됨

=> ￢Person(Marcus) ∨ ￢Ruler(Caesar) ∨ ￢Tryassassinate(Marcus, Caesar)

5단계 : ￢Person(Marcus) ∨ ￢Ruler(Caesar) ∨ ￢Tryassassinate(Marcus, Caesar) + ⑨ ￢Man(x) ∨ Person(x)

=> Person이 서로 상쇄되어 x는 marcus가 되고 제거됨

=> ￢Man(Marcus) ∨ ￢Ruler(Caesar) ∨ ￢Tryassassinate(Marcus, Caesar)

※ 아래 그림에서는 생략됨

6단계 : ￢Man(Marcus) ∨ ￢Ruler(Caesar) ∨ ￢Tryassassinate(Marcus, Caesar) + ① Man(Marcus)

=> Man이 서로 상쇄되고 제거됨

=> ￢Ruler(Caesar) ∨ ￢Tryassassinate(Marcus, Caesar)

7단계 : ￢Ruler(Caesar) ∨ ￢Tryassassinate(Marcus, Caesar) + ④ Ruler(Caesar)

=> Ruler가 서로 상쇄되고 제거됨

=> ￢Tryassassinate(Marcus, Caesar)

8단계 : ￢Tryassassinate(Marcus, Caesar) + ⑧ Tryassassinate(Marcus, Caesar)

=> Tryassassinate가 서로 상쇄되고 제거됨

=> □ (없음)