논 리

전문가 시스템 원리와 개발 : 이재규, 최형림, 김현수, 서민수, 주석진, 지원철 공저, 법영사, 1996, Page 210~228

1. 서 론

2. 명제계산(Propositional calculus)

3. 술어계산 (Predicate calculus)

    (1) 술어부호

    (2) 연결사

    (3) 정량자

    (4) 판명문의 진위값

    (5) 추론 규칙

    (6) 단일화(Unification)

4. 도출법 (Resolution)

    (1) 절(Clause) 집합으로의 변환

    (2) 변수가 없는 문장에 대한 도출법

    (3) 일반적인 절에 관한 도출법

    (4) 모순도출법

1. 서 론

논리는 인공지능 분야에서 가장 기본적인 지식 표현 및 추론을 위한 방법으로 이용되어 왔으며, 특히 유럽과 일본에서 인공지능 연구의 주안점이 되어 왔다. 논리는 기존의 지식으로부터 새로운 지식을 추출하기 위해 수학적 연역법을 이용함으로써, 지식 표현과 추론에 이론적인 기초를 제공하고 있다. 이미 참이라고 알려져 있는 사실로부터 새로운 사실을 유도함으로써, 새로운 사실 또한 참이라는 것을 증명하는 방법을 통해 질문에 대한 대답이나 문제에 대한 해를 유도할 수 있게 된다. 인공지능에서 주로 이용되는 논리는 명제계산 (Propositional Calculus) 및 술어계산 (Predicate Calculus) 으로서 지식 표현 방법이 간단하면서도 강력한 추론방법을 제공하는 수단이 되고 있다. 술어계산을 위한 인공지능 언어인 PROLOG 를 통해 실제 문제해결에도 이용되고 있다. 명제계산 및 술어계산이라는 용어 대신에 명제논리 및 술어논리라는 용어도 함께 사용되는데, 여기서는 보다 형식적인 형태를 강조하는 의미로 계산이라는 용어를 이용하고 있다. 명제계산 및 술어계산과 관련한 제반 용어, 추론 규칙 및 추론 과정을 상세히 알아보도록 하자.

2. 명제계산(Propositional calculus)

참이나 거짓을 판단할 수 있는 문장을 명제 (Proposition) 라 하며, 이를 부호로 나타낸 것을 ,명제부호라 한다. 예를 들어, "물은 상온에서 액체다"라는 문장은 명제이며, A라는 명제부호로서 이 문장을 표현할 수 있다. 참이나 거짓 그 자체는 진위부호라고 하며, 문장을 연결하는 부호를 연결사라 한다. 연결사로는 ∨, ∧, ¬, =>, = 가 있다. 명제계산에서 처리할 수 있도록 정의되어 있는 문장을 판명문 (Well Formed Formula) 이라 한다. 판명문은 명제부호, 진위부호 및 연결사로만 정의된 문장으로서 어떤 사실을 표현하기 위함이다. 판명문에서 이용할 수 있는 명제계산 문장을 다음과 같이 정의할 수 있다.

어떤 한 판명문이 주어졌을 때, 이 문장이 참인지 또는 거짓인지를 평가하는 것을 해석 (Interpretation) 이라고 한다. 명제계산의 기본적인 문장해석은 다음과 같다.

여러 명제계산 문장이 연결사로 연결되어 있는 복합 문장의 해석은 진위표 (Truth Table) 를 이용하면 명료하게 나타낼 수 있다. 일례로 A=>B 라는 암시 문장은 ¬A ∨ B 의 OR 결합문장과 같은 진위값을 갖게 되는데, <그림 1> 과 같은 진위표를 이용하여 두 문장의 해석이 같음을 알 수 있다.

A	B	¬A	¬A ∨ B
T	T	F	T
T	F	F	F
F	T	T	T
F	F	T	T

 <그림 1> ¬A ∨ B 문장의 진위표

