9 Inference In First-Order Logic

앞에서 나온 AI가 적용될 수 있는 First-Order Logic으로 표현된 Sentence나 Situation이 존재하면 그 다음 행동이나 결론으로 추론할 수 있는지를 확인하는 단원

Forward chaining : 기존의 알려진 사실들로 하여금 새로운 사실을 추리하면서 나아가는 방법
Backward chaining : 먼저 확인하고자 하는 사실 Q로부터 시작하여 Q를 사실로써 추가하기 위해 지식기지에서 결론이 Q인 함의, 문장을 찾습니다.
Resolution Rule을 이용한 증명이 나오게 된다.

9.1 Propositional VS First-Order Inference

9.1.1 Inference rules for quantifiers

위와 같은 식이 존재한다고 하자 왕이면서 탐욕스럽다면 악마다라는 논리이다.

여기에 사람을 대입하여 새로운 논리식을 추론해 낼 수 있다. 이와 같이 일반적인 rule과 특정한 경우에 대해서 식이 나오게 된다.

그래서 문장이 주어졌을때 matching이 될지 안될지를 따져보게 된다.

만약 위의 문장과 같이 x를 John에 매칭시키는 것을 Substitutions(대치)이라고 부른다. 이는 x가 다른 것으로 대치할 수 있다는 의미이다. 그래서 이를 수식으로 SUBST(θ,α)으로 작성한다.
그 결과 식은 다음과 같이 작성되게 된다.

그리고 Existential Instantiation의 규칙에 따라 변수는 상수 기호로 바뀌게 된다. 문장은 α로 변수는 v로 그리고 상수는 k로 대체된다.

이때 Existential Instantiation의 특별한 경우를 skolemization이라고 부른다.

예를 들어 아래와 같이 Crown과 OnHead의 특정 케이스를 만드는 것을 생각해 볼 수 있다.

9.1.2 Reductuion to propositional inference

일단 정량화된 문장에서 정량화되지 않은 문장을 추론하는 규칙을 갖게 되면, first-order 추론을 명제적 추론으로 줄이는 것이 가능해진다.
그래서 첫 번째 생각은 실존적으로 정량화된 문장이 하나의 인스턴스화로 대체될 수 있듯이, 보편적으로 정량화된 문장은 가능한 모든 것의 집합으로 대체될 수 있다는 것이다.

그 예시는 바로 아래와 같다.

그래서 이 챕터 전반에 대해서도 inferencing하는 과정을 최대한 간단하게 하기 위해서 propositionalization(명제 논리화)를 시키게 된다.

9.2 Unification ANd Lifting

Unification은 같게끔 한다는 의미이다.

위와 같이 존재할 때와 같이 Unification이 일어나지 않기 떄문에 결론을 내릴 수 없다고 하는 것이다.

9.2.1 A first-order inference rule

Generalize Modus Ponens 은 아래와 같은 수식을 통해 Generalize 된 Modus Ponens를 보도록 하자

위와 같이 변수가 포함되기 때문에 무조건 같다고 할 수 없기 떄문에 P1과 P1'하고 x와 John을 Substitution 만들게 된다면 그것이 바로 세타가 될 것이고 결론도 도출되게 될 것이다.

그래서 일반화된 Modus Ponens를 보여주는 것은 추론의 과정으로써. 첫번째, 우리는 그것을 관찰하여 어떠한 문장 p와 substitution θ를 보았다.

이때 Generalized Modus Ponens는 Modus Ponens의 lifted 버전이라고 볼 수 있다.

9.2.2 Unification

UNIFY algorithm은 두개의 문장과 반환을 묶어서 하나의 문장으로 만드는 과정을 거친다.

예시로 위와 같이 관계가 잡히어 있다면 하나로 합치었을 때 위와 같은 형태의 수식이 된다고 볼 수 있다.

most general unifier 은 Unifier가 return 되어 답이 출력이 된다면 변수의 값은 같은데 기호만 다른게 출력되었다면 다음과 같이 작성하여도 상관이 없다는 것이다.

그래서 만약에 John으로 고정해야 한다면 어쩔 수 없으나 변수를 넣을 수 있다면 John을 조금 더 추상화 시키자는 개념이라고 이해하면 된다.

그래서 이 챕터에서는 MG를 가지고 Unifier하게 된다. 그래서 MGU라고 부른다.

만약에 학생들에게 시험을 내게 된다면 MGU를 찾아내라고 문제를 낼 수도 있을 것이다.

9.2.3 Storage and retrieval

위와 같은 상황을 predicate indexing 이라고 부른다. 정보들은 매우 효율적인 방법으로 저장되어 진다.

9.3 Forward Chaining

Forward Chaining은 이미 존재한 정보는 그대로 두고 계속해서 추론을 해 나아가는 것을 Forward Chaining이라고 부른다.

9.3.1 First-order definite clauses

추론의 과정 중에서 어떠한 사소한 하나라도 정확하게 하여야만 결론에 도다를 수 있다는 이야기 이다.