9.5.2 The resolution inference rule(시험)
7장에 나오는 resolution rule을 그대로 옮기어 놓은 것이지만

라는 식에서

Unify를 계속해서 사용하여 결론을 도출한다.

다음 예시를 통해 좀 더 자세히 보자
- 모든 동물을 사랑하는 사람들은 다른 사람에게 사람 받는다.
- 동물을 죽인 누군가는 누구에게도 사랑 받지 못한다.
- Jack은 모든 동물을 사랑한다.
- Jack 혹은 고양이를 호기심에 죽인 Tuna가 있다
- 호기심이 고양이를 죽였는가?
위의 논리식을 CNF식으로 증명을 해보면


라는 Empty Solution이 나오게 된다.