어떤 한 판명문을 모든 해석하에서도 같은 진위값을 갖는 다른 모양의 판명문 형태로 변환할 수 있다. 이러한 변환은 논리적 추론을 수행하는데 매우 유용하게 이용될 수 있다. 부정부호와 연결사의 결합으로 인해 다음 문장들은 각각의 동일한 문장으로 변환될 수 있다. 괄호부호 (,)는 문장을 묶어 주는 역할을 하는 것으로 문장의 진위값과는 관련이 없다.

        ¬(¬A) = A
        A => B = (¬A ∨ B)
        de Morgan 법칙 : ¬(A ∨ B) = (¬A ∧ ¬B)
                                  ¬(A ∧ B) = (¬A ∨ ¬B)
        분  배  법  칙 : A ∨ (B ∧ C) = (A ∨ B) ∧ (A ∨ C)
                              A ∧ (B ∨ C) = (A ∧ B) ∨ (A ∧ C)
        교  환  법  칙 : (A ∧ B) = (B ∧ A)
                              (A ∨ B) = (B ∨ A)
        결  합  법  칙 : (A ∧ B) ∧ C = A ∧ (B ∧ C)
                              (A ∨ B) ∨ C = A ∨ (B ∨ C)
        대  치  법  칙 : A => B = (¬B => ¬A)

3. 술어계산 (Predicate calculus)

명제계산은 간단한 문제영역에서의 표현 언어로서는 문제가 없으나, 많은 문장을 효과적으로 표현하기 위한 수단으로서는 부족하다는 단점이 있다. 또한 명제계산 문장 내의 각 성분들ㅇ르 분리하여 이용할 수 있는 바업이 없다. 예를 들어 다음 두 명제계산 문장을 살펴보자.

        "모든 사람은 생명의 존엄성을 갖고 있다"
        "철수는 사람이다"

명제계산에서는 이러한 문장들로부터 "철수는 생명의 존엄성을 갖고 있다"라는 문장을 유도할 수가 없다. 이는 명제계산에서는 표현상의 제약으로 인해 문장 내의 각 성분을 분리하여, 다른 문장의 성분과 조합하여 이용할 수 없기 때문이다. 이러한 단점을 보완한 논리언어가 술어계산이다. 술어계산에서는 사물들의 관계를 나타내기 위해 술어부호라는 것을 이용하기 때문에 문장의 각 성분을 자유로이 분리하여 사용할 수 있으며, 변수를 이용하여 불특정 다수의 개념 또한 도입할 수 있다. 이처럼 명제계산의 단점을 극복한 논리언어인 술어계산의 문법과 논리적 추론 과정을 상세히 알아보도록 하자.

(1) 술어부호

술어계산 언어는 술어부호 및 항(Term)을 기본 구성 요소로 한다. 술어부호는 사물들의 관계를 표현하기 위해 사요오디는 부호이다. 항은 변수부호, 함수 부호, 상수부호로서 이루어진다.
   예를 들어, "세익스피어가 햄릿을 썼다"라는 문장을 술어계산에서는 다음과 같이 표현할 수 있다.

        write(Shakespear, Hamlet)

