정리 증명 (Theorem Proving)

 

인공지능 원론 : 유석인, 교학사, 1988, Page 213~245

 

1. 서론

2. 비교흡수 부정 시스템 (resolution refutation system)

     (1) 비교흡수 (resolution)

     (2) 비교흡수 부정 (resolution refutation)

     (3) 비교흡수 (resolution) 과정 제어

     (4) 단순화 방법

     (5) 대답 유도과정

3. 규칙에 기초한 추론 (rule-based deduction)

     (1) 전향 (forward) 추론 시스템

     (2) 후향 (backward) 추론 시스템

     (3) 전향과 후향 시스템의 결합

연습문제

 

 

1. 서론

이 장에서는 정리 증명을 위해 이용되는 두 개의 시스템, 즉 비교흡수 부정 (resolution refutation) 시스템과 규칙에 기초한 연역 (rule-based deduction) 시스템에 대해 고찰한다.

비교흡수 부정 시스템은 어떤 목표문장이, 주어진 문장들의 집합으로부터 논리적으로 뒤따르고 있는지를 증명하기 위해 이 목표문장을 먼저 부정한 후 주어진 문장들과 합하여 새로운 집합을 만들고, 그 다음에 비교흡수 (2 절에서 언급) 과정을 이용해서 모순을 유도하는 시스템이다. 물론 이러한 방법이 논리적으로 정당하다는 것은 뒷절에서 증명된다. 비교흡수 부정 시스템의 중심적인 주제는 비교흡수방법을 명확히 이해하는데서 비롯된다. 비교흡수에 사용되는 문장들은 우선 적용가능한 표현형태 (절 (clause) 이라 하며 (1) 절에서 변환절차를 언급) 로 변환되어야 한다. 더우기 어떤 문장을 선택하여 비교흡수과정을 수행할 것인가 하는 제어방법 ((3) 절에서 자세히 언급) 은 시스템의 효율성을 증가시키는데 기여를 하게 된다.

인공지능 시스템에 의해 사용되는 지식의 대부분은 암시기호 (⇒) 를 사용해서 표현이 가능하다. 비교흡수 부정 시스템에서는 이러한 표현을 우선 절들의 표현으로 변환하여 사용한다. 그러나 이러한 변환과정에서는 암시적 표현에서 주어지는 어떤 유용한 제어정보를 잃어 버릴  수 있다. 예를 들어 절의 표현 (A ∨ B ∨ C) 는 암시적 표현 (~A ∧ ~B) ⇒ C, (~A ∧ ~C) ⇒ B, (~B ∧ ~C) ⇒ A, ~A ⇒ (B ∨ C), ~B ⇒ (A ∨ C), ~C ⇒ (A ∨ B) 등과 논리적으로는 같지만, 이러한 암시적 표현들에는 절의 표현에 나타나지 못하는 각기 다른 제어정보를 가진다. 비교흡수 부정 시스템과는 달리 규칙을 기초로 한 연역 시스템이란 암시적 표현 그 자체를 규칙으로 사용하는 시스템이다.

규칙을 기초로 한 연역 시스템에는 이와 같이 일반적 지식을 표현한 규칙 (rule) 들과 전체 데이터베이스 (global database) 를 이루는 특정한 지식을 표현한 사실들 (규칙들이 적용됨에 따라 전체 데이터베이스의 내용이 변해 감) 로부터 목표 wff 를 증명한다. 이러한 연역 시스템은 전향 (forward) 시스템과 후향 (backward) 시스템으로 분류된다.

전향 시스템이란, 전체 데이터베이스가 목표 wff 를 포함하게 될 때까지 전체 데이터베이스에 규칙 (F-규칙이라 함 ) 들을 적용시키는 것이며, 후향 시스템이란, 목표 wff 로 된 전체 데이터베이스에 규칙 (B-규칙이라 함) 들을 적용시켜 원래 주어진 사실들로 이루어진 전체 데이터베이스를 유도하는 시스템이다.

2. 비교흡수 부정 시스템 (resolution refutation system)

(1) 비교흡수 (resolution)

