서술 논리를 이용한 지식의 표기

 

인공지능 : Elaine Rich 저서, 유석인.전주식.한상영 편역, 상조사, 1986 (원서 : Artificial Intelligence, McGraw-Hill, 1983,  Artificial Intelligence (2nd ed, 1991)), Page 145~185

 

1. 지식의 표기

2. 논리 기호에 의한 사실의 표기

3. 계산 가능한 함수와 술어형 명제에 의한 지식의 표기

4. 비교 흡수 방법 (Resolution)

     (1) 절의 형태 (Clause Form) 로 변환

     (2) 비교 흡수 과정의 기본 원리

     (3) 명제 논리에서의 비교 흡수 방법

     (4) 단일화 알고리즘 (Unification Algorithm)

     (5) 서술 논리에서의 비교 흡수 방법

     (6) 여러 치환의 수행

     (7) 질문에 답하기

5. 연역법 (Natural Deduction)

6. 요약

7. 연습문제

 

 

1. 지식의 표기

인공 지능 분야에 속하는 복잡한 문제를 풀기 위해서는 많은 양의 지식이 필요하며, 또한 이 지식을 처리하는 기법을 사용하여 새로운 문제에 대한 풀이를 얻을 수 있다.

탐색을 바탕으로 하여 지식을 처리하는 매우 일반적인 방법에 관하여 지금까지 알아보았다. 이 방법은 문제를 푸는데 사용될 지식의 표기 방법에 대해서는 언급할 필요가 없을 만큼 매우 일반적인 방법이었다. 예를 들어, A* 알고리즘에서는 문제 영역에 특수한 지식에 대해 논의하지 않고도 후계 노드를 만들고, 함수 h' 의 값을 계산할 수 있었다. 비록 이렇게 지식의 표기 방법에는 무관한 풀이 기법을 사용하여, 다양한 여러 가지 문제를 적절히 풀 수 있고, 많은 문제 풀이 방법의 기초를 이룰 수 있지만, 바로 이러한 일반성 때문에 이들의 사용 범위는 매우 제한되어 있다. 지식의 표기 방법에 따라 특수한 지식을 표기하는 모델을 사용하여, 이 모델에 작용하는 상당히 특수하고 강력한 추론 기법을 얻어 문제를 풀 수 있다.

인공 지능 분야의 프로그램에서는, 지식이나 사실을 표기하기 위해 여러 많은 기법들이 사용된다. 그러나 이 기법들을 논의하기에 앞서, 지식을 표기할 때 언급되는 다음 사항에 대해 살펴 보아야 한다 :

표기된 사실을 문제 풀이에 사용하기 위해서는, 사실을 표기된 사실로 대응시키고, 표기된 사실을 사실로 대응시킬 함수가 있어야 한다.

사실을 표기하기 위해 가장 널리 쓰이는 한 가지 방법은 자연 언어 (natural language) 로 표기된 문장이다. 프로그램에서 사용될 사실의 표기법과는 관계없이 시스템에 쉽게 정보를 입력하고, 사용하기 위해서 사실을 표기하는 자연 언어에 대해 알아 볼 필요가 있다. 이 경우, 문장을 실제로 사용될 표기로, 표기된 사실을 다시 문장으로 대응시킬 함수가 있어야 한다.

수학적 논리를 사용하여 사실을 표기한 간단한 예를 살펴 보자. 다음과 같은 영어 문장이 있다 :

    Spot is a dog. (스팟은 강아지이다.)

이 문장을 논리 형식을 사용하여

    Dog (Spot)

이라 표기할 수 있다. 모든 개가 꼬리를 가지고 있음을 표기하기 위해, 논리의 연역 추론 기법을 사용하여

    Hastail (Spot)

이라고 이 사실을 표기할 수 있다. 이때 적절한 대응 함수를 사용하여, 이에 대응하는 영어 문장,

    Spot  has a tail (스팟은 꼬리를 가지고 있다.)

을 얻을 수 있다. 혹은 새롭게 표기된 사실을 이용하여, 필요한 어떤 행동을 적절히 취할 수 있다. 그림 1 은 세 종류의 대상이 서로 어떻게 관련되어 있는지를 보여 준다.

그림 1  사실과 표기 간의 대응

일반적으로 이용 가능한 대응 함수는 일 대 일 대응이 아니라, 사실상 이들은 함수라기보다 다 대 다 관계 (many-to-many relation) 라 볼 수 있다 (즉, 정의 구역에 속하는 각 원소가 공변역 내의 여러 원소에 대응하며, 정의 구역에 속하는 여러 원소가 공변역 내의 한 원소에 대응한다). 이것은 특히 주어진 어떤 사실을 영문으로 표기했을 때 발생한다. 예를 들어 문장 "All dog have tails" 와 문장 "Every dog has tail" 은 같은 사실을 나타낸다. 반면 전자는 모든 개가 적어도 하나의 꼬리를 가졌다는 사실이나, 혹은 한 마리의 개가 여러 개의 꼬리를 가졌다는 사실을 나타낸다. 앞의 간단한 예에서 알 수 있듯이, 영어 문장을 논리 명제와 같은 다른 표기법을 사용하여 바꾸어 표현하기 위해서는 문장이 어떤 사실을 나타내는지 결정한 후, 이 사실을 적정한 형식을 사용하여, 문제를 풀 때 직접 처리될 수 있도록 표기된 형태로 바꾸어 표현해야 한다.

2. 논리 기호에 의한 사실의 표기

논리 기호를 사용하여 사실을 표기할 수 있는데, 논리 형식론에서는, 수학적 연역 추론 기법을 이용하여 이미 존재하는 사실로부터 새로운 사실을 이끌어낸다. 논리 형식으로 표기된 이미 알고 있는 문장으로부터 새로운 문장이 참인지를 추론하면서 증명할 수 있다. 이미 참으로 인정된 명제들로부터 새로운 참인 명제를 연역 추론하며 증명하는 이 방법은 단지 수학에서만이 아니라, 문제에 대한 풀이를 얻고자 하는 인공 지능 분야에서도 사용될 수 있다. 정수론이나 기하학과 같은 수학적인 문제를 증명하는 것은 초기 인공 지능 분야의 관심이었으며, 현재에도 여전히 이 분야에서 중추적인 부분이 되고 있다. 그러나 이러한 수학적 기법을 수학의 범위를 벗어나, 일반적인 문제에까지 이용할 수 있다. 어려운 탐색 문제를 제어하기 위해서는, 연역 추론 기법과 경험적으로 얻은 지식의 사용이 필요한데, 이러한 측면에서 볼 때 탐색의 제어 문제와 수학의 여러 복잡한 문제는 서로 다를 바가 없다.

먼저, 명제 논리 (propositional logic) 를 사용하여, 인공 지능 분야에서 필요로 하는 지식을 표기하는 방법에 대해 살펴 보자. 명제 논리는 다루기 쉽고, 또한 이에 대한 결정 과정 (decision procedure) 이 존재하기 때문에 지식을 표기하는데 사용된다. 명제 논리에서의 잘 구성된 공식 (well-formed formulas : wffs) 으로 쓰여진 논리적 명제 형태로 현실 세계의 사실을 표기하는데, 이에 대한 예가 그림 2 에 있다.

이 명제들을 사용하여, 예를 들어, 만약 비가 오면 날씨가 맑지 않다라는 것을 연역 추론할 수 있다.

비가 오고 있다.

        RAINING

날씨가 맑다.

        SUNNY

바람이 분다.

        WINDY

만약 비가 오면 날씨가 맑지 않다.

        RAINING → ~SUNNY

그림 2  명제 논리의 예

위의 예로부터 명제 논리의 한계성에 대해 알아 보자.

    Socrates is a man. (소크라테스는 사람이다.)

라는 문장을

    SOCRATESMAN

이라고 표기할 경우,

    Plato is a man. (플라톤은 사람이다.)

라는 문장을

    PLATOMAN

으로 표기된다. 사실의 표기를 위해 위와 같은 방법을 사용한다면, 위의 두 문장은 완전히 독립적인 주장으로 간주되어 이로부터 소크라테스와 플라톤 간의 어떤 유사성도 이끌어 낼 수 없다. 이 사실을

    MAN(SOCRATES)

    MAN(PLATO)

라고 표기하는 것이 더욱 적절한데, 이는 표기의 구조에 지식 자체의 구조가 반영되기 때문이다.

    All men are mortal. (모든 사람은 죽는다.)

라는 문장을 표기할 때, 이미 알려진 죽은 사람 개개인에 대해 별개의 문장을 사용하지 않을 경우 사람에 대한 한정 (quantification) 이 필요하기 때문에 명제 논리에 의해 이를 표기하는 것은 어려운 일이다.