이 문장은 술어계산 언어로 이루어져 있는데, write는 술어부호이며, Shakespear, Hamlet은 상수부호이다. 만일 세익스피어가 쓴 모든 작품을 나타내고자 한다면 다음과 같이 표현할 수 있다.

        ∀x (write(Shakespear, x)

이 문장에서 x는 변수부호로서 세익스피어가 쓴 작품을 나타내며, ∀는 전체정량자로서 모든 x를 의미한다. 변수부호를 이용하지 않으면 술어계산은 명제계산과 같게 된다.
항의 또 다른 요소인 함수부호를 알아보도록 하자. 어떤 한 실체와 다른 실체간의 지정된 관계를 나타내기 위하여 함수부호를 이용하게 된다. 예를 들면, 어떤 사람의 아버지를 나타내는 관계라면, 항상 그 사람과 아버지의 관계는 1대 1의 관계가 된다. 함수부호로서 다음과 같이 표현할 수 있다.

        father(A), father(B)

이처럼 정해진 개수의 인자를 가지면서, 인자간의 관계를 매핑(Mapping)하는 역할을 하는 것이 함수부호이다.

술어부호와 항으로 구성된 문장을 기본 문장(Atomic Sentence or Formula)이라고 하며, 술어계산의 문법에 부합되는 문장을 판명문이라 한다. 기본 문장은 판명문이 되며, 여러 기본 문장이 연결사 등으로 복합구성된 문장 또한 판명문이 된다.
술어계산 언어의 각 구성요소와 실제 문제의 대상 영역(Domain)에서의 실체와 실체간의 관계, 함수간의 관련성을 연관시키는 것을 해석(Interpretation)이라고 한다. 각 술어부호에는 문제 대상 영역에서의 관계가 대응되며, 각 상수부호에는 대상 영역에의 실체가 대응된다. 또한 함수부호는 문제 대상 영역에서의 함수를 나타내게 된다. 그러므로 술어문장에 대한 해석이 완료되면, 우리는 술어계산의 각 문장이 실제 문장의 어떤 상황이나 사실을 나타내고자 하는 것인가를 파악하게 되며, 따라서 술어문장의 참이나 거짓을 판명할 수 있다. 예를 들면, write(Shakespear, Hamlet) 문장에서 write 술어부호를 통해 Shakespear가 Hamlet을 썼다는 관계가 설정되는 것을 알 수 있으며, 이러한 실체간의 관계 해석을 통해 이 문장의 진위 여부를 평가할 수 있게 된다.

(2) 연결사

기본 문장에 연결사를 이용하여 보다 복잡한 문장을 만들 수 있는데 이러한 복합 문장 또한 판명문이 된다. 술어계산에서 이용되는 연결사로는 ∨, ∧, ¬, =>, = 로서 명제계신에서의 연결사와 같은 의미와 용법을 갖게 된다. 기본 문장과 기본 문장의 부정(¬)으로만 이루어진 문장을 논리구(Literal)라고 하는데, 술어계산의 추론 과정에서 유용하게 이용되는 판명문의 형태이다.

(3) 정량자

문장의 변수부분에 적용되어 그 변수의 적용범위를 나타내는 역할을 하는 것이 정량자로서, 전체정량자 ∀와 존재정량자 의 두 가지가 있다. 정량자의 적용범위는 정량자를 뒤따르는 문장이 된다. 이를 명확히 나타내기 위하여 괄호를 이용한다. 예를 들어, "모든 코끼리는 회색이다"는 문장을 술어언어로 표현하면 다음과 같다.

        (∀x) (elephant(x) => color(x, Gray))

   정량자를 갖는 문장의 진위값 평가를 알아보도록 하자. ∀x (P(x))라는 문장의 진위를 평가하고자 한다면, 문제의 대상 영역에 있는 모든 x에 대해 P(x)가 T값을 가질 때 이 문장은 T가 된다. 마찬가지로 x (P(x))라는 문장을 평가하는 경우에는, 문제의 대상 영역에서 최소한 한 개의 x에 대해 P(x)가 T값을 가질 때 이 문장은 T가 된다. 대상문제의 성격에 따라서는 정량자가 문장에 이용될 경우, 그 문장의 진위값을 평가하는 것이 항상 가능한 것은 아니다. 예를 들어, ∀x (P(x)) 문장에서 x변수에 대응하는 실체가 문제의 대상 영역에서 무한히 존재하는 경우에는, 이 문장의 진위값을 평가하기 위해서는 무한한 시간이 필요하게 되므로 유한시간 내에 결론을 얻을 수 없게 된다.

   정량자를 갖는 변수를 제한변수(Bound Variable)라고 하며, 정량자를 갖지 않는 변수를 자유변수(Free Variable)라고 한다. 판명문에 있는 모든 변수가 제한변수인 판명문을 제한판명문이라고 한다.
   술어계산에서 정량자가 변수부호에만 적용되고, 술어부호나 함수부호에 대해서는 정량자를 허용하지 않는 경우 이를 일차 술어계산(First Order Predicate Calculus)이라고 한다. 예를 들어, (∀P) P(x) 문장은 술어부호 P에 정량자가 적용되므로 일차 술어계산에서는 허용되지 ㅇ낳는 문장이다. 대부분의 모든 논리적인 표현은 일차 술어계산으로 모두 나타낼 수 있으므로, PROLOG와 같은 인공지능 언어들은 일차 술어계산에 근거하고 있다.

(4) 판명문의 진위값

술어계산 문장의 참, 거짓을 판명함으로써, 두 개의 판명문이 동일한지 여부를 평가할 수 있다. 기본적인 판명문의 진위값은 명제계산과 동일한 방식으로 해석될 수 있으나, 명제계산에서 적용되지 않는 정량자가 이용되는 경우에는 다음과 같은 관계가 설정된다.

        ¬(x)P(x) = (∀x)(¬P(x)) 

        ¬(∀x)P(x) = (x)(¬P(x))

        (x)(P(x) ∨ Q(x)) = (x)P(x) ∨ (y)Q(y)

        (∀x)(P(x) ∧ Q(x)) = (∀x)P(x) ∧ (∀y)Q(y)

        (∀x)P(x) = (∀y)P(y)

        (x)P(x) = (y)P(y)

(5) 추론 규칙

기존의 판명문으로부터 새로운 판명문을 생성하는 과정을 추론 규칙이라고 한다. 추론 규칙에 의해 새로 생성된 판명문이 기존의 판명문 집합과 논리적인 모순이 없어야만, 우리는 그 추론 규칙을 논리계산에서 이용할 수 있다. 이러한 추론 규칙을 위해서 다음과 같은 개념들을 정의해 보자.

   어떤 특정한 해석 I가 판명문 집합 S의 모든 판명문에 대해 T값을 부여할 때, 이 '해석 I는 판명문 집합 S를 만족한다' 라고 말한다.
   예를 들어, 판명문 집합 S={ (∀x)P(x), (∀y)P(y) }가 있다고 가정하자. 판명문 집합 S에 대하여 특정한 x, y값을 부여하는 것이 하나의 해석이 되며, 이때 S의 두 문장이 모두 참이 된다면 이 해석은 판명문 집합 S를 만족하게 된다. 그러므로 판명문 집합 S를 만족시키는 해석은 대상문제의 성격에 따라서는 무수히 많을 수도 있다.
   만일 판명문 집합 S를 만족하는 모든 해석이 판명문 X 또한 만족한다면, 판명문 X는 판명문 집합 S로부터 논리적으로 유도된다(Logically Follows)라고 말한다. 예를 들어, P(A)는 (∀x) P(x)로부터 논리적으로 유도된다라고 말할 수 있다. 또한 (∀x)(∀y) (P(x) ∨ Q(y))는 { (∀x)(∀y) (P(x) ∨ Q(y)), (∀z) (R(z) ∨ Q(A)) } 집합으로부터 논리적으로 유도된다라고 말할 수 있다.
   어떤 판명문이 다른 판명문의 집합으로부터 논리적으로 유도되었다는 것이 반드시 그 판명문 집합으로부터 추론 규칙을 이용하여 생성되었다는 것을 의미하는 것은 아니다. 그러므로 추론 규칙을 이용하려 한다면, 추론 규칙에 의해 생성된 문장이 기존의 문장으로부터 논리적으로 유도되는지를 평가하는 것이 중요하게 된다.

   어떤 추론 규칙이 있을 때, 판명문 집합 S로부터 이 추론 규칙에 의해 생성된 모든 판명문이 또한 S로부터 논리적으로 유도될 수 있을 때, 우리는 이 추론 규칙을 정당(Sound)하다고 한다.

   어떤 추론 규칙이 주어진 판명문 집합 S에 대해서 논리적으로 유도될 수 있는 모든 판명문ㅇ르 생성할 수 있다면, 이 추론 규칙은 완전(Complete)하다고 한다. 대부분의 경우 설사 완전하지는 않더라도 정당한 추론 규칙을 발견하는 것에 주안점을 두게 된다. 술어계한에서 기본적으로 이용되는 추론 규칙은 Modus Pones 및 Universal Specialization으로서, 모두 정당한 추론 규칙들이다.

   1) Modus Ponens
   W1 및 W1 => W2라는 두 문장이 모두 참일 때, W2문장을 새로 생성하는 추론 규칙을 Modus Ponens라고 한다.

   2) Universal Specialization
   Universal Specialization 추론 규칙은 (∀x) W(x)문장으로부터 W(A)라는 문장을 생성하는 것을 의미한다. 이때 A는 상수부호이다.

   추론 규칙을 이용하여 생성된 새로운 판명문을 정리(Theorem)라고 하며, 정리를 생성하기 위해 적용된 추론 규칙의 순서를 정리의 증명(Theorem Proving)이라고 한다. 예를 들어 다음과 같은 두 문장으로 정리를 생성하고 증명하도록 하자.

        (∀x) (W1(x) => W2(x)),
        W1(A)

   위의 두 문장을 결합하면 W2(A)라는 새로운 문장을 얻을 수 있으므로, W2(A)는 정리가 되며, 정리의 증명은 W2(A)를 생성하기 위해 적용된 규칙의 순서, 즉 Universal Specialization과 Modus Ponens가 된다.

