귀결과 SLD: 기계는 어떻게 증명하는가

📍 현재 위치: 2부 · 계산으로서의 추론 — 6장 「추론과 증명」에서는 전체 모델이 나타날 때까지 모든 규칙을 발화시키며 규칙을 전방으로 실행했습니다. 이제 우리는 규칙을 후방으로 실행하여, 하나의 질문에서 출발해 사실에 이를 때까지 그것을 추적합니다.

전방 연쇄는 우리가 한 번도 묻지 않은 질문에 답을 내놓았습니다. 그것은 특정 원자에 관심이 있든 없든 상관없이, 학계 세계의 규칙들이 도출할 수 있는 모든 것, 즉 47개의 원자 전부를 계산해 냈습니다. 하지만 대부분의 경우 우리는 결과 전체를 바라는 것이 아니라 단 하나의 질문을 품고 시작합니다. alice는 carol의 조부 지도교수(grand-advisor)인가? alice의 동료는 누구인가? 이 장은 바로 이러한 목표에서 출발하여 후방으로 진행하는 추론, 즉 어떤 규칙이 그것을 결론으로 이끌어낼 수 있는지 묻고, 다시 그 규칙이 무엇을 요구하는지 물으며, 그 요구가 이미 가지고 있는 사실들에서 바닥날 때까지 계속하는 추론을 다룹니다. 그것이 남기는 흔적은 예/아니오가 아니라, 한 줄 한 줄 읽어낼 수 있는 증명 트리(proof tree)입니다.

우리는 "기계가 증명했다"는 말을 블랙박스로 남겨두지 않을 것입니다. 단일화(unification)를 정밀하게 정의하고 치환 딕셔너리가 채워지는 내부 루프를 추적하며, 규칙을 그것이 나타내는 논리식으로 읽고, 하나의 목표를 그 하위 목표들로 바꾸는 단일한 귀결 단계를 도출하며, 전체 증명을 목표 목록이 빈 절로 붕괴하는 일련의 과정으로 실행하고, 모든 수식을 그것을 실행하는 동반 코드의 정확한 줄에 연결할 것입니다. 이 장을 다 읽고 나면 sld.py를 그저 하나의 스크립트가 아니라 증명 절차로 읽을 수 있게 될 것입니다.

쉽게 말하면

당신이 어떤 유명인의 후손임을 증명한다고 상상해 보세요. 지금까지 살았던 모든 사람을 나열하고 그중 누가 당신의 조상인지 확인하지는 않을 것입니다 — 그것은 전방으로, 모든 것을 계산하는 방식입니다. 대신 당신은 주장으로부터 거꾸로 작업합니다. "나는 그녀의 후손이다, 만약 내 부모 중 한 명이 그렇다면; 어느 부모이며, 그것을 보일 수 있는가?" 각각의 "만약"은 한 걸음 더 가까운 누군가에 관한 더 작은 질문을 건네주고, 당신은 가리킬 수 있는 출생증명서에 도달할 때까지 계속합니다. 후방 연쇄(backward chaining)는 이러한 습관을 기계적으로 만든 것입니다: 증명하고자 하는 것에서 시작해, 어떤 규칙이 그것을 결론으로 이끌어낼 수 있는지 묻고, 그 규칙이 필요로 하는 것에 대해 재귀적으로 반복하며, 모든 분기가 기록된 사실에 도달할 때 멈춥니다.

이 장에서 다루는 내용

목표 지향적 증명(goal-directed proof) — 질문에서 출발하여 사실로 거꾸로 작업하는 것이 왜 종종 모든 것을 도출하는 것보다 더 영리한지, 그리고 그것이 어떻게 증명을 탐색(search)으로 바꾸는지.
단일화, 공유되는 기본 연산(unification, the shared primitive) — 치환(substitution), 단일자(unifier), 최대 일반 단일자(most general unifier, MGU)의 정밀한 정의, 20줄짜리 unify.py 기본 연산, 그리고 바인딩 딕셔너리를 채워나가는 루프에 대한 한 줄 한 줄의 추적.
도출된 SLD 귀결 단계(the SLD resolution step, derived) — 규칙을 그것이 축약하는 논리절로 읽어내는 방법, 목표를 그 인스턴스화된 몸체로 대체하는 단일한 귀결 단계, 빈 절을 도출하는 것이 왜 증명이 되는지, 그리고 이 일이 일어나는 sld.py의 핵심 루프.
분해절 수열로서의 완성된 증명(a worked proof, as a resolvent sequence) — grandAdvisor(alice, carol)에 대한 목표 목록에서 빈 절까지의 전체 도출 과정, 렌더링된 증명 트리, 그리고 citesTransitively(p3, p1)에 대한 재귀적이고 백트래킹하는 도출 과정.
질의 응답(query answering) — "alice의 동료들"에 대한 탐색 트리, 부등호 가드(guard)가 제거하는 분기를 포함하여, 실제 실행에서 인용한 질의가 열거하는 모든 바인딩.
전방 대 후방(forward versus backward) — 모든 결과를 계산하는 것이 유리한 경우와 하나의 목표를 추적하는 것이 유리한 경우, 그리고 여기서 후방 탐색이 정확히 왜 종료되는지에 대한 정초적 하강(well-founded descent) 논증.

목표 지향적 증명: 질문에서 출발하기

이전 장인 추론과 증명은 아무것도 새로 나타나지 않을 때까지 모든 규칙을 거듭 발화시켜 — 사실로부터 전방으로 나아가는 체이스(chase) — 최소 고정점(least fixpoint)을 계산했습니다. 후방 연쇄(backward chaining)는 그 화살표를 뒤집습니다. 여러분은 그것에게 ("grandAdvisor", "alice", "carol")처럼 확립하고자 하는 원자인 목표(goal)를 건네주고, 그것은 단 하나의 질문을 던집니다. 어떤 규칙의 머리가 이 목표를 결론으로 이끌어낼 수 있는가? 그런 규칙 하나하나는 하나의 거래를 제안합니다. "네게 그 목표를 주겠다, 하지만 먼저 내 몸체를 증명해야 한다." 그리하여 하나의 목표는 그 규칙의 몸체 원자들로 치환되고, 그 각각은 새로운 하위 목표(sub-goal)가 되며, 이 과정이 되풀이됩니다. 어떤 갈래(branch)는 몸체가 비어 있어 더 이상 증명할 것이 없는 규칙인 사실(fact)에 도달하면 성공합니다 [1]. 이것이 Prolog(Programming in Logic의 줄임말) 뒤에 있는 전략이며, 그 정식 명칭은 SLD 귀결(SLD resolution) — 한정절에 대한 선택적 선형 귀결(Selective Linear resolution for Definite clauses) — 로, 이는 J. A. 로빈슨(J. A. Robinson)의 일반적인 귀결 규칙을, 우리의 규칙들이 이미 그러한 형태인 혼 절(확정절, Horn clause/definite clause)에 특화시킨 것입니다 [2][3].