제 2 장에서 논리기호를 이용한 지식 표기방법에 대해 살펴보았다. 지식 표현인 잘 구성된 공식 (wff) 의 한 종류로 절 (clause) 이 있는데, 절이란 문자들의 논리합으로 구성된 wff 로 정의된다. 여기서 논할 비교흡수방법이란 이러한 절들에 적용되는 하나의 중요한 추론규칙이다. 비교흡수방법을 설명하기에 앞서 먼저 아래의 서술형 명제 wff 을 절들의 집합으로 변환시키는 과정을 살펴보자.

위의 9 가지 단계를 거쳐 wff 는 절들의 집합으로 변환이 된다. 만일 wff X 가 wff 들의 집합 S 에 논리적으로 뒤따르는 (logically follow) 것이라면 집합 S 에 있는 모든 wff 들을 절의 형태로 변환시킨 집합에 wff X 는 논리적으로 뒤따르는 것을 보일 수 있다. 그러므로 절의 표현만을 취급하는 비교흡수방법은 정리증명 시스템에서의 한 추론규칙으로 이용이 될 수 있음이 정당화 된다.

만일 변수를 가지지 않는 항이 절의 변수에 대치되어질 때 나타나는 표현을 본래 절의 기초예시 (ground instance) 라 한다. 예로서 일종의 단순한 절인 Q(A, f(B)) 는 Q(x, y) 의 한 기초예시이다. 비교흡수방법을 쉽게 이해하는 방법은 이러한 기초절들에 어떻게 비교흡수방법이 적용되는가 살펴 보는 것이 편리하다. 두 개의 기초 절, P1 ∨ P2 ∨ … ∨ PN 과 ~P1 ∨ Q2 ∨ … ∨ QM 이 있다고 하자. Pi 와 Qj 모두 서로 다른 것이라고 가정한다. 이 두 개의 부모절 (parant clause) 로부터 비교흡수 절 (resolvent) 이라는 새로운 절을 논리적으로 유도할 수 있다. 이 비교흡수절은 두 개의 절에 대해 논리합을 취하면 P1 ∨ ~P1 ∨ P2 ∨ … ∨ PN ∨ Q2 ∨ … ∨ QM 이 되며 여기서 보수쌍 (complementary pair) 인 P1 ∨ ~P1 을 제거함에 의해 구해진다. 비교흡수방법의 흥미롭고 특수한 경우가 표 1 에 있다. 다음에는 이런 단순한 규칙이 변수를 지닌 절들에는 어떻게 확장되는지 살펴보자.

표 1

부모 절들

비교흡수절

설명

P, ~P ∨ Q (즉 P ⇒ Q)

Q

모더스 포넨스(modus ponens)

P ∨ Q, ~P ∨ Q

Q

이 비교흡수절을 합병 (merge) 이라 함

P ∨ Q, ~P ∨ ~Q

Q ∨ ~Q, P ∨ ~P

두 개의 비교흡수절이 가능하며 이들은 모두 항상 만족되는 동치명제 (tautology) 들임.

~P, P

NIL

모순 (contradiction) 을 나타냄

~P ∨ Q (즉 P ⇒ Q),

~Q ∨ R (즉 Q ⇒ R)

~P ∨ R (즉 P ⇒ R)

연결성 (chaining)

변수를 지닌 절에 대한 비교흡수방법은 제 2 장의 단일화 과정에서 언급한 치환 방법을 두 개의 부모절에 적용하여 이들이 보수문자 (complementary) 들을 서로 가지도록 함으로써 이루어진다. 공식화된 표현을 위해서 먼저 부모절을 문자들의 집합으로 표현한다면, 두 개의 부모절은 각기 {Li}, {Mi} 와 같이 나타내지고 변수들은 따로 표준화되어 있다고 가정할 수 있다 (집합의 문자들을 서로 논리합을 이루고 있음). 더우기 {li} 와 {mi} 는 각각 {Li}, {Mi} 의 부분집합으로 {li} 와 {~mi}  의 합에 대한 가장 일반적 단일화 (이를 s 라 하겠음) 가 존재한다고 하자. 그러면 이제 두 개의 절 {Li} 와 {Mi} 는 비교흡수되어 다음과 같은 비교흡수절이 유도되어진다.

예로써 다음의 두 절에 대한 몇 개의 비교흡수절을 구해 보자.

여기서

{li} = {P[x, f(A)], P[x, f(y)]}, {mi} = {~P[z, f(A)]} 라 하면 이의 비교 흡수절은

이 된다.