지식을 표기하는 방법으로 서술 논리가 많이 사용되는데, 이것은 명제 논리로 표기하기에 부적합한 것들을 서술 논리로 적절히 표기할 수 있기 때문이다. 서술 논리에서 현실 세계의 사실은 wff 로 쓰여진 언명 (statement) 으로 표기된다. 그러나 사실을 표기하는데 서술 논리를 사용하는 가장 중요한 이유는 지식의 표기 방법으로 논리적 언명을 사용할 경우 이 지식으로부터의 추론이 가능하기 때문이다. 명제 논리에서의 명제에 대한 타당성을 결정하는 것은 계산하기 어려운 것이지만, 예외가 없는 일정한 방법에 따라 할 수 있다. 따라서 지식을 표기하는 적절한 방법으로 서술 논리를 채택하기에 앞서, 이 서술 논리를 사용할 때, 지식으로부터의 추론이 가능한지 여부를 조사해야 한다. 다행히 이 조사에 대한 결과는 긍정적이다. 서술 논리는 이미 존재하는 문장으로부터 새로운 문장을 추론하는 방법을 제공한다. 그러나 명제 논리에서와는 달리, 서술 논리에는 결정 프로시쥬어 (decision procedure) 가 불필요하다. 제안된 정리가 정말로 정리라면, 이에 대한 증명을 찾기 위한 과정이 필요하지만, 제안된 문장이 정리가 아니라면 이 과정의 수행이 종료되지 않는 경우가 있다. 이런 간단한 과정은 일정한 방법에 따라 공리에 추론 규칙을 적용하여 정리를 생성하는데, 이렇게 하여 생성된 각각의 정리가 처음에 증명하고자 하는 정리인지 조사하게 된다. 그러나 이 방법은 특별히 효율적이라고 단언할 수 없기 때문에, 더 좋은 방법을 찾아야 한다. 서술 논리를 위한 어떤 결정 프로시쥬어도 존재하지 않는다는 부정적인 결과가 인공 지능 분야에 거의 직접적인 영향은 끼치지 못한다 할지라도, 이 부정적인 결과는 도움이 된다. 왜냐하면, 비록 정리가 아닌 것에 대해서는 종료가 보장되지 않더라도, 효율적인 증명 과정을 찾는 탐색 과정에서 정리를 증명할 수 있는 과정을 발견하게 된다면, 원하는 풀이를 얻었다는 사실을 이 부정적인 결과로부터 알 수 있기 때문이다. 또한 모든 가능한 입력에 대해 유한 시간 내에 결과를 출력하는 결정 프로시쥬어는 존재할 수 없다는 사실이 현실의 문제를 푸는 과정에서 주어지는지의 모든 입력에 대해 유한 시간 내에 결과를 출력하는 결정 프로시쥬어가 존재할 수 없다는 것을 의미하지는 않는다. 서술 논리의 이론적인 비결정성 (undecidability) 에도 불구하고 인공 지능 분야에서 사용될 지식을 표기하고 처리하는 적절한 방법으로 이 서술 논리가 사용된다.

간단한 예를 살펴봄으로써, 지식을 표기하기 위해 사용되는 서술 논리를 논의해 보자. 다음 문자의 집합이 주어졌다 :

    1. Marcus was a man. (마커스는 사람이었다.)

    2. Marcus was a Pompeian. (마커스는 폼페이 사람이었다.)

    3. All Pompeians were Roman. (모든 폼페이 사람은 로마인이었다.)

    4. Caesar was ruler.( 시이저는 통치자였다.)

    5. All Romans were either loyal to Caesar or hated him.
       (모든 로마인들은 시이저에 충성하였거나 그를 미워하였다.)

    6. Everyone is loyal to someone. (모든 사람은 누군가에게 충성한다.)

    7. People only try to assassinate rulers they are not loyal to.
       (사람은 그들이 충성하지 않는 통치자의 암살을 기도한다.)

    8. Marcus tried to assassinate Caesar. (마커스는 시이저를 암살하려 했다.)

위 문장으로 표기된 사실을 서술 논리의 다음과 같은 wff 들의 집합으로 표기할 수 있다 :

    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)

여기서는 많은 사람이 동일한 이름을 가질 수 있음에도 불구하고 표기에 사용된 이름이 유일한 사람을 나타내는지에 대해 언급하지 않았다. 때때로, 동일한 이름을 가진 여러 사람 중에서 특정한 언명에 언급될 사람을 결정하기 위해 많은 양의 지식과 추론이 사용된다.