(6) 단일화(Unification)

긍정식 (Modus Ponens) 와 같은 추론규칙 (Inference Rule) 을 적용하기 위해서는 두 개의 문장이 문법적으로 서로 동일한 형태를 갖는지를 평가하는 매칭 (Matching) 기능이 있어야 한다. 명제계산 (Propositional Calculus) 에서는 매칭이 간단하게 이루어질 수 있지만, 술어계산 (Predicate Calculus) 에서는 변수부호가 있으므로 매칭과정이 복잡하게 된다. 이러한 문장간의 매칭을 효과적으로 처리해주는 과정을 단일화 라고 한다.

두 개의 문장이 동일한 표현이 될 수 있도록 변수부호에 항을 대치하는 것이 단일화 과정인데, 예로써 (∀x) W(x) 문장에서 W(A) 라는 문장을 생성하기 위해서는 변수 x 에 문제의 대상 영역에 있는 상수부호 A 가 할당되어야 한다. 즉, W(x) 라는 문장과 W(A) 문장이 동일하게 되기 위해서는 x 가 A 로 대치되어야 한다. 이러한 단일화 과정에서 여러 개의 항이 x 에 대치될 수도 있다. 변수를 대응하는 항으로 대체해서 얻어진 표현을 대치문 이라고 하는데, W(A) 는 W(x) 문장에서 얻어진 대치문이 된다. 대치문이 기존문장으로부터 얻어지는 과정을 다음의 예를 통해 알아보도록 하자.

        P (x, f(y), Z)