두 개의 부모절로부터 유도되어진 비교흡수절은 또한 이 부모절에 논리적으로 뒤따르고 있음을 쉽게 보일 수 있다. 이를 기반으로 wff 들의 집합 S 에 논리적으로 뒤따르고 있는 wff 들은 이 wff 집합 S 에 비교흡수 부정방법을 적용해서 유도되어진다. 그러므로 정리 증명 시스템의 한 종류인 완전성을 지닌 비교흡수방법을 사용하는 비교흡수 부정 시스템의 이해는 이보다 더 효율적인 여러 정리 증명 시스템을 이해하는데 근본적인 기초를 제공하게 된다.

(2) 비교흡수 부정 (resolution refutation)

wff 의 집합 S 에 어떤 wff X 가 논리적으로 뒤따른다는 것을 증명하기 위해 비교흡수를 이용하는 비교흡수 부정방법은 먼저 집합 S 에 X 의 부정인 ~X 를 첨가하여 집합 P = S ∪ {~X} 을 형성한다. 이제 이 새로운 집합 P 로부터 비교흡수과정을 통해 유도되는 새로운 비교흡수절 Ri 을 유도하고, 집합 P 에 Ri 를 추가하여 나오는 새로운 집합에 대해 다시 비교흡수를 행하는 과정을 반복한다. 이 때 과정이 종결되는 시기는 새로이 유도되는 비교흡수절이 모순 (NIL 로 표기함) 을 나타내는 경우이며, 이로부터 wff X 는 집합 S 에 논리적으로 뒤따른다고 한다. 이와 같은 비교흡수 부정방법에 의해 정리 증명이 정당화되는 이유는 다음과 같은 논리로 설명된다.

wff 들로 구성된 집합 S 에 논리적으로 뒤따르는 wff X 가 있다고 가정하자. 그러면, 가정에 의해 S 을 만족하는 모든 해석 (interpretation) 은 또한 X 을 만족한다. 이것은 S 을 만족하는 어떠한 해석도 ~X 을 만족하지 못한다는 사실과 같다. 그러므로 위의 언급한 모든 해석들은 S 와 {~X} 를 동시에 만족시키지 못한다 (여기서 어떤 해석에 의해서도 만족되지 않는 wff 의 집합을 불만족 (unsatisfiable) 하다고 한다.).

실제적으로 X 가 S 에 논리적으로 뒤따른 wff 라면 S ∪ {~X} 는 불만족하다. 만일 비교흡수과정이 불만족한 집합에 반복적으로 적용이 되면 결국에는 모순 (NIL) 이 유도되는 것을 보일 수 있다. 그러므로 만일 X 가 S 에 논리적으로 뒤따르면 비교흡수과정에 의한 S ∪ {~X} 의 집합으로부터 NIL 절을 결국에는 유도하게 될 것이다. 역으로, 만일 NIL 이 집합 S ∪ {~X} 로부터 유도된다면 X 는 S 로부터 논리적으로 뒤따른다는 것을 보일 수 있다.

비교흡수 부정방법을 하나의 예를 통해 살펴보자. 먼저 wff 의 집합 S 가 다음과 같다고 할 때, I(z) ∧ ~R(z) 이 S 에 논리적으로 뒤따르는지를 증명하고자 한다.

먼저 목표 wff 인 I(z) ∧ ~R(z) 을 부정하여 아래의 형태와 같은 절을 구한다.

1) ~ 4) 로 이루어진 집합으로부터 NIL 의 유도에 이르는 동안의 비교흡수과정을 나타내면 그림 1 과 같은 트리 형태가 된다.

그림 1  비교흡수 부정 트리

(3) 비교흡수 (resolution) 과정 제어

앞 절의 예에서 보듯이 모순절인 NIL 을 유도하기 위해 어떠한 두 개의 부모절을 선택해서 단계적으로 비교흡수과정을 수행하게 된다. 이와 같이 비교흡수되는 두 개의 절을 선택하는 방법에는 여러 가지가 있을 수 있다. 그 중에서 어떤 제어방식은 모순이 존재할 경우에는 언제나 이러한 존재를 증명하게 한다. 이러한 제어방법을 완전 (complete) 하다고 한다 (앞에서 논한 추론규칙의 논리적 완전성과는 별개의 개념임). 그러나 인공지능 응용분야에서는, 모순을 보다 효율적으로 구하는 것이 완전성보다 더 중요하게 받아들여지고 있다. 이제 앞절의 예를 이용하여 비교흡수과정 제어방식들을 살펴보자.