영문에서 'or' 는 포섭적인 논리합 (inclusive or) 을 의미할 때도, 배타적인 논리합 (exclusive or) 을 의미할 때도 있다. 위에서의 'or' 는 포섭적인 논리합으로 사용되었다. 영어 문장에 나타난 or 가 실제로 배타적인 논리합을 의미할 수도 있는데, 이것은 다음과 같이 표기하여 나타낸다 :

    ∀x Roman(x) → ((loyalto(x, Caesar) ∨ hate(x, Caesar))
                           ∧ ~(loyalto(x, Caesar) ∧ hate(x, Caesar))

    6. Everyone is loyal to someone.
           ∀x∃y loyalto(x, y)

영어 문장을 논리적 문장으로 변환시킬 때 발생하는 가장 큰 문제는 한정사 (quantifier) 의 범위이다. 위 문장이, 각 사람에 대해 그가 충성할 어떤 사람 - 각 사람은 서로 다른 사람에 충성할 수도 있다 - 이 존재하는 것을 말하는가, 혹은 모든 사람이 충성할 어떤 사람이 존재하는 것 (이것은 ∃y ∀x loyal to (x, y) 라 쓸 수 있다) 을 말하는가? 두 가지 번역 중, 상황에 따라 더욱 적절한 것을 택해 사용한다.

    7. People only try to assassinate rulers they are not loyal to.
            ∀x∀y person(x) ∧ ruler(y) ∧ tryassassinate(x, y) → ~loyalto(x, y)

이 문장은 매우 모호하다. 이 문장이 사람들이 암살하고자 하는 통치자는 그들이 충성하지 않는 통치자임 (여기서는 이 의미로 사용한다) 을 의미하는지 혹은 사람들이 의도하는 유일한 행위는 그들이 충성하지 않는 통치자를 암살하고자 하는 행위임을 의미하는지 확실히 알 수 없다.

이 문장을 표기할 때, "암살을 기도한다" 를 하나의 서술형 명제 (predicate) 로 선택하였다. 이 서술형 명제는 암살을 기도한다는 것을 추론할 때 이용될 사실을 매우 간단히 표기한 것이다. 그러나 이 표기법으로는, 암살을 기도하는 것과 다른 어떤 것을 시도하는 것 간의 관계 및 암삭을 기도하는 것과 실제로 암살한 것 간의 관계를 쉽게 나타낼 수가 없다. 만약 이러한 관계가 필요하다면, 다른 표기법을 선택해야 한다.

    8. Marcus tried to assassinate Caesar.
           tryassassinate(Marcus, Caesar)

영어 문장을 논리적 언명으로 변환시키려는 위의 간단한 시도로부터, 이 작업이 얼마나 어려운 것인지를 알 수 있다.

    Was Marcus loyal to Caesar? (마커스는 시이저에 충성하였는가?)

라는 질문에 대한 답을 찾기 위해 앞에서 소개된 여덟 개의 언명을 사용한다고 하자. 언명 7 과 8 을 사용하여 마커스는 시이저에 충성치 않았음을 증명할 수 있다 (시제의 구별은 무시한다). 원하는 목표 - ~loyalto(Marcus, Caesar) - 로부터 후진 추론하면서, 형식적인 증명을 해 보자. 이 목표를 증명하기 위해 추론 규칙을 사용하여, 만족스럽지 못한 것이 하나도 남지 않을 때까지 이 목표를 다른 목표로 변환하고, 새로이 얻은 목표를 다시 다른 목표로 계속 변환시킨다. 이 과정에는 AND-OR 그래프의 탐색이 필요하다. 편의상, 하나의 유일한 경로만을 보이고자 한다. 그림 3 은 필요하지만 얻을 수 없는 목표의 집합을 공집합으로 축소시킴으로써 목표의 증명을 찾아내려는 시도를 보여 준다. 그러나 목표 person(Marcus) 가 이용 가능한 어떤 언명에 의해서도 만족될 수 없기 때문에 이 시도는 실패이다.

그림 3  ~Loyalto(Marcus, Caesar) 을 증명하는 과정

비록 마커스가 사람인지는 알고 있지만, 앞의 언명들로부터는 마커스가 인간임을 추론할 수 없다. 이를 위해 다음과 같이 표기된 사실이 필요하다 :

    9. All men are people.
           ∀x man(x) → person(x)

이제 원하는 목표를 만족시켜, 마커스가 시이저에 충성하지 않았다는 것을 증명할 수 있다.

이 간단한 예로부터, 영어 문장을 논리적 언명으로 바꿔 새로운 언명을 연역 추론하는 과정에서, 다음과 같은 세 가지 중요한 문제점이 발생함을 알 수 있다 :

연역 추론할 언명을 미리 알 수 없는 상황에서는 또 다른 문제가 발생한다. 위의 예에서는 "Was Marcus loyal to Caesar?" 라는 질문에 대한 답을 찾아야 한다.

    loyalto (Marcus, Caesar)

를 증명해야 할지, 혹은

    ~loyalto (Marcus, Caesar)

를 증명해야 할지를 프로그램은 어떻게 결정하는가? 이를 위해 여러 가지 방법이 있는데, 제안된 진리로부터 공리 (axiom) 로 후진 추론하는 방법 대신, 전진 추론하면 어떤 답을 얻게 될지 알아보자. 일반적으로, 이 방법에는 공리로부터의 전진 추론시 분기 계수가 엄청나게 커서 주어진 시간 내에 답을 얻을 수 없다는 문제점이 존재한다.

다른 또 하나의 방법은 경험적 지식의 규칙을 사용하여 가능성이 높은 답을 찾아, 먼저 이것에 대한 증명을 시도하는 것이다. 합당한 만큼의 노력 후에도 이것을 증명할 수 없다면, 다른 답에 대해 시도한다. 정리가 아닌 것을 증명하고자 할 경우, 어떤 증명 과정도 유한 시간 내에 이것에 대한 결과를 낼 수 없기 때문에, 노력에 제한을 둔다는 개념은 중요하다. 또 다른 방법은 두 답에 대한 증명을 동시에 시도하여 둘 중 어느 하나에 대한 증명을 찾으면, 이 과정을 중단하는 것이다. 그러나 질문에 대한 답을 찾을 때 이용 가능한 정보가 충분히 준비되지 않을 경우, 프로그램이 유한 시간 내에 답을 찾지 못할 수가 있다. 다른 또 하나의 방법은 한 답을 증명함과 동시에 이것이 답이 아님을 증명하는 것이다. DISPROVER 에 이 기법이 사용되었는데 DISPROVER 는 풀이가 존재하지 않음을 보인다. 만약 풀이가 존재할 경우, DISPROVER 는 풀이를 찾을 수 있음을 알리는 정보를 제공한다.

3. 계산 가능한 함수와 술어형 명제에 의한 지식의 표기

앞 절에서 논의된 예에서, 간단한 모든 사실은

    tryassassinate(Marcus, Caesar)

와 같은 개개 서술형 명제의 결합으로 표기되었다. 사실의 수가 적거나, 사실 자체가 매우 비 구조적일 경우, 이와 같이 표현할 수 있다. 그러나

gt (1, 0)          lt (0, 1)

gt (2, 1)          lt (1, 2)

gt (3, 2)          lt (2, 3)

.                   .

.                   .

.                   .

과 같이 간단한 예를 표기하고자 하는 경우를 살펴 보자.

위 사실을 각각 개별적으로 표기하는 것은 비효율적이다. 왜냐하면, 이와 같은 사실이 무한히 많이 존재하기 때문이다. 필요에 따라 각각을 얻어낼 수 있는 함수가 존재할 경우, 이 사실을 모두 기록하는 것은 매우 비효율적이다. 즉 계산이 가능한 서술형 명제를 사용하여 사실을 더욱 적절히 표기할 수 있다. 증명 과정이 이러한 서술형 명제를 이용할 경우, 데이터 베이스에서 그것을 찾거나, 연역 추론하는 대신, 이 서술형 명제를 평가하여 진리값을 돌려주는 과정을 정해진 규칙과 함께 규정하여, 필요에 따라 호출한다.

계산이 가능한 서술형 명제뿐만 아니라, 계산 가능한 함수를 적절히 사용함으로써 사실을 더욱 효율적으로 표현할 수 있다.

    gt (2 + 3, 1)

의 진리값을 구한다고 가정하자. 매개 변수로 2 와 3 이 주어진 덧셈 함수값을 먼저 계산한 후, 매개 변수 5 와 1 을 gt 에 보낸다.

다음 예는 계산 가능한 함수와 서술형 명제를 적절히 사용하는 방법을 설명해 준다. 이것은 등호의 개념을 이용하여, 증명의 수행 동안 필요에 따라 같은 물체들을 서로의 대용물로 사용한다.

마커스에 대한 다음 사실들을 살펴 보자 :

    1. Marcus was a man. (마커스는 사람이었다.)

                     man (Marcus)

여기서도 시제를 무시하였다.

    2. Marcus was a Pompeian. (마커스는 폼페이 사람이었다.)

                    Pompeian (Marcus)

    3. Marcus was born in 40 A.D. (마커스는 A.D. 40 년에 태어났다.)

                    born (Marcus, 40)

편의상, 일상 생활에서 A.D. 를 생략하였다. 만약 B.C 를 표기해야 할 경우, 음수 기호와 같은 것을 사용하여 이를 표기할 수 있다. 만약 문장을 표기된 문장으로, 표기된 문장을 문장으로 변환시킬 수 있는 방법이 있다면, 표기된 문장이 문장과 유사할 필요는 없다. 이러한 이유 때문에, 양수와 음수같은 표기법을 선택하여 프로그램을 쉽게 처리할 수 있다.

    4. All men are mortal. (모든 사람은 죽는다.)

                    ∀x man(x) → mortal(x)

    5. All Pompeians died when the volcano erupted in 79 A.D.
       (A.D. 79 년에 화산이 폭발하였을 때, 모든 폼페이 사람들은 죽었다.)

                    erupted (volcano, 79) ∧ ∀x (Pompeian(x) → died(x, 79))

이 문장은 위의 두 가지 사실을 표기하며, 또한 폼페이 사람들을 죽게 했던 화산의 분출이라는 증명할 수 없는 사실을 표기한다. 만약 동시에 발생한 사건 간에 인과 관계의 가능성이 있다고 생각되면, 이런 인과 관계를 가정한다.

이 문장을 번역할 때 발생하는 또 다른 문제는 화산이 나타내는 대상을 결정하는 문제이다. 지구상에는 많은 화산이 존재한다. 물론 여기서 말하는 화산은 폼페이 근처에 있고 A.D. 79 년에 폭발한 베수비어스 화산이다. 일반적으로 대상을 결정하기 위해서는 많은 추론과 이를 위한 지식이 필요하다.

    6. No mortal lives longer than 150 years. (어떤 생물도 150 년 이상 살 수 없다.)

                    ∀x∀t1∀t2 mortal(x) ∧ born(x, t1) ∧ gt(t2-t1, 150) → dead(x, t2)

여러 가지 방법을 사용하여 이 문장의 내용을 나타낼 수 있다. 예를 들어 "age" 라는 함수를 사용하여 이것의 함수값이 150 보다 적거나 같음을 주장할 수 있다. 그러나 위에 보여진 표기가 이보다 더욱 간단하고, 이 문장의 표현에 적합하다.

    7. It is now 1985. (올해는 1985 년이다.)

                    now = 1985

여기서는 서로 대신 사용할 수 있는 동일물의 개념을 이용하였다.

Is Marcus alive? (마커스는 살아 있는가?) 라는 질문에 대한 답을 찾아 보자. 주어진 언명들로부터, 두 가지 방법에 의해 이 문제에 대한 답을 추론할 수 있다. 화산 폭발로 마커스가 죽었다는 것을 보일 수도 있고, 150 년 이상 살 수 없다는 사실로 그는 죽어야만 한다는 것을 보일 수 있다. 그러나 앞의 예에서처럼 이 두 경로를 따라 가며 증명을 완성하기 위해 기타 지식들이 필요하다. 예를 들어, 죽음에 관해 말하는 언명은 있지만, 존재하고 있음과 관련된 언명들은 없다. 따라서 다음과 같은 사실들을 첨가한다 :

    1. Alive means not dead. (살아 있음은 죽지 않았음을 의미한다.)

                    ∀x∀t alive(x, t) ↔ ~dead(x, t)

죽지 않은 것은 살아 있는 것을 의미한다는 사실은 생물에 대해서만 성립한다. 따라서 엄격히 말하면 위 언명은 옳지 않다 (의자는 죽은 것도 살아 있는 것도 아니다). 여기서도 시제를 무시했다. 이것은 모든 상황에서 동일한 의미를 갖는 경우는 드물다는 사실을 보여 준다.

    2. If someone dies, then he is dead at all later times.
       (만약 누군가가 죽는다면, 그는 그 후 시대에서도 죽어 있다.)

                    ∀x∀t1∀t2 died(x, t1) ∧ gt(t2, t1) → dead(x, t2)

이것은 죽은 사람은 그 이후에도 죽어 있음을 나타낸 것으로, 그가 죽었던 해에 그가 죽어 있는지에 대한 의문은 무시하였다. 이 의문을 해결하기 위해, 해를 보다 작은 시간 단위로 나누어야 한다. 만약 (year 1, month 2) 동안에 죽었던 사람에 대해 month 2 가 month 1 보다 앞설 때 "One is dead at (year 1, month 1)" 과 같은 규칙을 첨가할 수 있다. 필요에 따라 일, 시간까지 해를 세분할 수 있다.

지금까지 표기되었던 모든 사실에 대한 요약이 그림 4 에 나타나 있다.

1. man (Marcus)

2. Pompeian (Marcus)

3. born (Marcus, 40)

4. ∀x man (x) → mortal (x)

5. ∀x Pompeian (x) → died (x, 79)

6. erupted (volcano, 79)

7. ∀x∀t1∀t2 mortal (x) ∧ born (x, t1) ∧ gt (t2-t1, 150) → dead(x, t2)

8. now = 1985

9. ∀x∀t alive(x, t) ↔ ~dead(x, t)

10.∀x∀t1∀t2 died(x, t1) ∧ gt(t2, t1) → dead(x, t2)

그림 4  마커스에 관한 사실들의 집합

 

그림 5  Marcus Is Dead 를 증명하는 한 방법

그림 6  That Marcus Is Dead 를 증명하는 다른 방법

    ~alive (Marcus, now)

를 증명함으로써, "Is Marcus alive?" 라는 질문에 대한 답을 찾아 보자. 그림 5 와 그림 6 에 이를 위한 두 가지 증명이 소개되었다. 각 증명의 끝에 나타난 nil 은 증명되기 위해 남아 있는 조건의 리스트가 전부 사용되어 성공적으로 증명되었음을 나타낸다. 증명 과정 중 나타난

    a ∧ b → c

형태의 언명에서 a 와 b 는 독립적인 부 목표로써 설정되었다. 그러나 a 와 b 가 동일한 변수를 사용할 경우, 이들 각각에 대해 모순이 없는 치환 대상을 만들 수 있기 때문에 독립적인 부 목표가 아닐 수도 있다. 예를 들어 그림 6 의 언명 3 을 사용하는 단계를 살펴 보자. t1 에 40 을 대입함으로써 언명 3 을 사용하여 목표

    born (Marcus, t1)

을 만족시킬 수 있지만, 또한 두 개의 t1 이 언명 4 에 나타난 것과 동일한 변수이기 때문에

    gt (now-t1, 150)

에 나타난 t1 에 40 을 대입해야 한다. 훌륭한 증명 과정에는 일치하는 것이 존재하는지 결정하는 방법과 증명을 통해 균일하게 대입하는 것을 보장하는 방법이 포함되어야 한다. 이 두 가지를 위해 사용되는 기법이 다음에 소개된다.

지금까지 보아 온 증명으로부터 다음 두 가지가 명백해졌다 :

첫번째 관찰로부터, 중요한 추론을 수행하기 위해서는 추론 과정 중 더욱 가깝게 결론으로 이끄는 언명이 필요함을 알 수 있다. 컴퓨터로부터 이 언명을 얻어내는 것은 어려운 문제로서, 이것에 대한 적절한 답을 여전히 찾지 못했다.

두번째 사실로부터 이와 같은 증명을 위해 필요한 일을 수행하는 프로그램을 작성하는 것이 사실상 쉬운 일이 아님을 알 수 있다. 다음 절에서는 먼저 하나의 정형 (canonical form) 으로 변화시킬 언명에 대해 적용하여 복잡성을 줄이는 비교 흡수 방법 (resolution) 이라 불리는 증명 과정을 다루었다.

4. 비교 흡수 방법 (Resolution)

앞 절에서 언급한 것처럼, 서술 논리에서 언명들을 추론할 때 관계되는 많은 과정을 하나의 과정으로 수행하는 증명 과정이 존재한다면, 계산면에서 볼 때 이것은 매우 유용하게 사용될 것이다. 비교 흡수 방법은 이 조건을 만족하는 증명 과정으로써 아래 설명할 매우 편리한 형태로 변환된 언명에 대해 작용하기 때문에 효과적이다.

비교 흡수 과정은 부정 (refutation) 에 의해 증명을 수행한다. 다시 말하면 언명을 증명하기 위해 이 언명을 부정하고, 이로부터 얻어진 언명이 이미 알려진 언명과 모순된다. 이 방법은 증명을 위해 증명될 정리로부터 공리로 후진 추론하던 지금까지의 기법들과 대조를 이룬다. 이 기법을 자세히 설명하기에 앞서, 먼저 언명을 표준형 (standard form) 으로 표기하는 방법에 대해 알아 보자.

(1) 절의 형태 (Clause Form) 로 변환

마커스를 알고 있는 모든 로마인은 시이저를 미워하는 사람이거나 혹은 누군가를 미워하는 사람들을 미친 사람으로 간주하는 사람이라고 가정하자. 이 사실을 wff 로 표기하면 다음과 같다 :

    ∀x [Roman(x) ∧ know(x, Marcus)]
                           → [hate(x, Caesar) ∨ (∀y (∃z hate(y, z))
                               → thinkcrazy(x, y))]

이 공식을 증명에 사용할 때 매우 복잡한 일치 과정이 필요하다. thinkcrazy (x, y) 와 같은 부분이 일치되었다고 할 때, 이 일치된 부분이 삽입되어 있는 부분과 삽입되어 있지 않는 부분을 포함하고 있는 공식의 나머지를 적절히 처리해야 한다. 만약 간단한 형태로 공식이 표현되었다면, 비교적 쉽게 이것을 처리할 수 있다. 다음과 같은 상황이라면 공식을 쉽게 처리할 수 있다 :

논리곱의 정규형 (conjunctive normal form) 은 이 성질을 모두 가지고 있다. 예를 들어, 위에 주어진 사실을 논리곱의 정규형으로 표기하면 다음과 같다 :

    ~Roman(x) ∨ ~know(x, Marcus) ∨ hate(x, Caesar) ∨ ~hate(y, z) ∨ thinkcrazy(x, z)

wff 를 논리곱의 정규형으로 변환시키는 알고리즘이 있기 때문에, 이 형태로 바뀐 wff 에만 적용하는 증명 과정 (예, 비교 흡수 방법) 을 사용해도 일반성은 상실되지 않는다.

wff 를 논리곱의 정규형으로 변환시키기 위해, 다음과 같은 일련의 단계를 수행한다 :

    1. a → b 와 ~a ∨ b 가 동치라는 사실을 이용하여, → 을 제거한다. 위에 주어진 wff 를 이것으로 변환시키면 다음과 같다 :

            ∀x ~[Roman(x) ∧ know(x, Marcus)]
            ∨ [hate(x, Caesar) ∨ (∀y ~(∃z hate(y, z))
                    ∨ thinkcrazy(x, y))]

    2. ~(~p) = p 와 ~∀xp(x) = ∃x~p(x) 와 ~∃xp(x) = ∀x~p(x) 라는 사실을 이용하여 ~ 의 범위를 축소한다. 단계 1 로부터 얻은 wff 에 이 전이를 수행하면

            ∀x[~Roman(x) ∨ ~know(x, Marcus)]
            ∨ [hate(x, Caesar) ∨ (∀y∀z ~hate(y, z)
                     ∨ thinkcrazy(x, y))]

        를 얻게 된다.

    3. 각 한정사가 균일한 변수와 결합되도록 변수를 표준화한다. 변수는 가상 이름이기 때문에, 이 과정이 wff 의 진리값에 영향을 미치지 않는다. 예를 들어, 다음 공식

            ∀xP(x) ∨ ∀xQ(x)

        는

            ∀xP(x) ∨ ∀yQ(y)

        로 바꿀 수 있다. 이 단계는 다음 단계의 준비 단계이다.

    4. 상대적 순서는 변화시키지 않고, 공식의 좌측에 표기된 한정사를 이동시킨다. 변수 이름 간에 어떤 충돌도 발생하지 않기 때문에 이것이 가능하다. 단계 2 에서 얻은 공식에 이 작업을 수행하면

            ∀x∀y∀z[~Roman(x) ∨ ~know(x, Marcus)]
            ∨ [hate(x, Caesar) ∨ (~hate(y, z)
                     ∨ thinkcrazy(x, y))]

        를 얻는다. 이렇게 얻은 공식을 프리넥스 정규형 (prenex normal form) 으로 표기되었다고 한다. 프리넥스 정규형은 한정사를 접두사로 하여 그 다음에 한정사에 영향을 받지 않는 모형이 뒤따라 나온다.

    5. 존재 한정 기호 (existential quantifier) 를 제거한다. 존재 한정 기호로 한정된 변수를 포함한 공식은 이 공식을 참으로 만드는 값이 존재함을 나타낸다. 원하는 값을 만드는 함수를 불러 변수에 대치시킴으로써, 한정사를 제거할 수 있다. 사실상 값을 만드는 방법은 알 필요가 없기 때문에, 모든 치환에 대해 새로운 함수 명칭을 사용해야 하며, 이때 단지 이런 함수가 존재하는지만 알면 된다. 예를 들어, 공식

            ∃y President(y)

        를

            President(S1)

        로 바꿀 수 있다. 여기서 s1 은 매개 변수가 없이 President 를 만족시키는 값을 만드는 함수이다.

        만약 존재 한정 기호가 전체 한정 기호 (universal quantifier) 의 범위 내에 발생한다면 서술형 명제를 만족시키는 값은 전체 한정 기호로 한정된 변수의 값에 의해 결정된다. 예를 들어, 공식

            ∀x∃y fatherof (y, x)

        에서, fatherof 를 만족시키는 y 의 값은 특정한 x 의 값에 의해 결정된다. 따라서 식에 포함된 전체 한정 기호의 수와 동일한 수의 매개 변수를 가진 함수를 만들어야만 한다. 따라서 이 예를 다음과 같이 바꿀 수 있다 :

            ∀x fatherof (S2(x), x)

        이렇게 만들어진 함수를 스콜램 함수 (Skolem function) 라 하며, 어떤 매개 변수도 가지고 있지 않은 스콜램 함수를 스콜램 상수 (Skolem constant) 라 한다.

    6. 접두사를 제거한다. 남아 있는 변수들은 전체 한정 기호로 한정된 변수들이기 때문에, 접두사를 생략할 수 있고, 사용될 어떤 증명 과정에서든지 공식에 나타난 변수가 전체 한정 기호로 한정된 변수라고 가정할 수 있다. 단계 4 에서 얻은 공식을

            ~Roman(x) ∨ ~know(x, Marcus) ∨ hate(x, Caesar)
           ∨ ~hate(y, z) ∨ thinkcrazy(x, y)

        를 얻는다. 그러나 배분 법칙 [(a ∧ b) ∨ c) = (a ∨ c) ∧ (b ∨ c)] 을 사용해야 할 경우가 있다. 예를 들어, 공식

            (winter ∧ wearingboots) ∨ (summer ∧ wearingsandals)

        를

            [winter ∨ (summer ∧ wearingsandals)]
           ∧ [wearingboots
               ∨ (summer ∧ wearingsandals)]

        로 바꿀 수 있다. 논리합으로 결합된 논리곱 인자가 포함되어 있기 때문에, 이를

            (winter ∨ summer)
       ∧ (winter ∨ wearingsandals)
       ∧ (wearingboots ∨ summer)
       ∧ (wearngboots ∨ wearingsandals)

        로 바꿀 수 있다.

    8. 각 논리곱 인자를 독립된 절 (clause) 이라 부른다. wff 가 참이기 위해서는, 이것으로부터 얻은 모든 절이 참이어야 한다. 만약 여러 개의 wff 들을 사용할 경우, 본래 wff 들에 의해 표기되었던 것과 동일한 사실들을 표기하기 위해 이들 각각으로부터 얻은 모든 절을 결합할 수 있다.

    9. 단계 8 로부터 얻은 절 속에 나타난 변수들을 표준화한다. 이렇게 함으로써 어떤 두 개의 절도 동일한 변수를 언급하지 못하도록 변수들을 명할 수 있다. 이를 위해

            (∀xP(x) ∧ Q(x)) = ∀xP(x) ∧ ∀xQ(x)

        라는 사실을 이용한다. 각 절이 독립적인 논리곱 인자이며, 변수들이 전체 한정 기호로 한정되었기 때문에, 비록 동일한 wff 로 얻어진 변수라 할지라도, 두 절의 변수들 간에 어떤 관계를 지을 필요는 없다.