이를 선호하는 이유는 경제성이며, 이는 실행 예제에서 측정 가능합니다. 전방 연쇄는 크기가 커지다가 이내 유지되는 세 번의 물결 [23, 41, 47, 47]만에 전체 모델에 도달합니다: 23개의 기본 사실, 그다음 41개, 그다음 47개, 그리고 새로 추가되는 것 없이 다시 47개입니다. "alice는 carol의 조부 지도교수인가?"라는 질문에 이 방식으로 답하려면, 여러분은 유도된 24개의 원자 전부( $47 - 23 = 24$ , 여기서 $|\cdot|$ 는 집합 안의 원자 개수를 셉니다)를 실체화한 다음 원하는 것을 찾아보아야 할 것입니다. 앞으로 한 단계씩 살펴보겠지만, 후방 연쇄는 정확히 세 개의 원자만을 건드립니다. 증명은 질문이 이끄는 하나의 탐색(search)이 되며, 그 탐색은 오직 질문이 필요로 하는 것만을 방문합니다.

단일화: 일치 여부를 결정하는 기본 연산

두 엔진 모두 하나의 연산에 의지하고 있으며, 코드를 읽기 전에 그 정의를 정확히 해 두고서 따로 만나볼 가치가 있습니다.

용어를 고정해 둡시다. 원자(atom)는 (predicate, arg1, arg2, ...) 형태의 튜플입니다. 예를 들면 ("advises", "alice", "bob")입니다. 항(term)은 인자 하나이며, 대문자로 시작하면(X, Y, Who) 변수(variable)이고 그렇지 않으면(alice, carol, mit) 상수(constant)인 문자열입니다. 이 하나의 관례는 kb.py의 25~28행에 있는 is_var에서 단 한 곳에 정해져 있습니다. 치환(substitution) $\sigma$ (그리스 문자 시그마)는 변수에서 항으로의 유한한 대응으로, $\sigma = \{X \mapsto \text{alice},\ Z \mapsto \text{carol}\}$ 처럼 씁니다. 여기서 화살표 $\mapsto$ 는 "로 치환된다"라고 읽습니다. 어떤 원자에 $\sigma$ 를 적용한다(applying)는 것은 그 원자 안의 모든 변수를 $\sigma$ 가 그것에 대응시키는 것으로 바꾸는 것을 뜻하며, 이는 정확히 unify.py의 4648행에 있는 apply_sub입니다. 우리는 "치환 $\sigma$ 가 적용된 원자 $A$ "를 $A\sigma$ 로 씁니다.

이제 연산 자체를 살펴봅시다. 두 원자 $A$ 와 $B$ 가 주어졌을 때, 단일자(unifier)란 그 둘을 문자 그대로 동일하게 만드는 치환 $\sigma$ , 즉 $A\sigma = B\sigma$ 인 $\sigma$ 입니다. 두 원자는 여러 개의 단일자를 가질 수도, 하나도 갖지 않을 수도 있습니다. 하나라도 존재한다면, 그중 가장 저렴한 정준적인 것이 하나 있는데, 바로 최대 일반 단일자(most general unifier, MGU)입니다: 다른 모든 단일자가 $\sigma$ 에 더 많은 변수를 바인딩함으로써 얻어질 수 있는 단일자 $\sigma$ 로, 즉 $\sigma$ 는 굳이 필요하지 않은 그 어떤 것에도 얽매이지 않습니다. 단일화(unification)는 두 원자가 일치할 수 있을 때 MGU를 돌려주고 그렇지 않으면 실패하는 절차입니다 [1]. 다음은 unify.py에 있는 그 기본 연산 전체입니다:

def unify(a: tuple, b: tuple, sub: dict | None = None) -> dict | None:
    sub = {} if sub is None else dict(sub)
    if a[0] != b[0] or len(a) != len(b):
        return None
    for x, y in zip(a[1:], b[1:]):
        x, y = walk(x, sub), walk(y, sub)
        if x == y:
            continue
        if is_var(x):
            sub[x] = y
        elif is_var(y):
            sub[y] = x
        else:
            return None  # two different constants — clash
    return sub

이를 세 가지 규칙으로 읽어봅시다. 첫째(위 코드의 31행, 가드), 술어 이름과 항수(arity, 인자의 개수, len(a))가 일치해야 하며, 그렇지 않으면 두 원자는 애초에 전혀 일치할 수 없고 함수는 None을 돌려줍니다. 그다음, 인자 하나하나에 대해(루프, 3342행): 둘이 이미 같으면 그냥 넘어가고, 한쪽이 변수라면 딕셔너리에 항목을 하나 적어 넣음으로써(sub[x] = y, 38행) 그것을 다른 쪽에 바인딩(bind)하며, 양쪽이 서로 다른 상수라면 그것은 충돌(clash)이고 unify는 None을 돌려줍니다. 보조 함수 walk(1620행)는 먼저 이미 이루어진 모든 바인딩을 따라가므로, 일단 X가 alice에 바인딩되면 그 일치 과정이 끝날 때까지 계속 alice로 남아 있으며, 바로 이것이 MGU가 그 자신과 일관되도록 지켜주는 요소입니다.

추적해보는 루프

딕셔너리가 채워지는 과정을 지켜봅시다. 규칙의 머리 grandAdvisor(X_1, Z_1)(그 변수들은 이미 서로 다르게 이름이 찍혀 있으며, 이에 대해서는 아래에서 더 다룹니다)을 목표 grandAdvisor(alice, carol)과 단일화합니다. 각 행은 루프를 한 번 통과하는 과정입니다:

`unify.py`의 단계	비교	결과	그 이후의 `sub`
가드, 31행	술어 `grandAdvisor` = `grandAdvisor`, 항수 $3 = 3$	통과	$\{\}$
루프 반복 1, 33~42행	`x = X_1`, `y = alice`; 다름; `is_var(X_1)`이 참	바인딩, 38행	$\{X_1 \mapsto \text{alice}\}$
루프 반복 2, 33~42행	`x = Z_1`, `y = carol`; 다름; `is_var(Z_1)`이 참	바인딩, 38행	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$
반환, 43행	루프 소진	`sub` 반환	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$