라는 문장이 있다고 하자. 만일 x변수를 a변수로 대치하고, y변수를 b변수로 대치한다면 다음과 같은 대치문이 얻어지게 된다.

        P(a, f(b), Z)

이때 대치되는 관계를 {a/x, b/y}로 표현하고 이를 단일자(Unifier) s로 표기하면 다음과 같은 관계가 성립하게 된다.

        P (a, f(b) Z) = P (x, f(y), Z) s
        s={a/x, b/y}

위의 예에서 나타난 대치관계는 단일화 과정에서 중요하게 이용되는데, 특히 단일자는 다음과 같이 정의된다.

단일자는 논리식 집합의 모든 문장에 대해 동일한 대치문을 생성하는 역할을 담당하게 된다. 예를 들어 다음과 같은 논리식 집합 E가 있다고 하자.

        E={E₁, E₂}={ P(x, f(y), B), P(x, f(B), B) }

단일자 s를 {A/x, B/y}로 정의한 후 E의 각 문장에 적용하여 대치문을 얻으면 다음 관계가 성립한다.

        E_1S=E_2S=P (A, f(B), B)

   그러므로 s는 E의 단일자가 된다.

두 개의 문장이 동일한 형태를 갖는지를 점검하는 단일화 과정을 구현하는 알고리즘을 다음과 같이 정리하였다. 효과적인 알고리즘 구현을 위해서 문장의 형태를 리스트 형식으로 변환해서 이용하도록 하였다. 예로써 P(x, f(A, y)) 문장은 (P x f(A,y)) 형태로 변환하여 처리한다.

   위에서 정리된 알고리즘 이용하여, 다음 두 문장을 단일화하는 과정을 살펴보도록 하자.

단일화 과정은 하나의 표현과 다른 표현을 패턴 매칭하는 과정과 유사하나, 변수를 포함하므로 패턴 매칭보다 더욱 포괄적인 기능을 갖추고 있다고 말할 수 있다. 

4. 도출법 (Resolution)

도출법 (resolution) 은 명제계산 이나 술어계산 에서 정리를 증명하기 위해 이용되는 추론 규칙 으로서, 논리구 (Literal) 의 OR 결합으로만 이루어진 절(Clause)이라고 하는 특별한 논리식의 집합에 적용된다. 도출법 과정은 두 개의 부모절로부터 새로운 절을 생성하는 추론 과정으로서 다음과 같은 단계를 거쳐 이루어지게 된다.