비교 흡수 과정 동안 때때로 전체 한정 기호로 한정된 변수에 특정한 값을 치환할 필요가 있기 때문에, 표준화를 수행하는 마지막 단계가 중요한 의미를 가진다. 그러나 대부분의 경우, 가장 일반적인 형태로, 가능한 한 오랫동안 절을 유지시켜야 한다. 따라서 변수에 특정한 값을 치환할 때, 치환할 값의 최소값을 기억하여, 시스템의 진리값을 보존시켜야 한다.

wff 에 위의 전체 과정을 적용함으로써, 절을 알게 되는데, 각 절은 문자 (literal) 를 논리합으로 연결한 것이다. 이 절들은 비교 흡수 과정에 사용되어 증명을 만든다.

(2) 비교 흡수 과정의 기본 원리

비교 흡수 과정은 간단한 순환 과정으로써, 매 단계마다 부모절 (parent clause) 이라 불리는 두 개의 절을 비교하고, 이들로부터 새로운 절을 추론하는 것이다. 새로이 얻은 절은 두 개의 부모절이 서로 상호 작용하는 방법을 나타낸다. 다음 두 개의 절을 살펴 보자 :

    winter ∨ summer
    ~winter ∨ cold

이것은 두 절이 모두 참임을 의미한다. 언제나 winter 와 ~winter 중의 하나는 참이다. 만약 winter 가 참이라면, 두번째 절을 참으로 유지하기 위해서는, cold 가 참이어야 한다. 만약 ~winter 가 참이라면, 첫번째 절을 참으로 유지하기 위해, summer 가 참이어야 한다. 따라서, 이 두 개의 절로부터

    summer ∨ cold