그 결과는 우리가 물었던 바로 그 목표의 모습으로 차려입은 규칙의 머리입니다: $\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$ 을 grandAdvisor(X_1, Z_1)에 적용하면 grandAdvisor(alice, carol)이 나오며, 그 이상으로는 아무것에도 얽매이지 않으므로 이것이 MGU입니다. 이와 대조되는 실패 사례도 마찬가지로 짧습니다. 목표 advises(alice, carol)을 사실 advises(alice, bob)과 단일화해 봅시다: 첫 번째 반복은 alice와 alice를 비교하는데, 같으므로 계속 진행합니다; 두 번째 반복은 서로 다른 두 상수 carol과 bob을 비교하는데, 어느 쪽도 변수가 아니므로 마지막 else가 발동하여 unify는 None을 돌려줍니다(42행). 바로 그 하나의 충돌 때문에 provable(("advises", "alice", "carol"))은 False를 돌려줍니다: alice는 오직 bob만을 지도하며, 어떤 치환도 carol을 bob과 같게 만들 수 없기 때문입니다.

이것이 왜 유명하게 까다로운 연산의 단순한 버전일까요? 우리의 언어에는 함수 기호가 전혀 없기 때문입니다: 이는 논리 프로그래밍의 함수 없는 파편인 데이터로그(Datalog)입니다. 완전한 1차 논리에서는 f(g(X))처럼 항이 중첩될 수 있으며, 단일화는 어떤 변수를 그것을 포함하는 항에 바인딩하는 것을 거부하기 위해 발생 검사(occurs-check)를 실행해야 하는데, 그렇지 않으면 무한한 구조가 만들어지기 때문입니다. 여기서는 모든 인자가 납작한 상수이거나 변수이므로, 중첩될 것이 아무것도 없고, 발생 검사도 필요 없으며, 처음 시작한 것보다 더 큰 항을 만들어 낼 방법도 없습니다. 학계 세계의 고정된 상수들로부터 형성될 수 있는 원자는 오직 유한하게 많을 뿐이며, 이것이 유한한 허브랜드 기저(Herbrand base)입니다. 바로 그 유한성이 전방 연쇄를 멈추게 만드는 것입니다; 후방 SLD는 더 미묘하며, 그것 역시 여기서 왜 종료하는지는 이 장의 끝에서 다시 다루겠습니다 — 허브랜드 기저와는 다른 이유에서입니다.

도출된 SLD 귀결 단계

엔진을 살펴보기 전에, 규칙을 그것이 축약하고 있는 논리로 읽어봅시다. 방법 전체가 하나의 논리적 단계를 거듭 적용하는 것이기 때문입니다. kb.py의 79행에 있는 조부 지도교수 규칙은

\text{grandAdvisor}(X, Z) \leftarrow \text{advises}(X, Y)\ \wedge\ \text{advises}(Y, Z),

1학년 독자라면 이미 한 번은 완전히 해독해 두었어야 할 세 가지 연결사(connective)를 사용합니다. 화살표 $\leftarrow$ 는 "만약"이라고 읽습니다: 왼쪽의 머리는 오른쪽의 몸체가 성립할 때에만 성립합니다. 쐐기 $\wedge$ 는 "그리고"라고 읽습니다. 나중에 우리는 $\vee$ ("또는")와 $\neg$ ("아님")를 만나게 될 것입니다. 논리적으로, " $B_1$ 이고 $B_2$ 이면 $H$ "는 " $H$ 이거나, 그렇지 않으면 $B_1$ 이 아니거나, 그렇지 않으면 $B_2$ 가 아니다", 즉 $H \vee \neg B_1 \vee \neg B_2$ 와 같은 진술입니다. 정확히 하나의 양의 원자 $H$ 를 갖는 이런 모양의 절은 확정절(definite clause, 혼 절)이며, kb.py의 모든 규칙이 바로 그것입니다.

목표(goal), 즉 질의는 비어 있는 머리를 갖는 $\leftarrow G_1 \wedge \cdots \wedge G_m$ 의 형태로 씁니다. 논리적으로 읽으면 이는 평평한 부정 $\neg(G_1 \wedge \cdots \wedge G_m)$ 입니다: "이것들이 동시에 모두 성립할 수는 없다." 그 틀 지음이 바로 귀결의 핵심입니다. 프로그램 $P$ 가 목표를 함의한다(entail)는 것, 즉 $P \models G_1 \wedge \cdots \wedge G_m$ (이중 턴스타일 $\models$ 는 "논리적으로 함의한다"라고 읽으며, $P$ 의 모든 모델에서 참임을 뜻합니다)을 증명하기 위해, 우리는 그 부정을 가정하고 모순을 찾아 나섭니다. $P$ 에 $\neg(G_1 \wedge \cdots)$ 를 더했을 때 언제나 거짓인 빈 절(empty clause), $\square$ 로 표기되는 것을 도출할 수 있다면, $P$ 와 그 부정을 함께 놓으면 충족 불가능(unsatisfiable)하므로, 결국 $P \models G_1 \wedge \cdots \wedge G_m$ 입니다. 이것이 논박에 의한 증명(proof by refutation)이며, 그 핵심 통찰은 단 하나의 추론 규칙인 귀결(resolution)만으로도 이를 이끌어 가기에 충분하다는 것입니다 [2]. 절차가 그런 논박을 찾아냈을 때 우리는 $P \vdash G$ (단일 턴스타일 $\vdash$ 는 "도출한다"라고 읽으며, 이는 절차에 관한 사실입니다)라고 쓰며, 건전성(soundness)이란 $P \vdash G$ 가 $P \models G$ 를 함의한다는 보장입니다.

SLD 단계는 다음과 같습니다. 현재의 목표 목록(분해절, resolvent) $\leftarrow A_1 \wedge \cdots \wedge A_m$ 을 취하고, 원자 하나 $A_i$ 를 선택하며(Prolog와 sld.py는 언제나 가장 왼쪽의 $A_1$ 을 선택합니다; 이 가장 왼쪽을 고르는 선택이 이름의 S, 즉 Selective에 해당하는 부분이며, 그것의 선택 함수입니다), 그 머리가 그것과 단일화되는 규칙 $H \leftarrow B_1 \wedge \cdots \wedge B_n$ 을 고릅니다, $\sigma = \text{unify}(H, A_i)$ . L, 즉 Linear는 완전히 다른 것을 가리킵니다: 도출 과정의 모양으로, 각각의 새 분해절이 이전 분해절을 프로그램의 절 단 하나에 대해 귀결시킴으로써 얻어지는, 절들의 가지치기식 조합이 아니라 하나의 사슬(chain)이라는 뜻입니다. 선택된 원자를 규칙의 몸체로 치환하고 모든 것에 단일자를 적용합니다:

