여러 가지 추론 방법
- Forward chaining: 이미 알려진 사실에서 출발해 적용 가능한 규칙을 계속 써서 새 결론을 만들어가는 자료 주도 추론
- Backward chaining: 증명하고 싶은 목표에서 출발해 그 목표를 만족시키는 하위 조건들을 거꾸로 찾는 목표 주도 추론
- Resolution: 문장들에서 서로 반대되는 리터럴을 제거해 새 절을 만들고, 최종적으로 모순을 유도하는 절 기반 추론
Forward Chaining
- 개별 명제가 지식 베이스에 추가 → 적용 가능한 모든 규칙을 실행
- 실행 결과는 지식 베이스에 새로운 명제로 추가
- 더 이상 새로운 명제를 추론할 수 없을 때까지 위 과정이 계속
- 필요한 경우 추론을 사전에 수행해서 저장할 수 있음
- 불필요한 사실이 추론되고 저장될 수 있다는 단점
- 규칙엔진(rule engine)에 주로 사용
Backward Chaining
- 특정 명제를 증명하기 위해 규칙을 역방향으로 적용
- 규칙을 적용하는데 필요한 모든 명제가 지식베이스에 있으면 증명 완료
- 논리 프로그래밍에서 주로 사용
- 비교) 가추법(abduction)
- 참인 결론으로부터 알려지지 않은 전제를 추론
- 가추법은 항상 옳은 것은 아님
분해법 Resolution
- 모든 명제를 CNF(논리곱 정규형, Conjunctive Normal Form)으로 변형
- CNF = 절 ∧ 절 ∧ ...
- 절(clause) = 리터럴 ∨ 리터럴 ∨ ...
- 절과 절을 짝지어, 부정 관계인 리터럴을 제거하여 하나의 절로 만듦
1차 술어 논리의 CNF 변환
- 스콜렘화: 존재양화사가 있는 경우, 함수 형태로 변형(아래에서 F, G)
- 동물을 사랑하는 모든 사람은 누군가에게 사랑받는다
Animal(F(x)) ∨ Loves(G(x), x)¬Loves(x, F(x)) ∨ Loves(G(x), x)
- 동물을 죽이는 모든 사람은 누구에게도 사랑받지 못한다
¬Loves(y, x) ∨ ¬Animal(z) ∨ ¬Kills(x, z)
- 잭은 모든 동물을 사랑한다
¬Animal(x) ∨ Loves(Jack, x)
- 잭이 튜나를 죽였거나 또는 호기심이 튜나를 죽였다
Kills(Jack, Tuna) ∨ Kills(Curiosity, Tuna)
- 튜나는 고양이다, 고양이는 동물이다
Cat(Tuna)¬Cat(x) ∨ Animal(x)
- 호기심이 튜나를 죽였을까?
1차 술어 논리의 분해법
- "호기심이 고양이를 죽이지 않았다"라는 명제를 가정하면
- 모순적인 결론에 도달:
- 아무도 잭을 좋아하지 않는다
¬Loves(y, Jack)
- 누군가 잭을 좋아한다
Loves(G(Jack), Jack)
- 따라서 호기심이 고양이를 죽인 것으로 결론