를 추론할 수 있다. 이것은 비교 흡수 과정에 의해 만들어진 연역 추론이다. 비교 흡수 방법은 같은 문자 - 여기서는 winter - 를 포함하고 있는 두 개의 절을 택해 이것에 대해 작용한다. 문자는 반드시 한 절에서는 긍정의 형태로, 다른 한 절에선느 부정의 형태를 나타내야 한다. 제거되는 문자를 제외하고 두 개의 부모절에 나타난 모든 문자를 결합하여 하나의 비교 흡수절 (resolvent) 를 얻는다.

만약 얻어진 절이 어떤 문자도 가지고 있지 않는 절이라면, 모순이 발견된 것이다. 예를 들어, 두 개의 절

    winter
    ~winter

로부터 얻어지는 비교 흡수절에는 어떤 문자도 포함되어 있지 않다. 만약 모순이 존재한다면, 이 모순은 반드시 발견된다. 만약 어떤 모순도 존재하지 않는다면, 비록 이 사실을 탐지할 수 있는 방법이 있더라도, 앞의 과정이 무한히 계속될 가능성이 있다.

지금까지 명제 논리에서의 비교 흡수 방법에 대해 알아 보았다. 서술 논리에 있어서는, 변수에 치환될 값들의 모든 가능성을 고려해야 하기 때문에, 매우 복잡하다. 서술 논리의 비교 흡수 과정에 대한 이론적인 기본 원리는 허브란드의 정리 (Herbrand's theorem) 로써, 다음과 같은 것을 알려 준다 :

어떤 과정도 유한 시간 내에 무한 집합을 조사할 수 없기 때문에, 불만족성 (unsatisfiability) 을 증명하는 계산 가능한 어떤 과정이 존재해야 할 경우, 위 정리의 두번째 부분은 중요한 의미를 가진다. 체계적으로, 가능한 모든 치환 대상을 찾아 각각이 모순을 유도하는지 조사함으로써 모순을 찾을 수 있다는 것을 첫번째 사실로부터 알 수 있다. 그러나 이것은 매우 비효율적인 방법이다. 비교 흡수 방법의 원칙으로부터, 최소 수의 치환 대상을 찾아 조사함으로써 모순을 찾을 수 있다는 것을 첫번째 사실로부터 알 수 있다. 그러나 이것은 매우 비효율적인 방법이다. 비교 흡수 방법의 원칙으로부터, 최소 수의 치환 대상을 찾아 조사함으로써 모순을 찾을 수 있다. 가능한 한 오랫동안 절을 일반적인 형태로 유지하면서 필요에 따라 특정한 치환 대상을 찾아내는 것은 비교 흡수 방법의 중요한 기본 개념이다.

(3) 명제 논리에서의 비교 흡수 방법

비교 흡수 과정의 적용 방법을 명백히 하기 위해, 먼저 명제 논리에서의 비교 흡수 과정을 살펴 본 후, 이것을 서술 논리까지 확장시켜 알아 보자.

명제 논리에서, 공리의 집합 F 에 대해 명제 S 를 비교 흡수하여 증명을 얻는 과정은 다음과 같다 :

    1. F 의 모든 명제를 절의 형태를 변환한다.

    2. S 의 부정하고, 이것을 절의 형태를 변환한다. 단계 1 로부터 얻은 절의 집합에 이것을 첨가한다.

    3. 모순이 발견되거나, 어떤 진보도 만들어지지 않을 때까지 다음을 반복하라 :
1) 두 개의 절을 선택한다. 이것을 부모절이라 부른다.
2) 이들을 함께 비교 흡수한다. 비교 흡수절이라 불리는 새로이 얻은 절은 다음의 예외를 가지고 부모절에 포함된 모든 문자들을 논리합으로 결합한 것이다 : 만약 한 부모절이 L 을, 다른 한 부모절이 ~L 을 포함한 그런 L 과 ~L 의 쌍이 존재한다면, 비교 흡수절에서 L 과 ~L 을 모두 제거한다.
3) 비교 흡수절이 어떤 문자도 포함하지 않은 절이라면 모순이 발견된 것이다. 만약 그렇지 않다면, 이 과정에서 이용 가능한 절의 집합에 새로이 얻은 비교 흡수절을 첨가한다.

주어진 공리

절 형태로의 변환

 

      p

      (p ∧ q) → r

      (s ∨ t) → q

       

      t

      p

      ~p ∨ ~q ∨ r

      ~s ∨ q

      ~t ∨ q

      t

1.

2.

3.

4.

5.

그림 7

간단한 예를 살펴 보자. 그림 7 의 첫번째 행과 같은 공리가 주어졌을 때, r 을 증명하고자 한다. 먼저 그림의 두번째 행에 보여진 것처럼, 공리를 절의 형태로 변환시켜야 한다. 그 다음, 이미 절의 형태 속에 나타난 r 을 부정하여, ~r 을 얻은 후, 비교 흡수를 수행하기 위해 함께 사용될 절들의 쌍을 선택한다. 비록 절의 어느 쌍이라도 비교 흡수될 수 있지만, 이 문자 (complementary literal) 가 포함되어 있는 쌍을 이용하여, 어떤 문자도 포함되어 있지 않는 절을 유도할 가능성이 높은 비교 흡수절을 얻는다. 예를 들어, 그림 8 에 보여진 일련의 비교 흡수절을 얻을 수 있다. 절 ~r 은 찾고자 하는 모순과 관련된 절 중의 하나이다. 따라서 이 절을 비교 흡수 과정의 시작에 사용한다.

그림 8  명제 논리에서 비교 흡수 방법

비교 흡수 과정은 모두 참으로 가정된 절들의 집합을 사용하는 과정으로 볼 수 있다. 다른 절로부터 얻은 정보를 기초로 하여, 이 방법에 의해 새로운 절이 얻어진다. 새로이 얻은 절은 원래 있던 절들을 참으로 유지하기 위해 가해져야 할 제한 조건을 나타낸다. 절을 참으로 유지할 수 없을 만큼, 이 절이 제한을 받게 될 때, 모순이 발생한 것이다. 이것은 어떤 문자도 포함하지 않는 절을 얻음으로써 알 수 있다. 앞의 예를 사용하여 이것의 작용 방법에 대해 알아 보자. 명제 2 가 참으로 유지되기 위해서는, ~p, ~q 혹은 r 중의 하나가 참이어야 한다. 그러나 ~r 이 참이라고 가정했기 때문에 명제 2 를 참으로 유지하기 위해서는, ~p 나 ~q 가 참이어야 한다. 첫번째로 얻은 비교 흡수절은 이것을 나타낸다. 명제 1 은 p 가 참이라는 것, 즉 ~p 가 거짓이라는 것을 나타내기 때문에, 명제 2 를 참으로 유지하기 위해서는 ~t 나 q 가 참이어야 한다. 그러나 반드시 ~q 가 참이어야 하기 때문에, 명제 4 를 참으로 유지하기 위해서는 ~t 가 참이어야 한다 (이것은 세번째 비교 흡수절에 의해 표기되었다). 명제 5 는 t 가 참임을 나타낸다. 따라서 모든 절을 참으로 유지시킬 방법은 없다. 어떤 문자도 포함되어 있지 않은 절을 얻음으로써, 이 사실을 알 수 있다.

(4) 단일화 알고리즘 (Unification Algorithm)

명제 논리의 경우, 두 개의 문자가 동시에 참이 될 수 없다는 것은 쉽게 결정된다. 간단한 예로 L 과 ~L 을 살펴 보자. 서술 논리에서는 변수의 바인딩을 고려해야 하기 때문에 이 일치 과정이 더욱 복잡하다. 예를 들어 man (Henry) 와 man (Spot) 은 모순이 아니다. 그러나 man (Henry) 와 ~man (Henry) 는 모순이다. 모순을 결정하기 위해서는, 두 개의 문자를 비교하여 이것을 동일한 것으로 만들 수 있는 치환 대상이 존재하는지 결정하는 일치 과정이 필요하다. 단일화 알고리즘이라 불리는 순환 과정은 이를 위해 사용된다.

단일화의 기본 개념은 매우 간단하다. 각 문자를 리스트로 나타낸다. 이 리스트의 첫번째 원소는 서술형 명제의 이름이며, 나머지 원소는 매개 변수로써, 하나의 원소 (LISP 용어로는 원자 (atom)) 이거나, 혹은 또 다른 리스트일 수 있다. 예를 들면,

    (tryassassinate Marcus Caesar)
    (tryassassinate Marcus (rulerof Rome))

두 개의 문자가 서로 같은 것인지를 결정하기 위해, 먼저 첫번째 원소가 서로 같은지 조사한다. 만약 그렇다면 수행을 계속하고, 그렇지 않다면 나머지 매개 변수들과는 상관없이 이 두 문자가 서로 다른 것임을 알 수 있다. 예를 들어, 다음 두 개는 서로 같은 것이라고 말할 수 없다 :

    (tryassassinate Marcus Caesar)
    (hate Marcus Caesar)

만약 첫번째 원소가 일치된다면, 한 번에 한 쌍씩 나머지 원소들을 조사한다. 남아 있는 각 원소를 조사하기 위해, 단일화 과정을 순환적으로 사용한다. 일치 규칙은 단순하다. 상이한 상수, 함수 혹은 서술형 명제는 서로 완전히 똑같을 경우만 서로 일치되고, 그렇지 않으면 서로 일치되지 못한다. 변수는 다른 변수, 모든 상수, 함수 혹은 서술형 명제의 식과 일치할 수 있는데, 이 때 함수나 서술형 명제의 식에는 어떤 변수도 포함될 수 없다.

단일화 과정을 수행하기 위해, 전체 문자에 대해 하나의 모순도 없이 일관된 치환대상을 찾아야 한다. 이를 이해, 두 문자를 하나로 볼 수 있는지 조사하기에 앞서, 찾은 각 치환 대상을 문자의 나머지 부분에 적용해야 한다. 예를 들어, 다음 식이 단일화 될 수 있는지 살펴 보자 :

    (P x x)
    (P y z)