\leftarrow (A_1 \wedge \cdots \wedge A_{i-1}\ \wedge\ B_1 \wedge \cdots \wedge B_n\ \wedge\ A_{i+1} \wedge \cdots \wedge A_m)\,\sigma.

이런 단계 하나하나는 건전한 논리적 추론이며, 그 한 줄짜리 이유는 그저 인용만 하기보다는 실제로 보여줄 가치가 있습니다. 분해절이 하나의 부정이라는 점을 떠올려 봅시다: 이전 것은 절 $\neg A_1 \vee \cdots \vee \neg A_m$ 을 주장하고, 규칙은 $H \vee \neg B_1 \vee \cdots \vee \neg B_n$ 을 주장하며, 우리는 $H\sigma = A_i\sigma$ 가 되도록 $\sigma$ 를 골랐습니다. $\sigma$ 를 적용한 뒤에 이 둘을 모두 만족시키는 임의의 모델 $M$ (접지 원자들에 대한 임의의 진리값 배정)을 취해 봅시다. 선택된 원자를 기준으로 경우를 나눕니다. $M$ 이 $A_i\sigma$ 를 참으로 만든다면, 이전 부정의 선언지 $\neg A_i\sigma$ 는 거짓이므로, 이전 부정은 오직 다른 어떤 $\neg A_j\sigma$ 가 참이기 때문에만 성립할 수 있습니다; 혹은 $M$ 이 $A_i\sigma$ 를, 따라서 $H\sigma$ 를 거짓으로 만든다면, 규칙은 오직 어떤 $\neg B_k\sigma$ 가 참이기 때문에만 성립할 수 있습니다. 어느 쪽이든 살아남는 선언지는 그 자체로 새 분해절의 선언지이므로, $M$ 은 새 분해절 또한 만족시킵니다: 새 분해절은 이전 분해절과 그 규칙이 함께 함의하는 것입니다 [2]. 사실(fact)은 몸체 원자가 $n = 0$ 개인 규칙이므로, 사실에 대해 귀결시키는 것은 그저 선택된 원자를 삭제하는 것입니다(끼워 넣을 몸체가 없습니다). 분해절이 비게 되면 모든 원자가 삭제된 것이며, 그 빈 분해절이 바로 빈 절 $\square$ 입니다: 논박이 완결되고 목표가 증명된 것입니다. 그 과정에서 누적되는 치환, 즉 각 단계에서 사용된 단일자들의 합성 $\sigma = \sigma_k \circ \cdots \circ \sigma_1$ (고리 $\circ$ 는 "~와 합성된다"라고 읽으며, 앞선 바인딩을 적용한 다음 나중 바인딩을 적용한다는 뜻입니다)이 바로 답(answer)입니다: 원래의 목표를 참으로 만드는 바인딩들입니다.

이제 엔진을 살펴봅시다. 위 정의의 모든 조항이 그 안에 나타납니다. 현재의 목표 목록이 주어지면, sld.py는 그 가운데 첫 번째 것을 가져와 각 규칙을 차례로 시도합니다:

    goal, rest = goals[0], goals[1:]
    g = apply_sub(goal, sub)
    ...
    for rule in rules:
        head, body = rename(rule, counter)
        s = unify(head, g, sub)
        if s is None:
            continue
        for s_body, body_proofs in _solve(body, s, rules, counter):
            this = Proof(apply_sub(g, s_body), body_proofs)
            for s_rest, rest_proofs in _solve(rest, s_body, rules, counter):
                yield s_rest, [this] + rest_proofs

이것을 앞서의 도출 과정과 맞추어 봅시다. goal, rest = goals[0], goals[1:](42행)는 가장 왼쪽 선택입니다: $A_1$ 이 goal이고, $A_2 \wedge \cdots \wedge A_m$ 이 rest입니다. unify(head, g, sub)(54행)는 단일자 $\sigma$ 를 계산하며, 이 규칙으로는 어떤 단계도 불가능할 때 정확히 None을 돌려주고, 그때 continue가 다음 규칙으로 넘어갑니다(이것이 백트래킹(backtracking)입니다). _solve(body, s, ...)(57행)는 끼워 넣어진 몸체 $B_1 \wedge \cdots \wedge B_n$ 을 증명하고, _solve(rest, s_body, ...)(59행)는 남은 목표들 $A_2 \wedge \cdots \wedge A_m$ 을 증명하는데, 둘 다 확장된 치환 아래에서 이루어집니다: 이 둘을 합치면 바로 새 분해절이 됩니다. 그리고 재귀를 멈추게 하는 기저 사례가 바로 빈 절 그 자체입니다:

def _solve(goals: list, sub: dict, rules: list, counter: list):
    """Yield ``(substitution, [proofs])`` for every way to prove all ``goals``."""
    if not goals:
        yield sub, []
        return

if not goals:(3941행)가 바로 " $\square$ , 성공"이라는 줄입니다: 남은 목표가 없으므로, 누적된 치환과 빈 증명 목록을 산출(yield)합니다. 한 가지가 더 제 몫을 합니다. 사용하기 전마다, rename(unify.py의 5164행)은 규칙 안의 모든 변수에 새로운 숫자 접미사를 찍어, 파일 안의 X를 X_1, X_2 등으로 바꿉니다. 이것이 분리 표준화(standardize-apart) 원칙이며, 이는 겉치레가 아닙니다: 이것이 없다면, 하나의 증명 안에서 같은 규칙을 두 번 사용하는 것(혹은 재귀적인 규칙이 자기 자신을 호출하는 것)은 실수로 변수를 공유하게 되어, 한쪽 사용에서 강제된 바인딩이 다른 쪽을 그릇되게 제약해 버릴 것입니다 [1]. 표기법에 관한 한 가지 유의점이 있습니다: 여기 추적 과정 전체에서 쓰인 접미사 _1(그리고 아래에서 R1과 R2를 구분하는 _2)은 예시적인 것일 뿐, 실제로 포착된 값이 아닙니다. rename은 자신이 시도하는 모든 규칙과 사실에 걸쳐 하나의 카운터를 공유하므로, 실제 정수는 순서에 의존하며 보통 더 큽니다. grandAdvisor(alice, carol)의 실제 실행에서는, 카운터가 이미 23개의 사실과 도중에 건너뛴 앞선 규칙들을 지나쳤으므로, 머리에는 X_27, Z_27이 찍힙니다. 오직 이름의 신선함(freshness)만이 중요할 뿐 특정한 숫자는 전혀 중요하지 않으며, 그래서 이 추적들은 가장 단순한 _1을 씁니다.