(1) 절(Clause) 집합으로의 변환

절은 논리구의 OR 결합만으로 구성된 논리식을 의미한다. 모든 술어계산의 논리식은 절로 구성된 집합으로 변환할 수 있다. 술어계산의 정리증명을 위해서는 모든 문장을 절의 집합으로 변환하는 것이 필요하므로 이 변환과정을 상세히 살펴보도록 하자.

   다음의 술어계산 문장을 절의 집합으로 변환하는 과정을 살펴보도록 하자. 이 때, {, }, [, ] 부호들은 문장을 묶기 위해 사용하는 부호로서 괄호부호와 같은 용도로 이용된다.

        (∀x) { P(x) => { (∀y) [P(y) => P(f(x,y))] ∧ ¬(∀y) [Q(x,y) => P(y)]}}

   1) 암시부호 =>를 삭제한다.
   암시부호가 있는 X1 => X2 문장을 동일한 ¬X1 ∨ X2 문장으로 대치함으로써, 암시부호를 삭제할 수 있다. 위 예제에서 이 대치가 실행되면 다음 문장을 얻게 된다.

        (∀x) { ¬P(x)  ∨ { (∀y) [¬P(y)  ∨ P(f(x,y))] ∧ ¬(∀y) [¬Q(x,y)  ∨ P(y)]}}

   2) 부정부호 ¬의 범위를 축소한다.
   각 부정부호의 적용범위를 최대 한 개의 기본 문장에만 한정하도록 한다. 이를 위하여 de Morgan 법칙 등을 이용하여 진위값의 변동이 없는 다른 문장으로 변환한다. 위 예제의 경우 de Morgan 법칙을 적용하면 다음과 같은 결과를 얻게 된다.

        (∀x) { ¬P(x)  ∨ { (∀y) [¬P(y)  ∨ P(f(x,y))] ∧ (y) [Q(x,y) ∧ ¬P(y)]}}

   3) 변수를 표준화한다.
   어떤 변수가 정량자에 의해 제한받는 제한변수인 경우, 변수명을 다른 변수명으로 치환하더라도 논리식의 진위값에는 변동이 없다. 각 정량자가 각기 고유한 변수이름을 갖도록 필요한 변수명을 치환한다. 위 예제의 경우에는 y라는 변수명이 전체정량자 및 존재정량자 모두에 이용되고 있으므로, 존재정량자에 이용되는 y변수를 다른 변수명 w로 치환하였다.

        (∀x) { ¬P(x) ∨ { (∀y) [¬P(y) ∨ P(f(x,y))] ∧ (w) [Q(x,w)  ∧ ¬P(w)]}}

   4) 존재정량자 를 제거한다.
다음과 같은 논리식을 살펴보자.

        (∀y)[ (x) P(x,y) ]

이 문장은 모든 y에 대해 P(x,y)인 어떤 x가 존재한다는 의미가 된다. 일반적으로 존재정량자는 전체정량자의 범위 내에서 적용하게 되므로 x변수는 y변수에 종속된다고 할 수 있다. 이러한 관계를 Skolem 함수로 표현할 수 있다. Skolem 함수를 이용하여 윗 문장을 동일하게 변환될 수 있다.

        (∀y) P( g(y), y )

   Skolem 함수 g(y)는 y의 각 값을 문제의 대상 영역에 존재하는 x로 매핑하게 된다.
   논리식으로부터 존재정량자를 제거하는 일반적인 방법은 존재정량자에 의해 제한받는 변수를 Skolem 함수로 대치하면 된다. 이때 Skolem 함수의 인자는 전체정량자에 의해 제한받는 변수이며, 함수부호는 기존에 사용되고 있지 않는 새로운 이름을 이용한다. 만일 존재정량자가 전체정량자의 적용범위 내에 있지 않는 경우에는 Skolem 함수는 인자없이 상수만을 사용한다. 예를 들어, (x) P(x)는 P(A)가 된다. 상수부호 A는 이미 존재하는 값을 가리키게 된다.
   3)과정에서 이용되는 예제를 보면, 존재정량자가 w 변수에 적용되고 있으므로 Skolem 함수 g(x)를 이용하여 다음과 같이 변환할 수 있다.

        (∀x) { ¬P(x) ∨ { (∀y) [¬P(y) ∨ P(f(x,y))] ∧ [Q(x,g(x)) ∧ ¬P(g(x))]}}

   5) 선행정량자(Prenex)형으로 변환한다.