그림 2  나비-우선방식의 예

그림 3  세트-오브-서포트 방식의 예

그림 4  선형 입력형 방식의 예

그림 5  비교흡수 부정 트리

(4) 단순화 방법

때때로 절들로 이루어진 어떤 집합에서 몇 개의 절이 제거되거나 또는 절을 이루는 어떤 문자들이 제거될 수 있다. 이러한 단순화는 원래의 집합이 불만족한 집합이면 단순화가 된 후의 새로운 집합도 불만족함을 유지하는 방향으로 진행될 수 있다. 그러므로 이러한 단순화 방법의 적용은 비교흡수 부정방법의 수행과정에서 생겨나는 비교흡수절의 수를 줄이는데 도움을 준다.

(5) 대답 유도과정

많은 서술 논리 정리 증명 시스템에는 존재를 나타내는 변수가 결국 무엇으로 예시되는지 알고자 하는 경우가 있다. 예로서 기초집합 S 에 논리적으로 뒤따르는 (∃x)W(x) 가 있다면 x 가 무엇으로 예시되는가 하는 것이다. 이를 해결하기 위한 과정을 예를 들어 살펴보자.

이것은 다음과 같이 표현된다.

여기서 증명하고자 하는 것은 목표 wff (∃x)AT(FIDO, x) 에서 x 가 무엇인가 하는 것이다. 이를 구하기 위해 (∃x)AT(FIDO, x) 의 부정인 (∀x)~AT(FIDO, x) 를 첨가하여 다음과 같은 기초집합이 형성된다.

이 기초집합을 이용해 NIL 을 유도하는 비교흡수 부정 트리는 그림 6 과 같다. 그러나 (∃x)AT(FIDO, x) 에서 x 를 구하기 위해서는 ~AT(FIDO, x) 를 다시 한 번 부정한 AT(FIDO, x) 를 추가하여 논리합을 시킨다. 그러면 다음과 같은 기초집합이되며 이로부터 위에서와 같은 절차를 거쳐 비교흡수를 행하며, 결국에는 NIL 이 아닌 대답을 지닌 문장이 유도된다.

위의 과정을 거친 대답 유도를 위한 트리는 그림 7 과 같으면 AT(FIDO, SCHOOL) 은 원하는 해답이 된다.

그림 6  비교흡수 부정 트리

그림 7  수정된 증명 트리

앞의 경우와는 달리 전체 한정에 의한 변수를 지닌 목표 wff 가 있는 경우를 살펴보자. 목표 wff 의 부정이 이루어지는 과정에서 이 변수는 존재변수가 되어 스콜렘함수 (skolem function) 로 대치된다.

이제 대답을 유도한 결과에서 이러한 스콜렘 함수가 어떻게 해석이 되는지 다음의 예를 통해 살펴 보자.

여기서 목표 wff (∀x)(∃y)P(y, x) 의 부정은 (∃x)(∀x)~P(y, x) 이 되며, x 는 스콜렘 함수로 대치되므로 ~P(y, A) 로 되어 대답 유도를 위한 기초집합은 아래와 같이 나타난다.

이제 대답 유도를 위한 증명 트리는 그림 8 처럼 된다. 여기서의 대답은 스콜렘 함수 A(상수 형태임) 을 지닌 P(p(A), A) 가 된다. 그러나 본래의 질문이 "모든 x 에 대해 x 의 부모는 누구인가? 즉 x 의 부모는 x 와 어떻게 연관되는 사람인가?" 이므로 A 의 해석을 상수가 아닌 모든 A 에 대해 P(p(A), A) 로 해석함이 타당하다.

그림 8  대답 유도를 지닌 증명 트리

하나의 예를 더 살펴보자. 기초집합 S 가 하나의 절 P(B, w, w) ∨ P(A, u, u) 와 목표 wff (∃x)(∀z)(∃y)P(x, z, y) 를 포함한다 하자.

이것의 비교흡수 부정 트리는 그림 9 와 같이 되며 대답 유도를 위한 증명 트리는 그림 10 과 같이 된다. 여기서 보면 스콜렘 함수 g(x) 대신에 변수 t 가 사용되었으며 결과적으로 P(A, t, t) ∨ P(B, z, z) 을 유도하였다. 그러나 P(A, t, t) 와 P(B, z, z) 은 같은 의미를 가진다.