첫번째 p 는 일치한다. 다음 x 와 y 를 비교하여, x 를 y 로 치환하면, 이들이 서로 일치될 수 있는지 결정한다. 이러한 치환을

    y/x

로 표기한다 (물론, x 와 y 가 가상 변수이기 때문에, y 를 x 로 치환할 수 있다). 다음 단순히 x 와 z 를 일치시키려 한다면, 치환 z/x 를 얻는다. 그러나 x 의 치환으로 y 와 z 를 모두 대입시킬 수 없기 때문에, 일관된 치환을 얻을 수가 없다. 첫번째 치환 y/x 를 찾은 후, 문자의 남아 있는 부분인

    (y)

    (z)

에 대한 치환을 만들어야 한다. 치환 z/y 를 사용하여 두 문자의 단일화를 시도할 수 있다. 발견한 두 개의 치환을 합성하여, 전체 단일화 과정을 완료한다. 합성 치환은

    (z/y)(y/x)

로 표기된다. 일반적으로 치환 ()() 는 리스트의 가장 우측의 치환부터 적용하고, 치환을 모두 적용할 때까지, 얻은 결과에 계속적으로 다음 리스트의 치환을 적용한다.

두 개의 문자를 일치시키는 치환을 적어도 한 개 찾는 것이 단일화 과정의 목표이다. 대부분의 경우에 있어서, 이런 치환이 한 개 존재한다면, 이 치환 외에도 여러 개의 치환이 존재함을 알 수 있다. 예를 들어, 문자

    hate (x, y)
    hate (Marcus, z)

는 다음과 같은 치환 중의 하나를 사용함으로써, 단일화될 수 있다 :

    (Marcus/x, z/y)
    (Marcus/x, y/z)
    (Marcus/x, Caesar/y, Caesar/z)
    (Marcus/x, Polonius/y, Polonius/z)

처음 두 개는 어휘만 다를 뿐 서로 같은 것이다. 그러나 다음 두 개로부터는, 일치를 위해 필요한 것 이상의 제한이 가해진 치환이 만들어진다. 단일화 과정에서 얻어진 마지막 치환이 비교 흡수 과정에 사용되기 때문에, 가능한 한 가장 일반성을 지닌 단일화 기호 (the most general unifier) 를 만드는 것이 효율적이다. 아래 소개된 알고리즘은 이러한 조건을 만족시킨다.

앞에서 단일화 알고리즘의 작용에 대해 설명하였기 때문에, 이제 이것을 자세히 기술하려 한다. 일치 과정 동안 수행된 치환의 합성을 나타내는 리스트를 값으로 돌려주는 UNIFY (L1, L2) 를 살펴 보자. 어떤 원소도 포함하고 있지 않는 리스트인 NIL 은 일치가 발견되었음을 알려 준다. 하나의 값으로 구성된 리스트 F 는 단일화 과정이 실패하였음을 알린다.

        Unify (L1, L2)

    1. L1 이나 L2 가 원자 (atom) 이라면, 다음을 수행한다.
       1) 만약 L1 과 L2 가 서로 같은 것이라면, NIL 을 돌려 준다.
       2) 그렇지 않을 경우, L1 이 변수라면,

            1. L1 이 L2 에 나타난다면, F 를 돌려 준다.
               그렇지 않다면, (L2/L1) 을 돌려 준다.

        3) 그렇지 않을 경우, L2 가 변수라면,

            1. L2 가 L1 에 나타난다면, F 를 돌려 준다.
               그렇지 않다면, (L1/L2) 를 돌려 준다.

    2. 만약 Length(L1) 이 Length(L2) 와 같지 않다면, F 를 돌려 준다.

    3. SUBST 의 값으로 NIL 을 지정한다 (이 과정이 끝날 때, SUBST 는 L1 과 L2 를 단일화 하기 위해 사용된 모든 치환을 포함하고 있다).

    4. for i : = 1 to number of elements in L1 do
1) L1 의 첫번째 원소와 L2 의 i 번째 원소를 매개 변수로 하여 Unify 를 호출하고, 이로부터 얻은 결과를 S 에 넣는다.
2) 만약 S = F 이면, F 를 돌려 준다.
3) 만약 S 가 NIL 이 아니라면

            1. S 를 L1 과 L2 의 나머지 부분에 적용한다.
    2. SUBST : = APPEND (S, SUBST)

        return SUBST

주어진 변수를 포함하고 있는 식이 그 변수로는 단일화될 수 없다는 것을 확신할 방법이 위의 알고리즘에서는 논의되지 않았다. 다음 식의 단일화를 조사해 보자.

    (f x x)
    (f g(x) g(x))

만약 x 를 g(x) 로 치환한다면, 이 식이 나머지 부분에 나타난 x 를 g(x) 로 치환해야 할 것이다. 그러나, x 를 결코 제거할 수 없기 때문에, 이로 인해 알고리즘은 무한히 순환 반복될 것이다.

(5) 서술 논리에서의 비교 흡수 방법

지금까지 두 개의 문자가 하나로 일치되지 못하면, 서로 모순이라고 결정하는 방법에 대해 논의하였다. 예를 들어, man(x) 와 man(spot) 는 단일화될 수 있기 때문에, man(x) 와 ~man(spot) 는 서로 모순이다. 서술 논리에 비교 흡수 방법을 사용하기 위해, 단일화 알고리즘을 이용하여 상쇄될 문자의 쌍을 찾는다.

또한, 단일화 알고리즘으로부터 얻은 단일화 기호 (unifier) 를 사용하여 비교 흡수절을 만든다. 예를 들어, 다음 두 절을 비교 흡수한다고 하자 :

    1. man(Marcus)
    2. ~man(x1) ∨ mortal(x1)

치환 Marcus/x1 을 사용하여 문자 man(Marcus) 와 man(x1) 을 같은 하나로 볼 수 있으며, 이것은 x1 = Marcus 의 경우 ~man(Marcus) 가 거짓임을 의미한다. 그러나 명제 논리에서처럼 간단히 두 개의 문자 man 을 상쇄하여 mortal(x1) 을 얻을 수 있는 것은 아니다. 절 2 는 주어진 x1 에 대해 ~man(x1) 이거나 martal(x1) 임을 의미한다. 따라서 절 2 가 참으로 유지되기 위해서는, mortal(Marcus) 가 참이어야 한다. ~man(x1) 을 참으로 만들 수 있는 x1 이 존재하여 Mortal(x1) 의 진리값이 전체 절의 진리값에 영향을 미치지 못할 경우가 있기 때문에, 모든 x1 에 대해 mortal(x1) 참이어야 할 필요는 없다. 따라서 절 1 과 절 2 에 의해 얻어진 비교 흡수절은 mortal(Marcus) 이어야만 하는데, 이것은 단일화 과정의 결과를 비교 흡수절에 적용함으로써 얻는다. 여기서부터 비교 흡수 과정이 수행되어 mortal(Marcus) 가 이용 가능한 다른 절과 모순을 유도할지에 대해 조사한다.

이 예로부터, 식을 절의 형태로 변환시키는 과정 동안, 변수들을 표준화해야 하는 것이 얼마나 중요한지 알 수 있다. 일단 표준화가 행해지면, 치환을 수행하여 비교 흡수절을 얻기 위해 단일화 과정이 어떻게 사용되어야 하는가를 결정하는 것은 용이하다. 만약 동일 변수를 사용한 두 개의 예가 발생한다면, 이들을 치환하여 동일한 것으로 만든다.

주어진 문장의 집합을 F 로, 증명될 문장을 S 로 가정할 때, 서술 논리에서의 비교 흡수 과정 알고리즘은 다음에 따라 수행된다.

    1. F 의 모든 문장을 절의 형태로 변환한다.

    2. S 를 부정하고, 그 결과를 절의 형태로 변환하여 1 로부터 얻어진 절의 집합에 첨가하라.

    3. 모순이 발견되거나, 미리 정해진 양 만큼의 노력이 소모될 때까지 다음을 반복 수행한다 :
1) 두 개의 절을 선택하여, 부모절이라 부른다.
2) 이들을 함께 비교 흡수한다. 비교 흡수절은 다은 예외를 가지고, 적절히 치환된 양 부모절의 모든 문자를 논리합으로 결합하여 얻는다 : 단일화 기호 T1 과 T2 에 대해 T1 은 부모절 중의 하나에, T2 는 나머지 다른 부모절에 포함된 이런 T1 과 ~T2 의 쌍이 있을 때, T1 도 T2 도 비교 흡수절에 포함되지 못한다. T1 과 T2 를 보수 문자 (complementary literal) 라 한다. 단일화 과정으로부터 얻은 치환을 사용하여 비교 흡수절을 만든다.
3) 비교 흡수절이 어떤 문자도 포함하지 않는 절이라면, 모순이 발견된 것이다. 그렇지 않다면, 얻은 비교 흡수절을 이 과정의 이용 가능한 절의 집합에 첨가한다.

매 단계에서 함께 비교 흡수된 절을 어떤 체계적인 방법을 사용하여 선택한다면, 만약 모순이 존재할 경우, 비교 흡수 과정에 의해 이 모순을 찾을 수 있다. 그러나 이를 위해서는 긴 시간이 필요하다. 이 과정을 상당히 빨리 수행할 수 있는 선택 방법이 존재한다 :

마커스의 토론으로 되돌아와, 그에 대한 새로운 것을 증명하기 위해 비교 흡수 방법이 어떻게 사용되는지 알아 보자. 먼저 2 절에 소개된 문장의 집합을 살펴 보자. 비교 흡수 과정에서 이들을 사용하기 위해서는 4.1 절에 기술된 절의 형태로 이들을 변환시켜야 한다. 그림 9(a) 에는 변환의 결과가, 그림 9(b) 에는 문장의 비교 흡수에 의한 증명이 보여진다. 물론 그림에 보여진 것보다 더 많은 비교 흡수 절을 만들 수 있으나, 탐색을 위해 위에서 기술된 경험적 탐색 방법을 사용하여 비교 흡수절을 만들었다. 여기서 증명하고자 하는 문장으로부터 후진 추론하면서 모순을 얻어내는 것은 필수적으로 행해진다.