모든 전체정량자를 논리식의 맨 앞으로 이동시켜 각 정량자가 논리식 전체에 적용되도록 한다. 이러한 논리식을 선행정량자형이라고 한다. 정량자가 없는 논리식을 무정량자(Matrix)형이라고 한다. 그러므로 선행정량자형은 전체 정량자와 무정량자형으로 이루어진 논리식 형태를 가리키게 된다.

        (∀x)(∀y) { ¬P(x) ∨ { [¬P(y) ∨ P(f(x,y))] ∧ [Q(x,g(x)) ∧ ¬P(g(x))]}}

   6) 무정량자형을 논리적 정규형(Conjuctive Normal)형으로 변환한다.
어떤 논리식이 유한개수의 절의 AND 결합으로 이루어져 있는 경우 이를 논리적 정규형이라고 한다. 분배법칙 X1 ∨ (X2 ∧ X3)=(X1 ∨ X2) ∧ (X1 ∨ X3)을 이용하여 무정량자형을 논리적 정규형으로 변환할 수 있다.

        (∀x)(∀y) {[¬P(x) ∨ ¬P(y) ∨ P(f(x,y))] ∧ [¬P(x) ∨ Q(x,g(x))] ∧ [¬P(x) ∨ ¬P(g(x))]}

   7) 전체정량자 ∀ 를 삭제한다.
무정량자형에 있는 변수는 모두 전체정량자에 의해서만 제한받게 되므로, 전체정량자를 논리식으로부터 삭제해도 항상 모든 변수는 전체정량자에 의해서만 제한받는 것으로 가정할 수 있다. 그러므로 논리식은 이제 논리적 정규 형태의 무정량자형만 남게 된다.

        {[¬P(x) ∨ ¬ P(y) ∨ P(f(x,y))] ∧ [¬P(x) ∨ Q(x,g(x))] ∧ [¬P(x) ∨ ¬P(g(x))]}

   8) AND 부호 ∧ 를 삭제한다.
X1 ∧ X2를 {X1, X2}로 표현함으로써, ∧ 부호를 삭제할 수 있다. 이때 X1과 X2는 각각 논리구의 OR 결합으로만 표현된 절이다.

        {[¬P(x) ∨ ¬P(y) ∨ P(f(x,y))],
         [¬P(x) ∨ Q(x,g(x))],
         [¬P(x) ∨ ¬P(g(x))]}

   9) 변수명을 다시 부여한다.
   각 절에서 사용되는 변수명을 고유하게 부여한다.

         {[¬P(x1) ∨ ¬P(y) ∨ P(f(x1,y))],
           [¬P(x2) ∨ Q(x2,g(x2))],
           [¬P(x3) ∨ ¬P(g(x3))]}

   1)~9)의 과정을 통해 논리식이 절집합으로 변환되게 된다. 이러한 절집합으로부터 추론 규칙 도출법이 적용될 수 있다.

일차 술어계산에서 사용되는 논리식 중에서 Horn 절이라고 불리우는 특수한 형태의 절이 있다. Horn 절은 한 개 이하의 긍정적 논리구(Positive Literal)만을 갖는 절을 의미하는데, 긍정적 논리구는 부정부호가 없는 논리구를 의미한다. 예를 들면 P, ¬P∨Q, P⇒Q는 모두 Horn절의 형태를 갖고 있다. P⇒Q 문장은 두 개의 긍정적 논리구를 갖고 있는 형태인 것처럼 보이나, 절 형태로 변환할 경우에는 ¬P∨Q  가 되므로 Horn 절이 됨을 알 수 있다. PROLOG에서 사용되는 문장은 모두 Horn절 형태를 갖고 있다.

(2) 변수가 없는 문장에 대한 도출법