분해절 수열로서의 증명

다음은 정의가 규정하는 방식으로 쓰인 grandAdvisor(alice, carol)에 대한 전체 도출 과정입니다: 질의에서 시작해 $\square$ 로 붕괴하는 분해절들의 수열입니다. 사실들은 빈 몸체를 갖는 절로서 규칙 집합에 접혀 들어가므로(sld.py의 72행: all_rules = [(fact, []) for fact in facts] + list(rules)), 사실과의 일치는 그저 $n = 0$ 인 SLD 단계일 뿐입니다.

#	분해절 (아직 증명할 목표)	선택된 원자	사용된 절 (이름 변경됨)	이 단계의 MGU	지금까지의 답 $\sigma$
0	$\leftarrow \text{grandAdvisor}(\text{alice}, \text{carol})$	grandAdvisor(alice, carol)	$\text{grandAdvisor}(X_1, Z_1) \leftarrow \text{advises}(X_1, Y_1) \wedge \text{advises}(Y_1, Z_1)$	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol}\}$
1	$\leftarrow \text{advises}(\text{alice}, Y_1) \wedge \text{advises}(Y_1, \text{carol})$	advises(alice, $Y_1$ )	$\text{advises}(\text{alice}, \text{bob}) \leftarrow$ (사실)	$\{Y_1 \mapsto \text{bob}\}$	$\{X_1 \mapsto \text{alice},\ Z_1 \mapsto \text{carol},\ Y_1 \mapsto \text{bob}\}$
2	$\leftarrow \text{advises}(\text{bob}, \text{carol})$	advises(bob, carol)	$\text{advises}(\text{bob}, \text{carol}) \leftarrow$ (사실)	$\{\}$ (이미 접지됨)	변화 없음
3	$\square$ (빈 절)	—	—	—	성공

0단계는 머리가 단일화되는 유일한 규칙에 대해 규칙 루프가 발동하는 것입니다. 1단계는 몸체를 끼워 넣고 그 첫 번째 원자를 곧바로 사실에 대해 귀결시켜 $Y_1 \mapsto \text{bob}$ 을 바인딩합니다; 그 바인딩이 어떻게 전파되는지 눈여겨보십시오, 1단계에서는 여전히 advises(Y_1, carol)이던 두 번째 몸체 원자가 2단계에 이르러서는 접지된 advises(bob, carol)이 됩니다. 3단계는 기저 사례 if not goals입니다. 이 증명은 정확히 grandAdvisor(alice, carol), advises(alice, bob), advises(bob, carol)이라는 세 개의 원자만을 방문했습니다 — 전방 연쇄였다면 만들어 냈을 스물네 개와 대비됩니다.

증명 트리: 감사 가능한 자취

성공이 단 하나의 불리언 값이 아니라 Proof 노드들(sld.py의 1934행에 있는 클래스)의 트리로 만들어지기 때문에, 우리는 추론 과정을 그대로 출력할 수 있습니다. Proof는 자신이 증명한 목표와, 그것을 확립한 몸체의 하위 증명들의 목록을 저장합니다; render(2934행)는 들여쓰기를 늘려가며 이를 순회합니다. sld.py를 실행하면 목표를 증명하고 그것을 렌더링합니다:

p = prove(("grandAdvisor", "alice", "carol"))
print("proof of grandAdvisor(alice, carol):")
print(p.render(1) if p else "  (unprovable)")

proof of grandAdvisor(alice, carol):
  grandAdvisor(alice, carol)
    advises(alice, bob)
    advises(bob, carol)

이것이 위의 분해절 수열을 다시 트리 모양으로 접어 넣은 것입니다: 뿌리에는 목표가 있고, 들여쓰기된 두 자식은 그것을 확립한 사실들로, 이는 정확히 $\sigma$ 가 적용된 뒤의 두 몸체 원자입니다. 이는 충실한 증명 자취(faithful proof trace)입니다: 모든 단계가 실제 규칙이나 사실에 대한 진짜 단일화이므로, 그 결론은 단언된 것이 아니라 감사 가능(auditable)합니다 [3].

SLD 귀결이 grandAdvisor(alice, carol)에 대해 만들어 내는 증명 트리: 뿌리에 놓인 목표, 그것을 결론으로 이끌어내는 규칙과 그 단일화 치환, 그리고 기본 사실에서 바닥을 이루는 두 개의 몸체 목표 — 그저 '예'가 아니라 감사 가능한 자취입니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

추적해보는 재귀와 백트래킹

규칙의 몸체가 같은 규칙을 다시 불러올 때 트리는 더 높아집니다. kb.py의 86~88행에 있는 인용 규칙들이 흥미로운 사례인데, 두 번째 규칙이 자기 몸체 안에서 citesTransitively를 호출하기 때문입니다:

\begin{aligned} &\text{R1:}\quad \text{citesTransitively}(A, B) \leftarrow \text{cites}(A, B),\\ &\text{R2:}\quad \text{citesTransitively}(A, C) \leftarrow \text{cites}(A, B)\ \wedge\ \text{citesTransitively}(B, C). \end{aligned}

citesTransitively(p3, p1)을 증명하는 과정은 재귀와 백트래킹을 강제하는 죽은 갈래를 모두 보여줍니다. 엔진은 절들을 순서대로 시도합니다:

R1(이름 변경됨), 실패. $\text{citesTransitively}(A_1, B_1)$ 을 목표와 단일화합니다: $\{A_1 \mapsto \text{p3},\ B_1 \mapsto \text{p1}\}$ . 몸체는 cites(p3, p1)이 됩니다. 하지만 인용 사실은 오직 cites(p2, p1)과 cites(p3, p2)뿐이며(kb.py의 57~58행), cites(p3, p1)은 없습니다. 그 단 하나의 몸체 원자가 귀결될 수 없으므로 이 갈래는 죽고, continue(56행)가 백트래킹합니다.
R2(이름 변경됨), 성공. $\text{citesTransitively}(A_2, C_2)$ $citesTransitively (A_{2}, C_{2})$ 를 목표와 단일화합니다: $\{A_2 \mapsto \text{p3},\ C_2 \mapsto \text{p1}\}$ ${A_{2} \mapsto p3, C_{2} \mapsto p1}$ . 몸체는 cites(p3, B_2) $\wedge$ $\land$ citesTransitively(B_2, p1)이 됩니다.
- cites(p3, B_2)는 사실 cites(p3, p2)에 대해 귀결되어 $\{B_2 \mapsto \text{p2}\}$ 를 바인딩합니다.
- citesTransitively(p2, p1)이 재귀합니다. 이번에는 R1이 발동합니다: 그 몸체 cites(p2, p1)이 바로 하나의 사실이므로, 하위 목표는 즉시 닫힙니다.

렌더링된 트리는 실제 출력과 일치하며, 조부 지도교수 트리보다 정확히 한 단계 더 높습니다:

  citesTransitively(p3, p1)
    cites(p3, p2)
    citesTransitively(p2, p1)
      cites(p2, p1)

cites(p3, p1)에 대한 죽은 R1 시도는 출력된 트리에 나타나지 않는데, 오직 성공한 경로만이 기록되기 때문입니다. 그러나 그것은 탐색이 실제로 수행했다가 되돌린 진짜 작업입니다. 절을 시도하고, 실패하고, 되돌아가서, 다음 것을 시도하는 이 상호작용이 후방 연쇄 제어 흐름의 전부이며, 그것은 if s is None: continue라는 두 줄 안에 살아 있습니다.

질의 응답: 모든 바인딩 열거하기

목표 안의 변수를 바인딩되지 않은 채로 남겨 두면, 예/아니오 증명이 하나의 질의(query)로 바뀝니다: "어떤 값들에 대해 이것이 증명 가능한가?" answers 함수(82~93행)는 목표를 증명하는 모든 치환을 모아 그 결과로 나온 접지 원자들을 보고하며, 각 해(solution)는 목표 변수들의 바인딩(binding)입니다 [3]. 동반 예제는 alice의 동료(colleague)들을 묻습니다:

print("colleagues of alice:", answers(("colleague", "alice", "Who")))

colleagues of alice: [('colleague', 'alice', 'bob')]

답은 bob 하나이며, 탐색 트리는 정확히 왜 하나만 살아남는지를 설명해 줍니다. 규칙(kb.py의 82~83행)은 $\text{colleague}(X, Y) \leftarrow \text{affiliated}(X, I) \wedge \text{affiliated}(Y, I) \wedge \text{neq}(X, Y)$ 입니다. 그 머리를 목표 colleague(alice, Who)와 단일화하면 $\{X_1 \mapsto \text{alice},\ Y_1 \mapsto \text{Who}\}$ 가 바인딩되고, 몸체는 세 개의 하위 목표가 됩니다: affiliated(alice, I_1), affiliated(Who, I_1), neq(alice, Who). 이들을 왼쪽에서 오른쪽으로 추적해 봅시다:

affiliated(alice, I_1): alice의 유일한 소속 사실은 affiliated(alice, mit)이므로, $\{I_1 \mapsto \text{mit}\}$ 입니다.
affiliated(Who, mit): 두 번째 인자로 mit을 갖는 사실이 둘 있습니다, affiliated(alice, mit)과 affiliated(bob, mit)이며, 그리하여 탐색은 $Who \mapsto \text{alice}$ $W h o \mapsto alice$ 와 $Who \mapsto \text{bob}$ $W h o \mapsto bob$ 으로 갈라집니다.
- 갈래 $Who \mapsto \text{alice}$ : 가드 neq(alice, alice)가 검사됩니다. 코드에서 이 가드는 양쪽 모두가 변수가 아니면서 같지 않을 때에만 발동합니다; 여기서는 둘이 같으므로 조건 x != y가 거짓이 되어 아무것도 산출되지 않고 이 갈래는 죽습니다.
- 갈래 $Who \mapsto \text{bob}$ : 가드 neq(alice, bob)가 통과되고( $\text{alice} \ne \text{bob}$ ), 분해절이 비게 되어, colleague(alice, bob)이 기록됩니다.

그 가드 neq는 유일한 비사실(non-fact) 술어입니다: 이는 지식 베이스에서 조회되는 것이 아니라 sld.py의 45~50행에서 엔진에 의해 직접 검사됩니다:

    if g[0] == "neq":  # built-in inequality guard
        x, y = walk(g[1], sub), walk(g[2], sub)
        if not is_var(x) and not is_var(y) and x != y:
            for s2, proofs in _solve(rest, sub, rules, counter):
                yield s2, [Proof(g, [])] + proofs
        return

후방 연쇄는 모든 사람 쌍을 열거하지 않았습니다; 그것은 alice에서 출발해 그녀의 소속 기관을 고정한 다음, 그 규칙을 충족시킬 수 있는 mit 소속 관계들만을 따라갔으며, 가드가 그것을 발견하는 순간 반사적인(reflexive) 쌍을 가지치기했습니다. 대칭성도 확인됩니다: answers(("colleague", "bob", "Who"))는 [('colleague', 'bob', 'alice')]를 돌려주는데, alice와 bob이 mit에 있는 유일한 두 사람이기 때문입니다. 완전히 열린 질의도 같은 메커니즘으로 열거됩니다. answers(("grandAdvisor", "alice", "Z"))를 물으면 grandAdvisor(alice, carol)과 grandAdvisor(alice, dave)가 모두 돌아오는데, alice는 bob을 지도하고, bob은 carol과 dave 둘 다를 지도하기 때문입니다; 양쪽 인자를 모두 열어 answers(("grandAdvisor", "A", "B"))를 물으면 grandAdvisor(bob, erin)(bob은 carol을 지도하고, carol은 erin을 지도합니다)이 더해져 모두 세 개의 조부 지도 쌍이 됩니다. 각각은 같은 탐색의 서로 다른 성공적인 갈래이며, 오직 그 단일화가 어떤 사실들에 안착했는지에 의해서만 구분됩니다.

전방 대 후방: 두 방향, 하나의 의미

이제 우리는 두 엔진을 모두 갖추었으며, 이 둘은 반대편 끝에서 출발해 같은 진리들을 계산해 냅니다. 전방 연쇄(forward chaining)는 사실들로부터 모든 결론을 향해 밀고 나갑니다; 학계 세계에서는 크기가 커지다가 이내 안정되는 세 번의 물결 만에 전체 모델에 도달합니다:

least fixpoint reached in 3 rounds; sizes per round: [23, 41, 47, 47]
47 atoms total, 24 derived.

24개의 유도된 원자 하나하나는 누군가 원하든 원하지 않든 실체화됩니다. 후방 연쇄(backward chaining)는 그 반대로 합니다: grandAdvisor(alice, carol)에 대해 그것이 만들어 내는 증명은 단 세 개의 원자에만 의존하며, 거기서 바닥을 이룹니다. 그 절충은 명확합니다. 전방 연쇄는 여러분이 안정적인 사실 집합에 대해 많은 질문을 던지려 할 때 이깁니다 — 모든 것을 한 번 유도해 두고, 그다음 각 질의에는 조회로 답하는 방식이며, 이는 정확히 데이터로그 데이터베이스가 자신의 규칙들을 실체화하는 방식입니다. 후방 연쇄는 여러분에게 하나의 목표, 혹은 채워야 할 변수가 있는 목표가 있고 그것에 답하기 위해 나머지 우주 전체를 계산하고 싶지 않을 때 이깁니다; 그것은 또한 자연스럽게 증명 트리를 만들어 내는 방식이기도 한데, 각 목표가 왜 성립했는지를 기록하기 때문입니다 [1].

두 방향 모두 이 프로그램에서는 종료하지만, 그 이유는 서로 다르며, 이는 제대로 짚고 넘어갈 가치가 있는 구분입니다. 전방 연쇄가 멈추는 것은 유한한 허브랜드 기저가 그 단조 연산자에 상한을 씌우기 때문입니다: 정해진 유한한 천장을 넘어 자랄 수 없는 집합은 반복을 멈추도록 강제하며, 이것이 정확히 [23, 41, 47, 47]이 보여주는 것입니다 — 성장한 다음 고정점에 이르는 것입니다. 후방 SLD는 일반적으로 그런 보장을 갖고 있지 않습니다. sld.py의 엔진은 자신이 이미 시도한 목표들을 전혀 기억하지 않으므로, 순환하는 데이터에 대한 재귀 규칙은 똑같은 유한한 원자들을 영원히 다시 유도하며 결코 돌아오지 못할 수도 있습니다; 유한한 허브랜드 기저는 그 자체만으로는 그런 순환을 막아 주지 않습니다. (실제 Prolog 시스템들은 정확히 이를 잡아내기 위해, 이미 시도한 목표들을 기억해 둠으로써, SLG 귀결이라고도 불리는 테이블링(tabling)을 추가합니다.)

그렇다면 후방 탐색은 여기서 왜 종료할까요? 재귀가 모든 재귀 호출마다 엄격히 감소하는 정초적 측도(well-founded measure)를 갖고 있기 때문입니다. 관계 cites는 비순환적(acyclic)입니다: 인용 사실들은 되돌아갈 방법이 없는 사슬 $\text{p3} \to \text{p2} \to \text{p1}$ 을 이룹니다. 각 논문에, 그로부터 뻗어 나가는 가장 긴 인용 경로의 길이와 같은 순위를 부여해 봅시다:

\text{rank}(\text{p1}) = 0, \qquad \text{rank}(\text{p2}) = 1, \qquad \text{rank}(\text{p3}) = 2.

간선 $A \to B$ 가 앞에 붙은, $B$ 에서 뻗어 나가는 가장 긴 경로는 곧 $A$ 에서 뻗어 나가는 하나의 경로이므로, 어떤 인용 간선이든 $\text{rank}(B) \lt \text{rank}(A)$ 를 강제합니다. 규칙 R2는 cites(A, B)가 방금 확립된 경우에 한해서만 citesTransitively(B, C)에 대해 재귀하므로, 첫 번째 인자의 순위는 재귀 단계마다 최소한 하나씩 떨어집니다. 음이 아닌 정수들의 엄격히 감소하는 수열은 무한할 수 없으므로, 재귀 깊이는 (여기서는 $\text{rank}(\text{p3}) = 2$ 에 의해) 유계이며 — 이것이 바로 이 장에서 가장 깊은 트리가 세 개의 원자 높이인 이유입니다 — 후방 탐색은 멈춥니다. 이 프로그램에서 순수한 SLD를 구해 주는 것은 유한한 허브랜드 기저가 아니라 비순환적인 데이터입니다.

아직 풀리지 않은 부분

SLD 귀결은 그 일치 판정 능력만큼만 훌륭하며, 그 일치 판정은 설계상 부서지기 쉽습니다(brittle by design). 단일화는 오직 정확한 기호적 일치에서만 성공합니다: advises는 advises와 단일화되며, 사람이 보기에는 거의 동의어인데도 mentors나 supervises와는 결코 단일화되지 않고, 서로 다른 두 상수는 그저 충돌할 뿐입니다 — 우리가 carol과 bob이 그렇게 하는 것을 지켜본 것처럼 말입니다. 만약 어떤 사실이 규칙과 아주 조금이라도 다르게 표현되어 있다면, 혹은 지식 베이스에 아예 빠져 있다면, 그 증명 갈래는 죽어 버리며, 어떤 근사한 실패(near-miss)도 그것을 구해 낼 수 없습니다. 그것이 확실성의 대가입니다: 모든 증명은 빈틈이 없지만, 오직 정확히 적어 놓은 기호들에 대해서만 그렇습니다. 이후의 권들이 다루는 열린 질문은, 기계가 목표, 규칙, 재귀, 증명 트리라는 이 추론의 형태를 유지하면서도, 전부 아니면 전무인 일치 판정을 완화할 수 있는가입니다. 4권의 신경망 정리 증명(neural theorem proving)은 소프트 단일화(soft unification)로 답합니다: 각 기호를 하나의 벡터로 표현하고, unify.py의 35행에 있는 엄격한 동등성 검사 x == y를 유사도(similarity) 점수로 대체하여, advises와 mentors가 그 임베딩(embedding)이 가까운 정도만큼 일치할 수 있게 합니다. 증명 트리는 살아남지만, 이제 그것은 보장이 아니라 확신도(confidence)를 지니게 됩니다 — 정확한 일치의 확실성을, 순수하게 기호적인 엔진을 무너뜨리는 근사한 실패와 빈틈들을 가로질러 무언가를 증명해 낼 수 있는 능력과 맞바꾸는 것입니다.

왜 중요한가