그림 9  비교 흡수 방법을 이용한 증명

문장

    hate(Marcus, Caesar)

를 증명할 때, 사실상 원하는 목표는 "Did Marcus hate Caesar?" (마커스는 시이저를 미워하였는가?) 라는 질문에 대한 답이라고 가정하자. 이 경우, 문장

    ~hate(Marcus, Caesar)

를 증명하면 된다. 이를 위해

    hate(Marcus, Caesar)

라는 문장을 이용 가능한 절의 집합에 첨가함으로써, 비교 흡수 과정의 수행을 시작할 수 있지만, 이 이용 가능한 절의 집합에는 ~hate 를 포함하고 있는 절이 존재하지 않음을 쉽게 알 수 있다. 비교 흡수 과정에서, 새로운 절은 이미 존재하고 있는 절에 포함된 문자들의 결합에 의해서만 얻어지기 때문에, 현재의 이용 가능한 절들로부터 ~hate 를 포함하고 있는 절은 결코 만들 수 없고 따라서

    hate(Marcus, Caesar)

는 이미 알려진 어느 문장과도 모순된 문장을 만들지 못한다. 이것은 비교 흡수 과정에서, 어떤 모순도 존재하지 않음이 탐지되는 상황의 예이다. 때때로, 이러한 상황은 증명의 시작에서가 아니라, 그림 9 에 주어진 공리를 토대로, 그림 10(a) 의 예에 보여진 것처럼, 증명이 수행 도중에 탐지된다.

그림 10  비교 흡수 방법에서 성공적이지 못한 시도

그러나 지식에 대한 데이터 베이스에 다음과 같은 두 개의 언명이 더 포함되어 있다고 가정하자 :

     (9) persecute(x, y) → hate(y, x)

    (10) hate (x, y) → persecute(y, x)

이것을 절의 형태로 변환하면 다음과 같다 :

     (9) ~persecute(x5, y2) ∨ hate(y2, x5)

    (10) ~hate(x6, y3) ∨ persecute(y3, x6)

이 언명을 사용하여, 그림 10(b) 에 보여진 것처럼 그림 10(a) 의 증명을 계속 수행할 수 있다. 이전에 만들어졌던 비교 흡수절이 다시 만들어질 때, 어떤 모순도 존재하지 않음을 알 수 있다.

그림 11 변수들을 표준화시켜야 하는 이유

공식의 집합을 절의 형태로 변환 과정의 첫번째 단계는 최후로 얻은 절에 나타난 변수들을 표준화하는 것이다. 비교 흡수 과정에 대해 논의해 오면서, 이 단계의 중요성을 알 수 있었다. 그림 11 은 변수의 표준화가 수행되지 않을 경우 발생할 어려운 상황의 예를 보여 준다. 절 1 과 절 2 에 모두 변수 y 가 사용되었기 때문에, 두번째 비교 흡수 단계의 치환이 수행되면, 매우 제한되어 결국 데이터 베이스 내에 존재하는 모순을 찾아낼 수 없는 절이 만들어진다. 그러나, 만약 절

    ~father(Chris, y)

가 만들어졌더라면, 절 4 로부터 모순을 발견할 수 있었을 것이다. 절 2 를

    ~mother(a, b) ∨ woman(a)

로 표기한다면, 이것이 가능하다.

기본적인 비교 흡수 과정의 수행에는, 절의 형태로 표기될 수 있는 지식이 모두 필요하다. 그러나 3 절에서 지적한 것처럼, 일부 정보를 계산 가능한 함수나 혹은 계산 가능한 서술형 명제와 동치 관계의 형태로 표기하는 것은 더욱 효과적이다. 비교 흡수 과정을 수정하고 향상시킴으로써, 이러한 종류의 정보를 차지하는 것은 어려운 일이 아니다. 그림 12 는 3 절에서 주어진 문장을 토대로, 문장

    ~alive(Marcus, now)

에 대한 비교 흡수 증명을 보여 준다. 새로운 절을 만들기 위해서, 비교 흡수 규칙뿐만 아니라, 두 가지 새로운 규칙이 사용된다

그림 12  동치 관계와 축소를 통한 비교 흡수 방법

(6) 여러 치환의 수행

비교 흡수 과정을 사용하여, 허브란드의 정리에 의해 제공된 가능한 모든 치환을 실제로 수행하지 않고, 부정에 의한 증명을 찾을 수 있다. 그러나, 항상 하나 이상의 치환이 불필요한 것은 아니다. 예를 들어 2 절에 주어진 문장 외에 다음과 같은 문장이 주어졌다고 가정하자 :

    hate(Marcus, Paulus)
    hate(Marcus, Julian)

마커스가 어떤 통치자를 미워한다는 것을 증명하고자 할 때, 그림 13(c) 에 보여진 모순을 발견하기에 앞서, 그림 13(a) 와 (b) 에 보여진 치환을 각각 수행할 수 있는 가능성이 있다. 때때로 많은 치환을 수행한 후에야 비로소 원하는 모순을 찾을 수 있을 경우가 있다.

그림 13  여러 치환의 시도

(7) 질문에 답하기

질문에 답하는 문제의 정리 증명 기법을 적용하는 것은 인공 지능의 초기에 실현되었다. 연역 추론 과정을 사용하여 공리로부터 정리를 유추하고, 이미 존재하는 사실로부터 새로운 사실 (답) 을 유추할 수 있기 때문에, 이것은 당연하다. 지금까지 "Is Marcus alive?" 와 같은 예-아니오 질문에 답하기 위해 비교 흡수 과정이 어떻게 사용되는지에 대해 논의하였다. 이 절에서는 "When did Marcus die?" (마커스는 언제 죽었는가?) 혹은 "Who tried to assassinate a ruler?" (누가 통치자를 암살하려 했는가?) 와 같은 공백 채우기 질문의 답을 찾기 위해 비교 흡수 과정이 어떻게 사용되는지에 대해 논의한다. 이러한 질문에 답하기 위해서는 질문에 주어진 항과 일치하는 이미 알려진 언명을 찾아, 이 동치 언명 중 질문에 의해 요구된 공백을 채울 수 있는 부분을 취해 응답으로 사용한다. 예를 들어 "When did Marcus die?" 라는 질문에 답하기 위해,

    died(Marcus, ??)

와 같은 형태의 절을 사용한다. 여기서 ?? 는 사실상 특정한 해로 채워져야 한다. 따라서, 언명

    died(Marcus, 79)

를 증명할 수 있기 때문에, 이 질문에 79 라고 답할 수 있다.

비교 흡수 과정을 사용하여, 필요한 언명을 찾아 이것에 대한 증명을 쉽게 얻을 수 있음이 판명되었다. "When did Marcus die?" 라는 질문을 계속 살펴 보자. 이 질문에 답하기 위해, 먼저 마커스가 죽었다는 것이 참이어야 한다. 따라서

    ∃t died(Marcus, t)

가 참이어야 한다. 첫 단계로 이것의 증명을 위해, 비교 흡수 과정을 사용하여

    ~∃t died(Marcus, t)

에 의해 모순이 발생된다는 것을 보여야 한다. 이 언명이 모순을 유도한다는 것이 어떤 의미를 가지는지에 대해 알아 보자. 이 언명은 다음과 같은 형태의

    ∀t died(Marcus, t)

라는 언명과 모순된다. 위 언명의 경우, 마커스가 수 차례 죽었다는 보고로서, 질문에 답하거나, 혹은 간단히 하나를 택해, 이것을 질문에 대한 답으로 사용할 수 있다. 또 다른 가능성은

    died(Marcus, date)

형태의 특정한 언명과 모순을 이끌 수 있다는 점이다. 모순을 만들 때 사용된 값은 모두 원하는 값이 될 수 있다.

비교 흡수 방법을 사용하여 원하는 문장을 찾는 방법이 그림 14(a) 에 보여진다. 출발 절을 향해 후진해 가는 연쇄적인 단일화를 사용하여, 질문에 대한 답을 유추할 수 있다. 모순을 찾는데 사용될 식에 새로운 어떤 식을 첨가함으로써, 이 마지막 단계의 수행을 생략할 수 있다. 바로 이 새로이 얻은 식이 참임을 증명하고자 하는 식이다 (즉, 이것은 비교 흡수 과정에서 실제로 사용된 식을 부정한 것이다). 이 식에 특정한 표시를 하여 비교 흡수 과정의 수행을 원활하게 한다 (그림 14 에서는 밑줄로 표시하였다). 단일화가 수행될 때마다 이 새로운 가상 식의 변수들은 마치 실제로 사용되고 있는 절의 변수들처럼 제한을 받는다. 비교 흡수 과정의 최종 수행 단계에서는 NIL 절이 아니라 가상 식이 남는다. 이 때 변수에 대입된 값이 질문에 대한 원하는 답이다. 그림 14(b) 는 이 과정을 사용하여 질문에 답하는 방법을 보여 준다.

그림 14  비교 흡수 방법을 사용한 답 추출

그러나, 시스템의 사실을 표현하기 위해 특정한 표기법이 주어졌을 경우, 이 기법을 사용하면, 답을 찾을 수 없는 질문들이 존재한다. 예를 들어, 3 절에 주어진 문장을 사용하여 "What happened in 79 A.D.?" (A.D. 79 년에 어떤 일이 발생하였는가?) 라는 질문에 대한 답을 찾고자 한다. 이 질문에 답하기 위해, 79 년에 발생한 사건이 존재함을 증명해야 하기 때문에,

    ∃x event(x, 79)

를 증명하여, x 의 값을 찾아야 한다. 그러나 [event(x, y)] 형태의 어떤 문장도 주어지질 않는다.

그러나, 다른 표기법을 사용하여 사실을 표현한다면, 이 질문에 대한 답을 찾을 수 있다.

    erupted(volcano, 79)

대신,

    event(erupted(volcano), 79)

로 표기할 수 있다. 그림 15 에 보여진 간단한 증명으로 질문에 대한 답을 찾을 수 있다.