그림 9  비교흡수 부정 트리

그림 10  수정된 증명 트리

결론적으로, 비교흡수방법을 이용한 대답 유도과정의 절차는 다음과 같다.

3. 규칙에 기초한 추론 (rule-based deduction)

(1) 전향 (forward) 추론 시스템

그림 11  사실 표현의 AND/OR 트리 표현

그림 12  변수를 가지지 않는 AND/OR 그래프

그림 13  규칙 적용 후의 AND/OR 그래프

그림 14  변수를 포함하는 사실 표현의 AND/OR 그래프

그림 15  변수를 지니는 규칙이 적용된 후의 AND/OR 그래프

일치하는 치환과 치환의 단일화 결합은 다음과 같이 정의된다.

을 치환의 집합이라 하며 각 는 다음과 같은 쌍의 집합이다.

여기서 t 들은 묶음 (term) 이고 v 들은 변수이다. 으로부터 두 개의 수식을 정의한다.

치환 이 일치한다 (consistent) 는 말은 가 단일화 가능하다는 말과 같다. 의 단일화 결합 u 는 의 가장 일반적 단일화를 말한다.

단일화 결합의 몇가지 예가 표 2 에 주어져 있다.

표 2  단일화 결합에 의한 치환

{A/x}

{x/y}

{f(z)/x}

{x/y, x/z}

{s}

{g(y)/x}

{f(g(x1))/x3,

f(x2)/x4}

{B/x}

{y/z}

{f(A)/x}

{A/z}

{ }

{f(x)/y}

{x4/x3, g(x1)/x2}

 

불일치

{x/y, x/z}

{f(A)/x, A/z}

{A/x, A/y, A/z}

{s}

불일치

{f(g(x))/x3,

f(g(x1))/x4, g(x1)/x2}

해결 그래프가 일치되는 비교선택 아크의 치환을 가진다는 것은 원래의 사실에 규칙들을 적용했을시 새로운 절들이 유도된다는 것을 말한다. 하나의 예를 살펴보자.

P(x) ∨ Q(x) 의 사실과 두 개의 규칙 P(A) ⇒ R(A), Q(B) ⇒ R(B) 의 AND/OR 그래프는 그림 16 과 같이 된다. 비록 이 그래프가 R(A), R(B) 로 이름이 붙여진 문자 노드를 가진 해결 그래프를 포함할지라도 이 그래프는 불일치된 치환을 포함한다. 그러므로 [R(A) ∨ R(B)] 는 그림 16 의 AND/OR 그래프에 의해 유도되는 절이 아니다.

그러나 그림 16 은 [R(A) ∨ Q(A)] 절의 표현을 나타낼 수 있다. R(A) 와 Q(x) 이름이 붙여진 문자 노드로 종결되는 해결 그래프에 일치되는 R(A) ∨ Q(x) 표현에 치환 {A/x} 을 적용하면 [R(A) ∨ Q(A)] 의 절이 얻어진다.

그림 16  불일치의 치환을 지닌 AND/OR 그래프

규칙과 목표 문자들에 의해 확장되는 AND/OR 그래프의 과정은 일치되는 해결 그래프가 모든 종료 노드에서 목표 노드를 가지는 순간에 성공적으로 종결이 된다. 이로부터 생성 시스템은 목표에 대한 OR 결합이 해결 그래프에 있는 목표 노드로 이름이 붙여진 문자의 OR 결합에 단일화 결합을 해서 얻어진다는 것을 알 수 있다. 이제 간단한 예를 들어 전향 생성 시스템의 작동을 설명한다. 다음과 같은 사실과 규칙들을 가지고 있다고 해보자.

그림 17  "Terrier" 문제의 AND/OR 그래프

이로부터 ~TERRIER(z) ∨ NOISY(z) 로 주어지는 목표 wff 를 증명하고자 한다. 여기서 z 는 존재한정변수이다. 이 문제의 AND/OR 그래프는 앞의 그림 17 과 같다. 이 AND/OR 그래프 안에서 일치되는 해결 그래프는 {FIDO/x}, {FIDO/y}, {FIDO/z} 의 치환을 가진다. 이 치환들의 단일화 결합은 {FIDO/x, FIDO/y, FIDO/z} 이 되며, 이것을 목표 문자들에 적용하면 다음과 같은 결과를 얻는다.