SLD 귀결은 이 시리즈의 모든 "미분 가능한 증명기"(differentiable prover)가 모방하려 애쓰는 또렷한 표적입니다. 뉴로-심볼릭 시스템은, 상당 부분, 여기서 드러난 두 가지 미덕 — 목표 지향성(goal-directedness, 질문이 필요로 하는 것만 쫓는 것)과 감사 가능성(auditability, 그저 답이 아니라 증명 트리를 남기는 것) — 을 지키면서, 정확한 일치를 깨뜨리는 잡음(noise), 동의어 관계(synonymy), 불완전성(incompleteness)에서도 살아남으려는 시도입니다. 심볼릭 증명이 어떠했어야 하는지를 알지 못하면 어떤 신경망 증명기가 충실한지 판단할 수 없으며, 이 장이 바로 그 기준점입니다: 단일화가 찾아내는 정확한 치환, 귀결이 밟아가는 정확한 분해절 수열, 질의가 돌려주는 정확한 바인딩입니다. 4권이 unify를 벡터 유사도로 부드럽게 만들 때, 그것이 부드럽게 만드는 대상은 바로 여러분이 방금 추적한 스무 줄입니다.

핵심 용어

후방 연쇄(Backward chaining) — 어떤 규칙이 목표를 결론으로 이끌어낼 수 있는지 물으면서 그 규칙의 몸체에 대해 재귀하여 목표를 증명하는 것으로, 모든 갈래가 사실에 도달하면 멈춥니다; 전방 연쇄와는 반대 방향입니다.
SLD 귀결(SLD resolution) — 한정절에 대한 선택적 선형 귀결(Selective Linear resolution for Definite clauses): 혼 절에 특화된 로빈슨의 귀결 규칙으로, Prolog 뒤에 있는 증명 절차입니다.
확정절(혼 절)(Definite (Horn) clause) — 정확히 하나의 양의 머리 원자를 갖는 규칙 $H \leftarrow B_1 \wedge \cdots \wedge B_n$ 입니다; 논리적으로는 $H \vee \neg B_1 \vee \cdots \vee \neg B_n$ 입니다.
목표 / 질의(Goal / query) — 머리가 없는 절 $\leftarrow G_1 \wedge \cdots \wedge G_m$ 로, 증명하고자 하는 것의 부정으로 읽습니다; 그 안에 변수를 남겨 두면 그것을 증명하는 모든 바인딩을 열거하게 됩니다.
분해절(Resolvent) — 아직 증명해야 할 현재의 목표 목록입니다; 각 SLD 단계는 선택된 원자를 인스턴스화된 규칙의 몸체로 치환하며, 빈 분해절 $\square$ 에 도달하면 논박이 완결됩니다.
논박(Refutation, $P \vdash G$ , $P \models G$ ) — $G$ 의 부정을 가정하고 빈 절을 도출함으로써 $G$ 를 증명하는 것입니다; 건전성이란 도출( $\vdash$ )이 함의( $\models$ )를 함의한다는 것입니다.
단일화 / 단일자 / MGU(Unification / unifier / MGU) — 두 원자를 동일하게 만드는 가장 일반적인 치환을 찾아내거나, 그럴 수 없을 때 실패하는(충돌, clash) 연산입니다.
치환(Substitution) — 변수에서 항으로의 대응이며 $\mapsto$ 로 씁니다; 바인딩(binding)은 그런 변수-항 항목 하나를 가리키며, $\circ$ 는 증명 갈래를 따라 치환들을 합성합니다.
발생 검사(Occurs-check) — 함수 기호가 있을 때에만 필요한 가드로, 어떤 변수가 자신을 포함하는 항에 바인딩되는 것을 막습니다; 함수 없는 데이터로그에서는 필요하지 않습니다.
분리 표준화(Standardize apart, rename) — 사용하기 전에 규칙의 변수들에 새로운 이름을 찍어 두어, 한 규칙을 두 번 적용하더라도 결코 변수를 공유하지 않도록 하는 것입니다.
증명 트리(Proof tree) — 목표들과 그것을 확립한 하위 목표들의 중첩된 기록입니다; 단순한 진릿값이 아니라 감사 가능한 자취입니다.
허브랜드 기저(Herbrand base) — 프로그램의 상수들로부터 형성될 수 있는 접지 원자들의 유한 집합입니다; 그 유한성이 바로 전방 연쇄가 종료하는 이유이며, 반면 후방 SLD는 대신 비순환적인 데이터(정초적 순위)나 테이블링에 의지합니다.
테이블링(Tabling, SLG resolution) — 실제 Prolog가 순수한 SLD에 추가하는 순환 검사 원칙으로, 이미 시도한 목표들을 기억해 두어 순환하는 데이터에 대한 재귀 규칙이 영원히 맴돌 수 없게 합니다.
소프트 단일화(Soft unification) — 정확한 기호 동등성을 벡터 유사도로 대체하는 4권의 방식으로, 근사한 동의어들이 어느 정도 일치할 수 있게 하되 확실성을 도달 범위와 맞바꿉니다.

이 다음으로 이어지는 것

우리는 추론이 양방향으로 실행되는 것을 지켜보았습니다 — 전방으로는 전체 모델까지, 후방으로는 하나의 증명까지 — 그리고 두 경우 모두 무언가가 정착(settle)되었습니다: 전방 체이스는 47개 원자에서 자라기를 멈추었고, 후방 탐색은 그 순위가 더 이상 떨어질 수 없게 되었을 때 사실에서 바닥을 이루었습니다. 다음 장인 고정점: 극한에 도달하는 것으로서의 추론은 그 정착 아래에 놓인 수학에 이름을 붙입니다: 즉시 결과 연산자(immediate-consequence operator), 그것이 올라가는 최소 고정점, 그리고 그런 극한이 언제나 존재하고 유일함을 보장하는 순서-격자(order-and-lattice) 이론입니다. 이는 "아무것도 바뀌지 않을 때까지 규칙을 계속 적용한다"는 것이 희망이 아니라 하나의 정리(theorem)인 형식적인 이유이며, 2권의 기술 논리 추론기가 그대로 재사용할 형태이기도 합니다.

이 장에서 다루는 내용​

목표 지향적 증명: 질문에서 출발하기​

단일화: 일치 여부를 결정하는 기본 연산​

추적해보는 루프​

도출된 SLD 귀결 단계​

분해절 수열로서의 증명​

증명 트리: 감사 가능한 자취​

추적해보는 재귀와 백트래킹​

질의 응답: 모든 바인딩 열거하기​

전방 대 후방: 두 방향, 하나의 의미​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 다음으로 이어지는 것​