어떤 논리식들의 집합으로부터 새로운 논리식을 생성하는 과정을 알아보기 위해 논리식에 변수가 없는 절에 대한 도출법을 알아보도록 한다. 부모절로부터 새로운 절이 생성되면 이 절은 도출절(Resolvant)이라고 하는데, 도출절은 두 부모절의 OR 결합을 취한 다음 상호 짝이 되는 ¬P, P를 제거하면 얻어지게 된다. 예를 들어, A ∨ P 문장과 ¬P ∨ Q 문장이 모두 참이라고 한다면 이 두 개의 절로부터 얻어지는 도출절은 A ∨ Q가 된다. 이러한 도출법과정은 다음과 같은 설명에 의해 정당함을 알 수 있다. 

(3) 일반적인 절에 관한 도출법

변수를 포함하는 절에 대한 도출법과정은 우선 변수를 치환하기 위해 단일화 과정이 필요하다. 다음절에서 단일화 과정을 통해 두 개의 문장을 동일한 형태로 바꾸어 놓은 다음에 도출법이 진행되는 과정을 설명하였다.

도출법은 정당한 추론 규칙이다. 즉, 두 개의 부모절로부터 생성된 도출절은 부모절로부터 논리적으로 유도될 수 있다. 도출법이 모순법(Refutation)이라 불리우는 정리 증명 시스템에 사용될 경우에는 완전한 추론 규칙도 될 수 있다. 즉, 어떤 논리식 집합으로부터 논리적으로 유도될 수 있는 모든 논리식을 모순도출법 (Resolution Refutation) 을 이용하여 그 집합으로부터 생성해낼 수 있는 것이다.

(4) 모순도출법

술어계산에서 정리를 증명하기 위한 방법으로는 크게 두 가지 방법이 있다. 모순을 이용하는 방법과 연역(Deduction)을 이용하는 방법이다. 연역을 이용하는 방법에는 전문가시스템의 대표적인 추론방법으로 많이 이용되고 있는 정방향 추론과 역방향 추론이 있다. 그러면 이하에서는 반박을 이용한 정리증명방법에 대해 상세히 알아보도록 하자.

만일 논리식 W가 논리식 집합 S로부터 논리적으로 유도될 수 있는 것인지를 증명하려고 한다면, 도출법을 이용하는 시스템에서는 모순에 의해 증명한다. 이때의 증명방법은 다음과 같다. W를 부정한 ¬W를 S집합에 포함시켜서 S'를 생성한다. 이 확장된 S'를 절의 집합으로 변환한 후 도출법을 이용해서 모순(NIL 절로 표현)을 이끌어낸다. 만일 NIL이 얻어지지 않으면 W는 S로부터 논리적으로 유도될 수 없음을 나타낸다.
이러한 모순도출법 과정을 예를 통해 알아보도록 하자.

   다음과 같은 사실이 술어계산 논리식으로 표현되어 있다고 하자.

   1) 읽을 수 있는 존재는 글을 안다.
        (∀x) [ R(x) => L(x) ]

   2) 모든 돌고래는 글을 알지 못한다.
        (∀x) [ D(x) => ¬L(x) ]

   3) 어떤 돌고래는 영리하다.
        (x) [ D(x) ∧ I(x) ]

   위의 사실로부터 우리는 다음과 같은 사실을 증명하고자 한다.

   4) 영리하더라도 읽지 못하는 경우도 있다.
        (x) [I(x) ∧ ¬R(x) ]

   우선 1)~3)의 논리식을 절의 집합으로 변환하면 다음과 같은 결과를 얻게 된다.

   1)   ¬R(x) ∨ L(x)
   2)   ¬D(y) ∨ ¬L(y)
   3)  D(A)
   3') I(A)

각 변수는 표준화되었으며, A는 Skolem 상수이다. 정리를 증명하기 위해서는 정리의 부정문을 절의 형태로 변환한 후 1)~3')의 집합에 추가하여 모순(NIL)을 이끌어 내도록 한다. 모순도출법 과정은 다음과 같은 반박트리의 형태로 나타낼 수 있다.

위의 반박트리에서 NIL이 얻어졌으므로 새로운 절은 기존의 논리식들로부터 논리적으로 유도될 수 있음을 보여 주고 있다. 모순도출법 과정에서 도출절을 생성하기 위해 어떤 부모절을 선택하느냐에 따라서 증명에 소요되는 시간이 영향을 받게 된다. 이러한 도출법의 통제 전략으로는 너비우선전략, 깊이우선전략 등과 같은 여러 가지 전략이 있다.