이 표현은 우리가 증명하고자 하는 목표 wff 의 답이 되며 원하는 결과이다.

(2) 후향 (backward) 추론 시스템

그림 18  목표 wff 의 AND/OR 그래프 표현

그림 19  후향 시스템의 일치되는 해결 그래프

(3) 전향과 후향 시스템의 결합

전향과 후향의 규칙을 기초로한 추론 시스템 각각이 저마다의 한계를 가진다. 후향 시스템의 경우, 어떠한 임의의 형태의 목표 표현도 가질 수 있는 반면에 사실 표현은 문자의 AND 결합이어야만 한다. 전향 시스템의 경우, 어떠한 임의의 형태의 사실 표현도 가능하지만 목표 표현은 문자들의 OR 결합이어야 한다. 그러면 위에서 말한 전향과 후향 시스템에서 나타나는 장점만을 가지는 시스템을 생각해 볼 필요가 있다.

둘을 결합한 시스템의 전체 데이터 베이스는 두 개의 AND/OR 그래프 구조를 가지며, 하나는 목표를, 하나는 사실을 나타낸다. 이 구조들은 앞에서 언급했듯이 B-규칙과, F-규칙에 의해 각각 수정이 되어진다. 이 결합된 시스템은 종결조건이 복잡하게 되는데, 종결이 되는 순간은 그래프에서 비교선택되는 모든 문자 노드들이 단일화되어지는 순간이다. 두 그래프 사이의 모든 가능한 비교선택이 이루어진 후, 목표 그래프의 루트 노드에 있는 표현이 사실 그래프의 루트 노드에 있는 표현과 규칙으로부터 증명이 되는지를 결정해야 한다. 이것이 증명될 때 결합된 시스템은 종결이 된다. 이 종결조건은 사실 노드와 목표 노드가 CANCEL 될 때 이루어진다. CANCEL 은 다음과 같이 순환적으로 정의된다.

예로서 그림 20 의 굵은 선은 사실 노드와 목표 노드가 CANCEL 되는 과정을 보여준다.

그림 20  CANCEL 그래프의 예

연습문제

1. 다음의 wff 들을 클로저 형태로 바꾸어라.

2. 결정은 건전 (sound) 함을 보여라. 즉, 두 클로저의 결정자는 논리적으로 두 클로저를 따른다는 것을 보여라.

3. 다음의 만족되지 않은 클로저들의 집합에 대해 일차적 입력형태 반복을 구하여라.

4. 아래의 어떤 클로저들이 P(f(x), y) 에 의해 포함 (subsume) 되는지 지적하여라.

5. 다음의 각 공식은 항진 (tautologies) 임을 결정반복에 의해 보여라.

6. 결정반복방법을 사용해서 다음의 wff 들의 유효성 (validity) 을 증명하라.

7. 결정반복에 의해 wff (∃x)(Px)) 는 논리적으로 wff[P(A1) ∨ P(A2)] 로부터 따른다는 것을 보여라. 그러나 (∃x)(P(x)) 의 스클렘한 형태인, P(A) 는 [P(A1) ∨ P(A2)] 로부터 논리적으로 따르지 않는다. 여기에 대해 설명하여라.

8. 전체 데이터베이스에서의 결정규칙방식을 사용한 생성 시스템은 가환성 (commutative) 을 가진다는 것을 보여라.

9. 다음의 문장들을 규칙에 기초한 기하정리증명을 위한 생성규칙으로 나타내어라.

10. 블력 문제의 상황이 다음의 wff 들의 집합에 의해 묘사된다.

이러한 wff 들이 묘사하고자 하는 상황을 기술해보아라.

아래의 문장은 이러한 블럭 문제에 대한 일반적인 지식을 제공한다.

    Every big, blue block is on a green block.
    Each heavy, wooden block is big.
    All blocks with clear tops are blue.
    All wooden blocks are blue.

이러한 문장들을 암시적 표현으로 나타내어라. 더우기 "Which block is on a green block?" 을 풀기 위해서 B-규칙을 사용하여 일치하는 AND-OR 해결 트리를 그려라.