그림 15  새로운 표현의 사용

이 새로운 표기법은 이 전의 표기법보다 더 복잡하다는 결점을 가지고 있다. 또한 이 표기법을 사용한다고 해서, 생각할 수 있는 모든 질문에 대한 답을 항상 찾을 수 있는 것도 아니다. 일반적으로 요구될 질문의 종류를 결정하고, 이 질문을 위해 사용될 적절한 표기법을 작성해야 한다.

물론, 질문의 유형으로 예-아니오와 공백 채우기 질문만 존재하는 것은 아니다. 예를 들어, 어떤 일을 하고자 할 때 이 일을 수행하기 위한 방법을 질문할 수도 있다. 따라서 항상 가능한 모든 형태의 질문에 대한 완전한 답을 찾을 수 있는 것은 아니다. 이 후의 장에서는 다양한 종류의 질문에 대한 답을 찾기 위해 사용될 여러 방법들이 다루어진다.

5. 연역법 (Natural Deduction)

앞 절에서는 비교 흡수 과정을, 사용될 문장을 균일하게 표기함으로써 쉽게 구현할 수 있는 증명 과정으로 설명하였다. 그러나, 이 견해에서는 균일성을 위해 모든 것을 동일한 것으로 보았기 때문에, 특정한 문제의 풀이를 가장 효과적으로 찾을 수 있는 언명을 쉽게 선택할 수 없는 결점이 있다. 모든 것을 절의 형태로 변환하여 표기할 때 원래 표기된 사실에 포함되어 있는 귀중한 경험적 정보는 대부분 손실된다. 예를 들어 정직한 판사는 모두 충분한 교육을 받았다는 사실이 주어졌다고 가정할 때, 이것을 다음과 같이 표기할 수 있다 :

    ∀x judge(x) ∧ ~crooked(x) → educated(x)

이 표기된 언명으로부터, 어떤 사람이 교육을 받았다는 것을 연역 추론할 수 있다. 그러나, 위 언명을 다음과 같은 절의 형태

    ~judge(x) ∨ crooked(x) ∨ educated(x)

로 변환시키면, 이것은 정직하지만 교육을 받지 않았다는 것을 보임으로써, 어떤 사람이 판사가 아니라는 것을 연역 추론하는 것처럼 보인다. 물론 논리적 의미로 볼 때 이것은 사실이다. 그러나 이것은 어떤 사람이 판사가 아니라는 것을 보이기에는 매우 부적합한 방법이다. 원래의 언명에 포함되어 있던 경험적 정보가 이 변환으로 인해 손실되었다.

정리 증명 시스템의 기본으로 비교 흡수 방법을 사용할 때 수반되는 또 다른 문제는 인간의 사고 과정이 비교 흡수 방법에 따라 행해지지 않는다는 점이다. 따라서 비교 흡수 과정을 사용한 정리 증명 과정으로부터 충고를 받거나, 혹은 이 정리 증명 과정에 충고를 주고자 할 때, 인간과 정리 증명 과정이 서로 상호 작용하기란 매우 어려운 일이다. 상당히 어려운 문제에 대한 증명을 수행하기 위해 컴퓨터를 사용하는 것은 아직 미숙한 단계이기 때문에 실질적인 면에서 볼 때, 이러한 상호 작용이 가능하다는 것은 매우 중요한 역할을 한다. 이를 쉽게 하기 위해 컴퓨터의 증명 수행 과정을 가능한 한, 인간의 증명 수행 과정과 유사해지도록 한다. 연역법이 이를 위해 사용된다.

연역법은 정확한 용어라기보다는 어떤 한 가지 방법만으로는 풀 수 없는 문제를 풀기 위해 여러 기법을 결합 사용한 혼합물로서 설명된다. 일반적인 한 가지 기법을 지금까지처럼 서술형 명제에 따라 지식을 배열하는 것이 아니라, 서술형 명제 내에 포함된 물체에 따라 지식을 배열하는 방법이다. 제 7 장에서, 이를 위한 여러 기법들이 다루어진다. 또 다른 기법은 논리적 내포 (logical implication) 를 기술할 뿐만 아니라, 증명 과정에서 이 내포를 사용할 수 있는 방법을 알려 주는 재표기 규칙 (rewrite rule) 의 집합을 사용하는 것이다.

6. 요약

이 장에서는 지식 표기법을 위한 기법의 토대로 서술 논리를 사용하는 방법을 설명하였다. 또한, 지식을 이 방법으로 표기할 때 적용할 수 있는 문제 풀이 기법인 비교 흡수 방법을 설명하였다. 비교 흡수 과정은 정리가 아닌 것을 증명하고자 할 때, 긑나지 않을 수 있다. 그러나, 증명이 존재한다면 모순을 찾아 증명을 끝낼 수 있다고 보장할 수 있는가? 이것을 완전성 문제 (completeness problem) 라고 한다. 알고리즘을 소개한 형태에서 이 질문에 대한 답은 '아니오' 이다. 완전성을 보장하기 위해서는 약간의 수정이 필요한데, 이것은 대체로 정리 증명 시스템에서는 구현되지 않는다. 그러나 계산적인 측면에서 볼 때 완전성은 중요하지 않다. 대신 허용된 시간 내에 증명을 찾을 수 있는 적합한 경험적 방법이 존재하는지의 여부가 더 중요하다.

인공 지능 분야에 정리 증명을 시도할 때 수반되는 두번째 난점은 일부 정보는 서술 논리로 쉽게 나타낼 수 없다는 것이다. 이에 대한 예가 다음 장의 서두에 소개된다. 즉 이 장에서 소개된 방법은 일부 분야에서는 상당히 유용하지만, 모든 인공 지능 문제의 풀이를 찾는 데는 부적합하다.

7. 연습문제

1. 3 절에서 주어진 사실에 대해

        ~alive(Marcus, now)

    가 두 가지 방법에 의해 증명되는 것을 보았다. 그림 12 에서 이 두 가지 방법 중의 하나에 대응하는 비교 흡수 과정에 의한 증명이 보여졌다. 비교 흡수 과정을 사용하여 언명의 또 다른 증명을 추론하라.

2. 항들의 다음 각 쌍에 대해 단일화 알고리즘이 어떻게 작용하는지 조사하라 :

   a. (f Marcus) (f Caesar)
b. (f x) (f g(y))
c. (f Marcus(g x y)) (f x(g(Caesar Marcus))

3. 다음 문장에 대해

        John likes all kinds of food.
    Apples are food.
    Chicken is food.
    Anything anyone eats and isn't killed by is food.
    Bill eats peanuts and is still alive.
    Sue eats everything Bill eats.

    a. 위 문장들을 서술 논리의 형식으로 고쳐라.
b. 이 형식으로 표기된 언명을 절의 형태로 변환하라.
c. 비교 흡수 과정을 사용하여, 존이 땅콩을 좋아한다는 것을 증명하라.
d. "What food does Sue eat? (수는 어떤 음식을 먹는가?)" 를 비교 흡수 과정을 사용하여 답하라.

4. 다음 사실에 대해

       The members of the Elm St. Bridge Club are Joe, Sally, Bill and Ellen.
   Joe is married to Sally.
   Bill is Ellen's brother.
   The spouse of every married person in the club is also in the club.
   The last meeting of the club was at Joe's house.

    a. 서술 논리로 이 사실을 표기하라.
b. 위에 주어진 사실로부터 다음 언명의 진리값을 결정 할 수 있다.

위에 주어진 다섯 가지 사실로부터 이 언명 각각에 대한 진리값을 나타내는 비교 흡수 증명을 찾을 수 있는가? 만약 가능하다면 찾아라. 그렇지 않다면, 필요한 사실을 첨가하여 증명을 찾아라.

6. 4.7 절에서 비교 흡수 방법을 사용하여 "When did Marcus die?" 에 대한 답을 찾아 마커스가 죽었던 때가 있음을 보였다. 그림 4 에 주어진 사실에

        ∀x∀t1 dead (x, t1) → ∃t2 gt(t1, t2) ∧ died(x, t2)

    라는 사실을 첨가함으로써, 다른 방법으로 이 질문에 대한 답을 찾을 수 있다.

    a. 다른 추론의 연쇄를 사용하여 비교 흡수 증명을 하라.
b. "When did Marcus die?" 라는 질문에 대해 이 증명은 어떤 답을 주는가?

8. 다음 사실이 주어졌다고 가정하자 :

        ∀x, y, z gt(x, y) ∧ gt(y, z) → gt(x, z)
    ∀a, b succ(a, b) → gt(a, b)
    ∀x ~gt(x, x)

    이 때,

        gt(5, 2)

    를 증명하려 한다. 다음 비교 흡수 증명을 살펴 보자.

 

    a. 무엇이 잘못되었는가?
b. 이러한 것의 발생을 막기 위해 어떤 것을 비교 흡수 과정에 첨가해야 하는가?

9. 앞 문제에 대한 답으로 x 와 f(x) 를 함께 단일화하는 것의 방지를 위해 조사하는 과정을 생략해서  단일화 과정을 단순화할 수 있음을 알 수 있다. 이것은 어떤 두 절도 변수를 공유할 수 없기 때문에 가능하다. 만약 x 가 한 절에 나타난다면 f(x) 는 다른 절에 나타날 수 없다. 단일화 과정에 다음 두 절이 주어졌다고 가정하자 :

        (p x f(x))
    (p f(a) a)

    이 과정의 수행을 조사하라.

10. 다음 삼단 논법에 발생한 잘못은 무엇인가?

       Men are widely distributed over the earth.
   Socrates is a man.
   Therefore, Socrates is widely distributed over the earth.

    이러한 문제의 발생을 막기 위해 어떤 방법으로 사실을 표기해야 하는가?

11. 다음과 같은 언명을 서술 논리로 표기하고자 한다면 어떠한 문제가 발생하는가? 여기서는 마지막 언명을 다른 언명으로부터 추론할 수 있다 :

       John only likes seeing French movies.
   It is safe to assume a movie is American unless explicifly told otherwise.
   People don't to things that will cause them to be in situations that they don't like.
   John does not go to the Playhouse very often.