추론과 증명: 사실의 연쇄로 결론에 이르기

📍 우리가 있는 곳: 2부 · 계산으로서의 추론 — 5장. 일차 논리는 어떤 문장이 한 세계에서 참이라는 것이 무엇을 의미하는지 알려주었고, holds()로 모든 개체를 훑어 이를 검사했습니다. 이제 우리는 의미에서 메커니즘으로 방향을 돌려, 기계가 낡은 사실을 단순히 검사하는 대신 새로운 사실을 도출하게 합니다.

이전 장은 우리에게 작동은 하지만 묘하게 수동적인 진리의 그림을 남겼습니다. 완성된 세계와 하나의 문장을 추론기에 건네주면, 추론기는 모든 개체를 훑어 예 또는 아니오로 답합니다. 이것은 검사이며, 세계가 이미 완결되어 있다고 전제합니다. 진짜 추론은 그 반대의 일을 합니다. 그것은 세계를 키워나갑니다. 소수의 단언된 사실과 규칙의 집합을 취하여 그 규칙들이 강제하는 모든 결론을 만들어냅니다. 이 장은 하나의 주장을 정밀하게 세운 뒤 이를 증명합니다. 추론은 기계적인 규칙 적용이며, 어떤 사실을 만들어낸 규칙 발화의 자취가 곧 그 사실의 증명이라는 것입니다. 우리는 "귀결을 도출한다"를 블랙박스로 다루지 않을 것입니다. 규칙을 사실들과 맞추는 단 하나의 기본 연산을 정의하고, 도출을 수행하는 단 하나의 연산자를 정의하며, 이 둘이 진행 중인 예제 위에서 사실 하나하나씩 움직이는 것을 지켜보고, 이들이 계산하는 것이 너무 적지도(귀결되는 것이 하나도 빠지지 않음) 너무 많지도(거짓이 하나도 섞여 들지 않음) 않음을 증명할 것입니다.

쉽게 말하면

도미노로 가득 찬 방을 상상해 보세요. 각 도미노에는 "누군가 학생이면 그는 연구자다"와 같은 규칙이 적혀 있습니다. 도미노는 자신이 기다리던 모든 사실이 이미 서 있게 되는 순간 넘어집니다. 여러분은 그저 전해 들은 사실들, 즉 처음 몇 개의 도미노를 손으로 직접 넘어뜨리고, 그다음에는 그저 지켜보기만 하면 됩니다. 쓰러지는 도미노 하나하나가 다음 도미노를 넘어뜨리고, 물결이 이어지고 이어지다가, 더 이상 아무것도 넘어질 수 없을 때 방은 잠잠해집니다. 여기서 두 가지가 나옵니다. 여러분은 규칙이 허용하는 모든 결론을 발견한 것입니다. 그리고 어떤 사실이든 원하는 것을 골라, 그것을 넘어뜨린 정확한 도미노의 연쇄를 거꾸로 추적할 수 있으며, 그 연쇄가 바로 증명입니다.

이 장에서 다루는 내용

추론의 원자로서의 추론 규칙: 기호 하나하나 풀어낸 전건 긍정법(modus ponens), 그리고 증명이란 결국 규칙 적용의 유한한 연쇄에 지나지 않는 이유.
단일화(unification)의 도출과 추적: 치환(substitution), 결속 사슬을 풀어내는 walk, 그리고 규칙 본문이 사실과 맞는지를 논항 단위로 판정하는 unify를, 실제 매칭 사례와 실제 충돌 사례에서 한 단계씩 실행해 봅니다.
전방 연쇄(forward chaining)의 형식화: 집합 방정식으로 쓴 즉각귀결 연산자(immediate-consequence operator) $T_P$ 를 실제 t_p와 한 줄씩 대조하고, 그 정의로부터 두 가지 구조적 성질(단조성, 팽창성)을 증명합니다.
루프가 멈춰야 하는 이유: 우리 세계에 대해 정확히 헤아린 유한한 허브랜드 기저(Herbrand base, 가능한 원자 1404개)가 반복 횟수에 확고한 상한을 제공합니다.
한 차례의 스윕과 세 개의 증명 트리: $T_P$ 의 한 차례 전체 적용을 치환 하나하나씩 추적한 뒤, person(erin), 하나의 grand-advisor 관계, 하나의 추이적 인용을 실제 도출로서 구성합니다.
물결은 곧 증명의 깊이다: 크기 자취 [23, 41, 47, 47]을 "물결마다 추론 단계가 하나씩 늘어난다"로 다시 읽고, 각 물결의 모든 원자를 남김없이 설명합니다.
건전성과 완전성의 증명: 귀납법으로 전방 연쇄가 귀결되는 사실만을 도출함을 보이고, 모델 이론적 논증으로 귀결되는 사실을 모두 도출함을 보입니다. 이것이 바로 도출된 모델을 신뢰할 수 있는 이유입니다.
증명의 두 방향과, 극한까지 반복하는 이 엔진이 온전한 수학적 다룸을 받는 고정점(Fixpoints) 장으로의 안내.

추론 규칙: 추론의 가장 작은 움직임

추론의 원자는 추론 규칙(inference rule)입니다. 이미 가지고 있는 전제로부터 이제 추가해도 되는 결론으로 나아가는, 정당화된 움직임입니다. 가장 오래되고 가장 중요한 것은 전건 긍정법(modus ponens, 라틴어로 "긍정하는 방식")입니다. 사실 $P$ 와 규칙 $P \to Q$ 로부터 $Q$ 를 결론지을 수 있습니다 [1]. 여기에는 두 개의 연산이 등장하며, 이를 딛고 서기 전에 둘 다 풀어 볼 가치가 있습니다. 화살표 $\to$ 는 실질 함의(material implication)로, "왼쪽이 성립하면 오른쪽이 성립한다"로 읽습니다. 문장 $P \to Q$ 는 $P$ 와 $Q$ 가 어떻게 연결되어 있는지에 대한 하나의 단일한 주장일 뿐, 무언가를 하라는 지시가 아닙니다. 전건 긍정법이 바로 그 지시입니다. 그것은, 왼쪽의 사실 $P$ 가 그 자체로 이미 성립함을 여러분이 동시에 가지고 있다면, 오른쪽의 사실 $Q$ 를 얻은 것이라고 말합니다. 한 줄로 쓰면, 가로줄은 "위에 있는 것들로부터 아래에 있는 것을 결론짓는다"로 읽습니다.

\frac{P \qquad P \to Q}{Q}.

우리의 학술 세계는 정확히 이 움직임 위에서 돌아갑니다. kb.py의 규칙들(76행과 77행) 가운데는 학생은 연구자라는 규칙과, 연구자는 사람이라는 규칙이 있습니다.

(("researcher", "X"), [("student", "X")]),
(("person", "X"), [("researcher", "X")]),

여기서 X는 변수(variable)입니다(대문자로 시작하는 것으로, 진행 중인 예제가 is_var에서 고정한 관례에 따릅니다. kb.py 25–28행: 어떤 항이 대문자로 시작하는 비어 있지 않은 문자열일 때, 정확히 그때 그 항은 변수입니다). 각 규칙은 혼 규칙(Horn rule)입니다. 왼쪽에 하나의 양성 헤드 원자, 오른쪽에 양성 본문 원자들의 논리곱이 오며, "모든 본문 원자가 성립하면 헤드가 성립한다"로 읽습니다. 본문 원자들을 잇는 기호 $\land$ 는 논리곱(conjunction), 평이한 "그리고"입니다. $b_1 \land b_2$ 는 $b_1$ 과 $b_2$ 가 모두 참일 때 정확히 참입니다. 사실(fact)은 본문이 비어 있는 혼 규칙의 특수한 경우일 뿐입니다. 먼저 성립해야 할 것이 아무것도 없으므로, 그것은 무조건 성립합니다. 규칙을 발화시키려면 치환(substitution)이 필요합니다. 규칙의 변수를 상수로 대응시켜 본문이 우리가 이미 가진 사실과 맞아떨어지게 만드는 대응입니다. 치환은 그리스 문자 $\sigma$ (시그마)로 쓰고, $b\sigma$ 는 "원자 $b$ 에 $\sigma$ 를 그 변수들에 적용한 것"을 나타냅니다. 기저 사실 student(erin)이 주어지면, 치환 $\sigma = \{X \mapsto \text{erin}\}$ ("~로 보내진다"라고 읽는 매플릿 $\mapsto$ )은 첫 번째 규칙의 본문 student(X)를 우리가 가지고 있는 student(erin)으로 바꾸어 주므로, 전건 긍정법이 우리에게 researcher(erin)을 건네줍니다. 그 $\sigma$ 를 기계적으로 찾아내는 것이 unify라는 루틴이 하는 일이며, 이는 다음 절에서 온전히 구성해 봅니다.

증명(proof, 또는 도출(derivation))은 그렇다면 원자들의 유한한 수열 $A_1, A_2, \ldots, A_m$ 으로서, 그 안의 모든 원자가 기저 사실이거나, 아니면 본문 원자 $b_1\sigma, \ldots, b_k\sigma$ 가 모두 수열 안에서 더 앞서 등장하는 어떤 규칙 $h \leftarrow b_1, \ldots, b_k$ 의 헤드 $h\sigma$ 인 것입니다. 규칙의 화살표 $\leftarrow$ 는 결론을 먼저 쓴, 헤드에서 그것이 딛고 선 조건들로 거슬러 가리키는 동일한 함의입니다. 마지막 원자 $A_m$ 이 증명된 대상이고, 수열 전체가 그 증거입니다. 여기에는 창의적인 것이 전혀 없습니다. 이는 기계가 판단 없이도 해낼 수 있는 장부 정리이며, 그 기계적인 성질이야말로 이 장 전체의 핵심입니다.

단일화: 규칙을 사실과 맞추는 기본 연산

규칙이 발화하기 전에 우리는 더 작은 질문 하나를 해결해야 합니다. 이 규칙의 본문이 우리가 가진 사실과 맞아떨어지는가, 그리고 만약 그렇다면 그 변수들을 어떻게 결속시켜야 하는가? 그 맞춤 작업이 바로 단일화(unification)이며, 이 책의 두 추론 엔진이 공유하는 단 하나의 기본 연산입니다. 이는 그 자체로 도출해 볼 가치가 있습니다. 왜냐하면 앞으로 나올 자취 속의 모든 발화는 작은 단일화들의 더미이며, 다음 장의 후방 엔진에서도 동일한 루틴이 변함없이 다시 등장하기 때문입니다.

어휘를 다시 떠올려 봅시다. 항(term)은 상수(constant, bob이나 p1처럼 하나의 고정된 개체를 나타내는 소문자 이름)이거나 변수(variable, X처럼 "아직 확정되지 않은 어떤 개체"를 나타내는 대문자 이름)입니다. 원자(atom)는 항들의 튜플에 적용된 술어로, 파이썬 튜플 (pred, arg1, arg2, ...)로 저장됩니다. 치환(substitution) $\sigma$ 는 변수에서 항으로 가는 유한한 대응입니다. 코드에서는(unify.py, 파일 맨 위에 설명되어 있듯) "변수 이름을 항에 대응시키는 평범한 dict"이며, 그래서 치환 $\{X \mapsto \text{bob},\, Y \mapsto \text{carol}\}$ 은 문자 그대로 딕셔너리 {'X': 'bob', 'Y': 'carol'}입니다.

두 원자를 단일화한다는 것은 그 둘을 동일하게 만드는 치환을 찾는 일입니다. 루틴 unify(unify.py 23–43행)는 이를 논항 하나하나씩 처리합니다.

def unify(a, b, sub=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
    return sub

이를 네 개의 움직임으로 읽어 봅시다. 30행은 넘겨받은 치환을 복사하므로, 실패한 시도가 호출자의 결속을 결코 오염시키지 않습니다. 31행은 빠른 기각 조건입니다. 두 원자가 술어 이름 a[0]에서 다르거나 항수(arity, 논항의 개수, len(a))에서 다르면 결코 같아질 수 없으므로, 함수는 "단일자가 존재하지 않는다"로 읽히는 None을 반환합니다. 그다음 루프는 두 논항 목록을 나란히 훑습니다. 각 쌍에 대해 walk(16–20행)는 먼저 각 항을 그것이 현재 나타내는 것으로 풀어내는데, sub에 이미 있는 결속의 사슬을 끝까지 따라갑니다. walk 안의 while이 바로 그 추적입니다. 항이 sub의 키로 등장하는 변수인 한, 그것을 결속된 값으로 바꾸고 다시 살펴보며, 상수이거나 결속되지 않은 변수인 첫 항에서 멈춥니다. 그런 다음 세 가지 경우가 그 쌍을 결정합니다. 풀어낸 두 항이 이미 같다면 할 일이 없으므로 계속 진행합니다. 한쪽이 변수라면 그것을 다른 쪽에 결속시켜 $\sigma$ 를 한 항목만큼 확장합니다. 양쪽이 서로 다른 상수라면 충돌이 일어나 단일화 전체가 실패합니다. 모든 논항을 무사히 통과하면 43행이 확장된 치환을 반환합니다.

grandAdvisor 규칙이 필요로 하는 바로 그 매칭, unify(("advises","X","Y"), ("advises","bob","carol"), {})에서 이를 추적해 봅시다.

단계	풀어낸 쌍 $(x, y)$	촉발된 경우	이후의 치환
시작	—	—	`{}`
술어/항수	`advises` 대 `advises`, 둘 다 항수 2	31행 통과, 계속	`{}`
논항 1	`X` 대 `bob`	`is_var(x)`: `X` 결속	`{'X': 'bob'}`
논항 2	`Y` 대 `carol`	`is_var(x)`: `Y` 결속	`{'X': 'bob', 'Y': 'carol'}`

결과 $\{X \mapsto \text{bob},\, Y \mapsto \text{carol}\}$ 는 정확히 본문 원자 advises(X, Y)를 기저 사실 advises(bob, carol)로 바꾸어 주는 결속입니다. 이제 충돌을 지켜봅시다. 이는 엔진이 막다른 길을 쳐내는 방식입니다. 이 두 결속을 이미 손에 쥔 채로, 규칙의 두 번째 본문 원자 advises(Y, Z)를 사실 advises(bob, carol)에 맞춰 보려 한다고 합시다. 첫 번째 논항 쌍은 (Y, bob)입니다. walk은 Y를 carol로 풀어내고, 사실은 상수 bob을 제공하는데, carol과 bob은 서로 다른 두 상수이므로 42행은 None을 반환하고 이 짝짓기는 조용히 버려집니다. 따라서 첫 번째 원자가 만든 결속은 두 번째 원자가 맞출 수 있는 것을 제약하며, 이것이 바로 다음에 지켜볼 조인의 전체 메커니즘입니다.

apply_sub(46–48행)은 unify의 거울상입니다. 완성된 치환이 주어지면 원자의 모든 논항을 훑어 결속된 각 변수를 그 값으로 바꾸어, 규칙 헤드 ("grandAdvisor","X","Z")를 $\{X\mapsto\text{bob},\, Z\mapsto\text{erin}\}$ 아래에서 접지된 원자 ("grandAdvisor","bob","erin")로 만들어 줍니다. 결속을 찾기 위해 단일화하고, 새 사실을 만들기 위해 그것을 적용합니다. 이 한 쌍의 단계가 코드 속 전건 긍정법 한 번의 전부이며, 그 위에서 벌어지는 모든 일은 그저 이를 여러 번 반복하는 것일 뿐입니다.

전방 연쇄의 형식화: 즉각귀결 연산자

전건 긍정법은 하나의 규칙을 한 번 발화시킵니다. 전방 연쇄(forward chaining)는 이를 남김없이 해냅니다. 본문이 현재 충족되는 모든 규칙을 발화시키고, 모든 새 헤드를 모아, 새로운 사실이 더 이상 나타나지 않을 때까지 반복합니다 [1]. "지금 적용 가능한 모든 것을 발화시킨다"는 한 차례의 완전한 스윕이 바로 즉각귀결 연산자(immediate-consequence operator)로, $T_P$ 라고 쓰며 흔히 프로그램 $P$ 가 사실 집합에 가하는 변환으로 읽습니다 [2]. 이를 하나의 집합 방정식으로 쓸 수 있습니다. $S$ 를 현재의 접지 원자 집합이라 합시다. 그러면

T_P(S) \;=\; S \;\cup\; \bigl\{\, h\sigma \;:\; (h \leftarrow b_1, \ldots, b_k) \in P,\ \sigma \text{ a substitution},\ b_i\sigma \in S \text{ for all } i = 1, \ldots, k \,\bigr\}.

각 조각을 풀어 봅시다. 합집합 기호 $\cup$ 는 "두 모음을 하나의 집합으로 함께 던져 넣는다"는 뜻입니다. 중괄호 $\{\,\cdot : \cdot\,\}$ 는 집합 구성 표기(set-builder notation)로, 콜론 앞의 모든 것은 원소의 형태이고, 콜론 뒤의 모든 것은 그것이 만족해야 하는 조건이며, 콜론은 "다음을 만족하는"으로 읽습니다. 소속 기호 $\in$ 는 "~의 원소이다"로 읽으므로, $b_i\sigma \in S$ 는 치환된 본문 원자가 우리가 현재 가진 사실들 가운데 하나라는 뜻이고, $(h \leftarrow b_1, \ldots, b_k) \in P$ 는 그 규칙이 프로그램의 규칙들 가운데 하나라는 뜻입니다. "모든 $i = 1, \ldots, k$ 에 대하여"라는 한정어구는 그 규칙의 모든 본문 원자에 걸쳐 있습니다. 곧 사용하게 될 기호 $\forall$ 는 그 줄임 표기이며 단순히 "모든 ~에 대하여"로 읽습니다. 이 줄 전체를 우리말로 읽으면: $T_P(S)$ 는 우리가 이미 가지고 있던 사실들에, 규칙 본문 전체를 $S$ 안에서 참으로 만드는 치환 하나를 찾아 만들어 낼 수 있는 모든 헤드를 더한 것입니다. forward_chain.py(42–49행)의 정의는 그 문장을 거의 그대로 옮겨 적은 것입니다.

def t_p(facts: set, rules: list) -> set:
    """One application of the immediate-consequence operator: the input facts
    plus every head derivable in a single step."""
    out = set(facts)
    for head, body in rules:
        for sub in _match_body(body, facts, {}):
            out.add(apply_sub(head, sub))
    return out

45행 out = set(facts)는 $S \cup \{\cdot\}$ 에 해당하는 부분입니다. 출력은 우리가 가지고 있던 모든 것의 사본으로 시작합니다. 이중 루프는 집합 구성 표기를 절차적으로 바꾼 것입니다. 모든 규칙에 대해 _match_body(19–39행)는 현재 사실들에 맞서 본문 전체를 충족시키는 모든 치환 sub를 산출하는데, 원자를 왼쪽에서 오른쪽으로 맞추며 위에서 unify가 했던 것과 정확히 같은 방식으로 진행 중인 $\sigma$ 를 확장해 나갑니다. 그런 다음 out.add(apply_sub(head, sub))가 치환된 헤드 $h\sigma$ 를 만들어 추가합니다. $T_P$ 의 두 가지 구조적 성질이 이 정의로부터 곧바로 따라 나오며, 둘 다 나중에 중요한 역할을 합니다.

$T_P$ 는 팽창적입니다: 항상 $S \subseteq T_P(S)$ 입니다. 기호 $\subseteq$ 는 "~의 부분집합이거나 같다"로 읽으며, 왼쪽 집합의 모든 원소가 오른쪽 집합에도 있다는 뜻입니다. 이는 45행이 무언가 추가되기 전에 out을 facts 전체로 채워 넣기 때문에 성립하며, 그래서 어떤 입력 사실도 결코 사라지지 않습니다. 따라서 $T_P$ 를 반복하면 집합은 오직 커질 수만 있습니다.

$T_P$ 는 단조적입니다: $S \subseteq S'$ 이면 $T_P(S) \subseteq T_P(S')$ 입니다. 다음은 방정식으로부터 곧바로 나오는 증명입니다. 임의의 원자 $A \in T_P(S)$ 를 취합시다. 두 가지 경우가 있습니다. $A \in S$ 라면, $S \subseteq S'$ 이므로 $A \in S' \subseteq T_P(S')$ 이고, 끝입니다. 그렇지 않다면 $A = h\sigma$ 이며, 이때 어떤 규칙의 본문 원자들이 모두 $b_i\sigma \in S$ 를 만족합니다. $S \subseteq S'$ 이므로 그 동일한 원자들은 $b_i\sigma \in S'$ 도 만족하고, 따라서 동일한 발화가 $S'$ 위에서도 가능하여 $A = h\sigma \in T_P(S')$ 입니다. 어느 경우든 $A \in T_P(S')$ 이므로 $T_P(S) \subseteq T_P(S')$ 입니다. 사실을 추가하는 것은 결코 결론을 제거하지 않습니다. 더 큰 입력은 더 큰 출력을 냅니다.

아무것도 새로 나타나지 않는 지점까지 $T_P$ 를 반복하는 구동기가 least_fixpoint입니다(forward_chain.py 52–63행).

def least_fixpoint(facts, rules, trace: bool = False):
    current = set(facts)
    sizes = [len(current)]
    while True:
        nxt = t_p(current, rules)
        sizes.append(len(nxt))
        if nxt == current:
            return (current, sizes) if trace else current
        current = nxt

이 루프는 $S_0$ 을 기저 사실로 하고 $S_{n+1} = T_P(S_n)$ 인 사슬 $S_0, S_1, S_2, \ldots$ 를 만들어 나갑니다. $T_P$ 가 팽창적이므로 이 사슬은 $S_0 \subseteq S_1 \subseteq S_2 \subseteq \cdots$ 처럼 상승하며, 어떤 스윕이 아무것도 바꾸지 못하는 순간, 즉 nxt == current인 순간 멈춥니다. 멈추는 지점의 집합이 고정점(fixpoint)입니다. 즉 $T_P(S) = S$ 인 집합 $S$ 이며, 이는 한 번 더 스윕해도 새로운 것이 나오지 않는다는 뜻입니다. 기저 사실로부터 도달 가능한 가장 작은 고정점이 최소 고정점(least fixpoint)이며, $\mathrm{lfp}(T_P)$ 라고 씁니다. 혼 프로그램에 대해서는 이것이 정확히 그 프로그램의 최소 허브랜드 모델(least Herbrand model), 즉 모든 규칙을 참으로 만드는 최소한의 접지 원자 집합과 일치합니다 [2]. 이 주장은 건전성-완전성 절에서 정밀하게 다듬어 사용합니다.

루프가 반드시 멈추는 이유

while True는 데이터로그 프로그래머를 결코 불안하게 하지 않으며, 여기 그 정확한 이유가 있습니다. 규칙들이 만들어 낼 수 있는 모든 것은 허브랜드 기저(Herbrand base) $B$ 안에 살고 있습니다. 이는 프로그램의 술어와 유한한 개수의 상수로부터 만들 수 있는 모든 접지 원자의 집합입니다. 우리 세계에 대해 이를 세어 봅시다. 상수(kb.py 32–35행)는 사람 5명, 논문 3편, 기관 2곳, 주제 3개이므로 $|C| = 13$ 입니다(막대 기호 $|\cdot|$ 는 집합의 크기, 즉 원소의 개수를 나타냅니다). 술어는 단항 술어 네 개(professor, student, researcher, person)와 이항 술어 여덟 개(advises, authored, cites, affiliated, about, grandAdvisor, colleague, citesTransitively)입니다. 단항 원자는 하나의 술어를 하나의 상수에 적용한 것이므로 $4 \times 13 = 52$ 가지 가능성을 주고, 이항 원자는 하나의 술어를 상수의 순서쌍에 적용한 것이므로 $8 \times 13^2 = 8 \times 169 = 1352$ 가지를 줍니다. 따라서

|B| \;=\; 4 \cdot 13 \;+\; 8 \cdot 13^2 \;=\; 52 + 1352 \;=\; 1404 .

모든 $S_n$ 은 이 유한한 $B$ 의 부분집합입니다. 크기 $N$ 인 집합의 부분집합으로 이루어진 상승 사슬은 공간이 바닥나기 전까지 엄격하게 최대 $N$ 번 커질 수 있습니다. 왜냐하면 엄격한 단계 하나하나가 적어도 하나의 새 원소를 추가하는데, 추가할 수 있는 원소는 오직 $N$ 개뿐이기 때문입니다. 따라서 $T_P$ 는 많아야 $|B| = 1404$ 번의 스윕 안에 고정점에 도달해야 합니다. 이는 최악의 경우이며, 실제 학술 세계는 곧 지켜볼 것처럼 생산적인 스윕 단 두 번 만에 소진됩니다.

한 차례의 스윕, 그리고 세 개의 증명

이 모듈을 학술 세계 위에서 실행하면 이 장의 나머지 부분에서 풀어낼 자취가 출력됩니다.

least fixpoint reached in 3 rounds; sizes per round: [23, 41, 47, 47]
47 atoms total, 24 derived.
   ('citesTransitively', 'p2', 'p1')
   ('citesTransitively', 'p3', 'p1')
   ('citesTransitively', 'p3', 'p2')

단언된 23개의 기저 사실로부터, 일곱 개의 규칙이 24개를 더 강제로 만들어내어, 47개 원자로 이루어진 도출된 모델을 이룹니다. (23은 클래스 소속 $5$ 개, advises $4$ 개, authored $4$ 개, cites $2$ 개, affiliated $5$ 개, about $3$ 개로 합산되며, 이는 정확히 kb.py 39–69행에 나열된 기저 사실들입니다.) 그 모델에서 증명을 읽어 내기 전에, $T_P$ 의 단일한 스윕이 23개의 기저 사실 $S_0$ 에서 41개 원자의 $S_1$ 으로 실제로 움직이는 것을 지켜봅시다. 이것이 규칙 하나, 치환 하나씩 작동 중인 메커니즘입니다.

발화한 규칙 (`kb.py` 행)	$S_0$ 에서 본문을 충족시키는 치환 $\sigma$	추가된 헤드
`researcher(X) ← professor(X)` (75)	$X\mapsto$ alice; $X\mapsto$ bob	`researcher(alice)`, `researcher(bob)`
`researcher(X) ← student(X)` (76)	$X\mapsto$ carol, dave, erin	`researcher(carol)`, `researcher(dave)`, `researcher(erin)`
`person(X) ← researcher(X)` (77)	( $S_0$ 에는 아직 `researcher` 원자가 없음)	없음
`grandAdvisor(X,Z) ← advises(X,Y) ∧ advises(Y,Z)` (79)	$\{X,Y,Z\}\mapsto$ (alice,bob,carol), (alice,bob,dave), (bob,carol,erin)	`grandAdvisor(alice,carol)`, `grandAdvisor(alice,dave)`, `grandAdvisor(bob,erin)`
`colleague(X,Y) ← affiliated(X,I) ∧ affiliated(Y,I) ∧ neq(X,Y)` (82)	같은 기관에 속한 모든 순서쌍: mit의 alice/bob; cmu의 carol/dave/erin	`colleague` 원자 8개
`citesTransitively(A,B) ← cites(A,B)` (86)	$\{A,B\}\mapsto$ (p2,p1), (p3,p2)	`citesTransitively(p2,p1)`, `citesTransitively(p3,p2)`
`citesTransitively(A,C) ← cites(A,B) ∧ citesTransitively(B,C)` (87)	( $S_0$ 에는 아직 `citesTransitively` 원자가 없음)	없음

두 행은 아무것도 만들어내지 못하는데, 그 이유가 이 장 전체의 핵심입니다. person(X) ← researcher(X)는 이번 스윕에서 발화할 수 없습니다. $S_0$ 에는 researcher 원자가 하나도 없기 때문입니다. 그 원자들은 바로 이번 스윕에서 만들어지는 중이며, $T_P$ 는 본문을 절반쯤 만들어진 새 집합이 아니라 예전 집합 $S_0$ 에 대해서만 읽습니다(47행은 out이 아니라 facts를 넘겨줍니다). 마찬가지로 재귀적인 인용 규칙은 본문에 citesTransitively 원자가 필요한데, 아직 그런 것이 존재하지 않습니다. 그래서 둘 다 다음 스윕을 기다립니다. 발화하는 다섯 행은 $5 + 3 + 8 + 2 = 18$ 개의 새 원자를 추가하고, $23 + 18 = 41$ 은 정확히 자취의 두 번째 항목입니다. 엔진은 무엇을 어떤 순서로 도출할지 지시받은 적이 없습니다. 규칙들의 의존 구조가 스스로 그 순서를 부과할 뿐입니다.

조인: 한 번에 하나씩 결속하기

grandAdvisor와 colleague 행은 더 자세히 들여다볼 가치가 있습니다. 각각이 공유된 변수를 통해 두 원자를 조인하기 때문이며, 여기가 바로 앞 절에서 다룬 진행 중인 치환이 제 몫을 하는 지점입니다. _match_body는 본문 원자를 왼쪽에서 오른쪽으로 맞춥니다. 첫 번째 원자 advises(X,Y)가 $X$ 와 $Y$ 를 결속시키고, 그런 다음 두 번째 원자 advises(Y,Z)는 이미 $Y$ 가 고정된 채로 맞춰지므로, 같은 중간 인물을 축으로 삼는 지도 사슬만이 살아남습니다. 다음은 grandAdvisor 규칙에 대해 엔진이 실행하는 탐색 전체이며, 각 행은 치환을 확장하거나 고정된 $Y$ 에서 충돌하는 unify 호출입니다.

`advises(X,Y)` 매칭 후의 $\sigma$	`advises(Y,Z)`의 후보	결과	만들어진 헤드
$\{X\mapsto\text{alice}, Y\mapsto\text{bob}\}$	`advises(bob,carol)`	$Z\mapsto$ carol	`grandAdvisor(alice,carol)`
$\{X\mapsto\text{alice}, Y\mapsto\text{bob}\}$	`advises(bob,dave)`	$Z\mapsto$ dave	`grandAdvisor(alice,dave)`
$\{X\mapsto\text{bob}, Y\mapsto\text{carol}\}$	`advises(carol,erin)`	$Z\mapsto$ erin	`grandAdvisor(bob,erin)`
$\{X\mapsto\text{bob}, Y\mapsto\text{dave}\}$	사실 `advises(dave, ·)` 없음	$Y$ 에서 충돌	없음
$\{X\mapsto\text{carol}, Y\mapsto\text{erin}\}$	사실 `advises(erin, ·)` 없음	$Y$ 에서 충돌	없음

네 개의 advises 사실은 첫 번째 본문 원자를 결속하는 네 가지 방법을 주지만, 그 가운데 첫 번째 논항이 고정된 $Y$ 와 같은 두 번째 advises 사실로 확장되는 것은 셋뿐이므로, 정확히 세 개의 grand-advisor가 나옵니다. colleague 규칙은 세 번째 본문 원자로 내장 가드 neq(X, Y)를 추가하는데, 이는 _match_body(30–35행)에서 특별히 처리됩니다. 그것은 저장된 사실이 아니라, 이제 접지된 두 논항이 서로 다를 때에만 성공하는 검사이며, 이것이 바로 엔진이 모든 사람을 자기 자신의 동료라고 부르는 일을 막아 줍니다. mit에서는 순서쌍 (alice, bob)과 (bob, alice)가 남고, cmu에서는 carol, dave, erin 사이의 여섯 개 순서쌍, 즉 (carol, dave), (carol, erin), (dave, carol), (dave, erin), (erin, carol), (erin, dave)가 남아, 모두 여덟 개, 정확히 실행 결과가 출력하는 여덟 개의 colleague 원자와 일치합니다.

메커니즘이 눈에 보이게 되었으니, 증명은 저절로 쓰입니다. 도출된 모델은 그저 47개 원자의 자루가 아닙니다. 기저가 아닌 모든 원자는 그것을 그 자리에 가져다 놓은 발화의 사슬, 즉 암묵적인 증명을 지니고 있습니다. 가장 단순한 사다리인 person(erin)을 예로 들면, 이는 두 번의 규칙 적용으로 도달합니다.

student(erin)은 직접 단언된 기저 사실입니다(kb.py 44행).
researcher(X) ← student(X)가 $\sigma = \{X \mapsto \text{erin}\}$ 로 발화하여 researcher(erin)을 추가합니다.
person(X) ← researcher(X)가 같은 $\sigma$ 로 발화하여 person(erin)을 추가합니다.

원자 세 개, 전건 긍정법 두 번의 적용, 증명 하나. 증명 트리로 나타내면, 잎에서부터 위로 읽습니다.

        student(erin)          [base fact]
      ───────────────────      researcher(X) ← student(X),  X↦erin
        researcher(erin)
      ───────────────────      person(X) ← researcher(X),   X↦erin
          person(erin)

erin은 그녀가 사람이라고 전해 들은 적이 결코 없습니다. 규칙들이 그것을 도출했으며, 그 도출은 단계마다 감사할 수 있습니다. grand-advisor 증명은 조인 표에서 이미 보았듯, 공유된 중간 인물을 통해 두 전제를 하나로 고정하는 단 한 번의 적용입니다.

   advises(bob,carol)   advises(carol,erin)     [two base facts]
   ─────────────────────────────────────────    grandAdvisor(X,Z) ← advises(X,Y) ∧ advises(Y,Z)
              grandAdvisor(bob,erin)             X↦bob, Y↦carol, Z↦erin

이 세계에서 가장 깊은 증명은 추이적 인용입니다. 그 규칙이 자신의 출력을 다시 자신의 입력으로 먹이기 때문입니다(kb.py 86–88행). 기저 사실들은 인용 사슬 p3 → p2 → p1을 줍니다. 직접 규칙은 인용된 각 쌍을 추이적인 것으로 바꾸므로, citesTransitively(p2, p1)과 citesTransitively(p3, p2)는 첫 번째 스윕에서 나타납니다. 그러나 citesTransitively(p3, p1)은 그럴 수 없습니다. 그 재귀 규칙은 cites(p3, p2)(기저 사실) 그리고 citesTransitively(p2, p1)(그 자체로 도출된 사실)을 필요로 하기 때문입니다. 그 두 번째 사실이 존재한 뒤에야 재귀 규칙은 사슬 전체를 가로질러 도달할 수 있습니다.

   cites(p3,p2)   citesTransitively(p2,p1)        [base fact ; derived in sweep 1]
   ──────────────────────────────────────         citesTransitively(A,C) ← cites(A,B) ∧ citesTransitively(B,C)
           citesTransitively(p3,p1)                A↦p3, B↦p2, C↦p1

증명이 이미 증명된 사실을 필요로 하는 이 의존성이야말로, 바로 이 규칙이 고정점을 필요로 하며 한 번의 통과로는 해결될 수 없는 이유입니다. 그 증명 트리는 정말로 두 층 깊이이며, 그것이 두 번째 생산적인 스윕이 애당초 존재하는 이유입니다.

물결은 곧 증명의 깊이다

크기 자취 [23, 41, 47, 47]을 다시 읽으면, 이는 더 이상 구현 세부사항이 아니라 증명 깊이의 지도가 됩니다. 각 항목은 $T_P$ 의 $n$ 번째 스윕 이후의 모델인 $|S_n|$ 이고, 스윕 하나는 추론 단계 하나가 더 늘어난 것이므로, 어떤 사실이 처음 나타나는 물결은 그 사실의 가장 짧은 증명의 길이입니다. 다음은 모든 원자를 남김없이 설명한 것입니다.

| 물결 $n$ | $|S_n|$ | 이번 물결에서 새로 나온 것 | 무엇이 들어오고, 무엇을 기다렸는가 | |---|---|---|---| | 0 | 23 | 23 | 기저 사실, 증명 깊이 0(단언된 것, 도출된 것 없음) | | 1 | 41 | 18 | researcher 5개, colleague 8개, grandAdvisor 3개, 직접 citesTransitively 2개: 모두 기저 사실로부터 한 번 발화한 것 | | 2 | 47 | 6 | person 5개(각각 물결 1의 researcher를 기다림)와 citesTransitively(p3,p1)(물결 1의 citesTransitively(p2,p1)을 기다림) | | 3 | 47 | 0 | 확인용 스윕: 모든 규칙이 다시 발화하지만 이미 존재하는 원자만을 산출함 |

이 개수들은 실행 결과 자체가 보여 주는 것입니다. 물결 1의 새 원자 18개는 우리가 열거한 researcher 다섯 개, colleague 여덟 개, grandAdvisor 세 개, 직접 citesTransitively 두 개이고, 물결 2의 새 원자 6개는 person 다섯 개에 하나의 도달 원자 citesTransitively(p3,p1)을 더한 것이며, $5+3+8+2+5+1 = 24$ 는 헤더 줄이 보고하는 도출된 총합입니다. 물결 2 행은 재귀의 결실입니다. 그 여섯 원자는 정확히 가장 짧은 증명의 길이가 2인 것들이며, 표의 "무엇을 기다렸는가" 열은 각각이 소비하는 물결 1의 사실을 이름 붙입니다. 마지막 행인 물결 3은 아무것도 추가하지 않습니다. 47개 원자의 집합 전체에 대해 모든 규칙을 발화시켜도 동일한 47개 원자만 다시 도출될 뿐 그 이상은 없으므로, nxt == current가 되어 루프가 반환합니다. 그 변화 없는 물결은 낭비된 작업이 아닙니다. 그것은 알고리즘이 스스로에게 끝났음을 증명하는 것이며, 완전성의 실행 시간적 얼굴입니다. 이 세계에서 가장 깊은 사실들(person(erin)과 citesTransitively(p3, p1))은 길이 2의 증명을 가지며, 그래서 모델은 생산적인 스윕 두 번 만에 완전히 자라나고 세 번째는 그저 그것을 확인할 뿐입니다. 앞 절의 최악의 경우 상한에서는 루프가 1404번 실행될 수도 있었지만, 이 프로그램의 규칙 의존성은 그것을 2번 만에 끝내도록 해 줍니다.

증명으로 읽은 전방 연쇄: 각 물결은 정확히 이전보다 추론 한 단계 더 깊은 사실들을 추가하고, 학생 에린에서 사람 에린으로 이어지는 강조된 사슬은 하나의 증명이며, 마지막의 빈 물결은 알고리즘이 최소 고정점에 도달했음을 확인하는 것이다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

건전성과 완전성: 이 모델을 신뢰할 수 있는 이유

추론 절차는 그 출력이 무엇을 뜻하는지 정확히 말할 수 있을 때에만 실행할 가치가 있습니다. 두 가지 성질이 그것을 못박아 주며, 전방 연쇄는 혼 규칙에 대해 그 둘을 모두 가지고 있습니다 [1]. 이를 진술하려면 두 개의 연산을 더 필요로 합니다. $P \vDash A$ 는 " $P$ 가 $A$ 를 귀결시킨다(entails)"로 읽으며, $A$ 가 $P$ 의 모든 모델에서 참임을, 즉 기저 사실을 담고 모든 규칙을 만족하는 모든 접지 원자 집합이 $A$ 도 담고 있어야 함을 뜻합니다. $P \vdash A$ 는 " $P$ 가 $A$ 를 도출한다(derives)"로 읽으며, 전방 연쇄가 실제로 $A$ 를 산출한다는 것, 즉 $A \in \mathrm{lfp}(T_P)$ 임을 뜻합니다. 이중 턴스타일 $\vDash$ 는 모든 모델에서의 참(의미론)에 관한 것이고, 단일 턴스타일 $\vdash$ 는 기계가 산출할 수 있는 것(구문론)에 관한 것입니다. 건전성과 완전성은 이 둘이 일치한다고 말합니다.

건전성(soundness)은 $P \vdash A \implies P \vDash A$ 방향입니다(여기서 화살표 $\implies$ 는 문장 전체 수준에서 "함의한다"로 읽습니다). 절차는 귀결되는 사실만을 도출합니다. 이를 $A$ 가 처음 나타나는 물결에 대한 귀납법으로 증명합니다. $P$ 의 임의의 모델 $M$ 을 고정합시다. 즉 $M$ 은 기저 사실을 담고 모든 규칙을 만족합니다. 기저 사례: $S_0$ 의 원자는 기저 사실이고, $M$ 은 모든 기저 사실을 담고 있으므로 그것은 $M$ 안에 있습니다. 귀납 단계: $S_n$ 의 모든 원자가 $M$ 안에 있다고 가정하고, $A$ 를 $S_{n+1}$ 에서 새로 나타난 것이라 합시다. $T_P$ 의 정의에 의해 $A = h\sigma$ 이며, 이때 어떤 규칙 $h \leftarrow b_1, \ldots, b_k$ 에 대해 모든 $b_i\sigma \in S_n$ 입니다. 귀납 가설에 의해 각 $b_i\sigma \in M$ 이며, $M$ 이 그 규칙을 만족하므로 본문이 $M$ 에서 참이라는 사실은 헤드 $h\sigma \in M$ 을 강제합니다. 따라서 $S_{n+1}$ 의 모든 원자가 $M$ 안에 있습니다. $M$ 이 임의의 모델이었으므로, 도출된 모든 원자는 모든 모델 안에 있으며, 이것이 바로 $P \vDash A$ 의 정의입니다. 엔진이 하는 유일한 움직임은 전건 긍정법이고, 전건 긍정법은 참을 보존하며, 참을 보존하는 단계들의 사슬은 결코 거짓을 만들어낼 수 없습니다. 이것이 바로 출력 속의 person(erin)이 추측이 아니라 확실성인 이유입니다.

완전성(completeness)은 그 반대 방향인 $P \vDash A \implies P \vdash A$ 입니다. 절차는 귀결되는 사실을 모두 도출합니다. 이 논증은 $\mathrm{lfp}(T_P)$ 에 대한 한 가지 사실, 즉 그것 자체가 $P$ 의 모델이라는 사실을 중심으로 돌아갑니다. 그것은 기저 사실을 담고 있으며( $S_0 \subseteq \mathrm{lfp}(T_P)$ 이므로), 모든 규칙을 만족합니다. 왜냐하면 만약 어떤 규칙의 본문이 치환 $\sigma$ 에 의해 $\mathrm{lfp}(T_P)$ 에서 충족되는데도 헤드 $h\sigma$ 가 빠져 있다면, $T_P$ 를 한 번 더 적용하면 $h\sigma$ 가 추가될 것이고, 이는 $\mathrm{lfp}(T_P)$ 가 한 번 더 스윕해도 아무것도 바뀌지 않는 고정점이라는 사실과 모순되기 때문입니다. 따라서 $\mathrm{lfp}(T_P)$ 는 하나의 모델입니다. 이제 $P \vDash A$ 라고 합시다. 그러면 $A$ 는 모든 모델에서 참이고, 특히 모델 $\mathrm{lfp}(T_P)$ 에서도 참이므로 $A \in \mathrm{lfp}(T_P)$ 이며, 이것이 정확히 $P \vdash A$ 입니다. 더욱이 $\mathrm{lfp}(T_P)$ 는 최소 허브랜드 모델입니다. 혼 프로그램의 모델들은 교집합에 대해 닫혀 있으므로(어떤 모델 모임의 교집합도 다시 모델이므로), 모든 모델의 교집합은 그 자체로 가장 작은 모델이며, 그것이 $\mathrm{lfp}(T_P)$ 와 같기 때문입니다 [2][3]. "최소"라는 것이 바로 이 주장을 양방향 모두에서 동시에 팽팽하게 만들어 주는 요소입니다. 이 모델은 규칙이 강제하는 것 이상은 아무것도 더하지 않으므로, 귀결되지 않는 원자도 담고 있지 않습니다.

두 반쪽을 합치면: $P \vdash A$ 인 것과 $P \vDash A$ 인 것은 서로 필요충분조건입니다. 47개 원자로 이루어진 모델은 정확히 귀결되는 접지 원자들의 집합이며, 그보다 적지도(완전성) 많지도(건전성) 않습니다. 크기 자취가 47, 47로 반복되는 순간, 여러분은 귀결의 한 집합이 아니라 바로 그 완전한 집합을 손에 쥐게 되며, 이것이 바로 다운스트림 시스템이 이를 발견적 스케치가 아니라 근거 진리로 취급할 수 있는 이유입니다.

증명의 두 방향, 그리고 고정점이 향하는 곳

전방 연쇄는 증명을 실행할 수 있는 두 방향 가운데 하나입니다. 그것은 자료 주도적(data-driven)입니다. 사실에서 시작해 앞으로 밀고 나가며, 요청했는지 여부와 상관없이 모든 것을 도출합니다. 이는 데이터베이스 뷰나 온톨로지의 폐포처럼 모델 전체를 실체화하고 싶을 때 이상적입니다. 다른 방향은 목표 주도적(goal-driven) 후방 연쇄(backward chaining)입니다. 질의에서 시작해 거꾸로 작업하며, "어떤 규칙이 이것을 결론지을 수 있고, 그렇다면 그 본문은 무엇을 요구하는가?"를 물어, 기저 사실에 접지될 때까지 그 하위 목표들에 대해 재귀합니다 [1]. person(erin)이 성립하는지 답하려면, 후방 연쇄는 그것을 person(X) ← researcher(X)의 헤드에 맞춰 목표를 researcher(erin)으로 줄이고, 그것을 researcher(X) ← student(X)에 맞춰 student(erin)으로 줄인 다음, 사실들 가운데서 그것을 찾아냅니다. 이는 위에서 그렸던 바로 그 증명 트리를 걷는 것이지만, 자료로부터 아래에서 위로가 아니라 질문으로부터 위에서 아래로 구성된 것입니다. 두 방향 모두 우리가 도출한 동일한 unify 기본 연산 위에서 실행됩니다. 둘의 차이는 오직 단일화가 사실을 겨냥하는지, 규칙 헤드를 겨냥하는지뿐입니다. 전방 연쇄는 모든 것을 계산한 뒤 답을 찾아보고, 후방 연쇄는 오직 질문이 요구하는 것만을 계산합니다. 이 둘은 정반대의 경로로 같은 정리를 증명하며, 다음 장에서 후방 엔진을 온전히 구성해 봅니다.

전방 방향은 또한 이 시리즈에서 더 긴 미래를 갖고 있으며, 이는 전적으로 고정점 위에 놓여 있습니다. "고정점까지 적용 가능한 모든 규칙을 발화시킨다"는 동일한 루프가 기술 논리의 구성체에 특화되면, 2권이 EL 계열의 온톨로지를 분류하는 데 사용하는 완성 알고리즘(completion algorithm)이 됩니다. EL은 앞 장이 완전한 일차 논리로부터의 의도적인 후퇴로 지적했던 결정 가능한 조각입니다. 규칙 researcher(X) ← student(X)와 person(X) ← researcher(X)는 그런 관점에서 읽으면, 암묵적인 클래스 계층 $\text{student} \sqsubseteq \text{researcher} \sqsubseteq \text{person}$ 이며, 여기서 연산 $\sqsubseteq$ 는 "~에 포섭된다"(is subsumed by)로 읽고, "~의 부분클래스이다, 그래서 왼쪽의 모든 인스턴스는 오른쪽의 인스턴스이다"를 뜻합니다. 이는 동일한 엔진이 다시 등장하는 여러 지점 가운데 하나이므로, 여기서 풀어내기보다 앞으로 넘겨 둡니다. 고정점, 7장에서 이 연산과 그 최소 고정점이 온전한 수학적 다룸을 받게 되는데, 이는 전방 연쇄, 데이터로그, 추이적 폐포, 그리고 그 기술 논리 엔진 모두의 밑바탕에 있는 단 하나의 아이디어입니다. 여기서는 도출이 곧 증명임을 보는 데 필요한 만큼만 고정점을 다루었지만, 그곳에서는 그것이 주제 전체가 됩니다.

아직 풀리지 않은 부분

전방 연쇄가 주는 보장에는 미리 치러야 할 값이 따라붙습니다. 그것은 필요하든 필요하지 않든 모든 것을 도출한다는 점입니다. 우리의 장난감 세계에서는 그것이 무해한 원자 24개에 불과하지만, 추이적 인용 규칙은 축소판 경고입니다. 크고 조밀하게 연결된 지식 그래프 위의 재귀 규칙은 최소 고정점을 폭발시킬 수 있습니다. $m$ 개의 간선을 가진 인용 그래프의 추이적 폐포는 최대 $m^2$ 정도의 도출된 간선을 담을 수 있으므로, 여기서 우리를 안심시켰던 상한 $|B|$ (원자 1404개)는 웹 규모에서는 천문학적인 크기가 됩니다. 오직 하나의 사실만이 문제일 때, 그것에 답하기 위해 모델 전체를 실체화하는 것은 엄청난 낭비 작업이며, 이것이 바로 후방의 목표 주도적 방향을 지지하는 항구적인 논거입니다. 그리고 전방 연쇄의 깔끔한 건전성-완전성 이야기는 규칙이 혼 규칙이기 때문에 성립합니다. 하나의 양성 헤드, 부정 없음, 논리합 없음. 위의 증명들은 정확히 그 형태를 사용했습니다. 건전성은 "본문이 참이면 헤드를 강제한다"를 사용했고, 완전성은 모델 교집합 성질을 사용했는데, 이 둘은 모두 특별히 혼 절에 관한 정리입니다. 부정을 추가하면("어떤 사람이 논문을 발표했다는 것을 도출할 수 없으면 그 사람은 비활동적이다") 모델 교집합 성질은 무너집니다. 프로그램은 단 하나의 최소 모델 없이 동등하게 최소인 여러 모델을 허용할 수 있으며, 그래서 $\mathrm{lfp}(T_P)$ 는, 심지어 "그 프로그램의 의미"조차 더 이상 잘 정의되지 않습니다. 부정이 들어오는 순간 규칙 집합이 도대체 무엇을 의미하는지 결정하는 일은 진정으로 열려 있는 설계 공간이며, 규칙이 신경 시스템이 살아가는 열려 있고 불완전한 세계와 마주치는 순간 이후의 여러 권이 반드시 맞닥뜨려야 할 문제입니다.

왜 중요한가

신경-기호 AI는 이 장이 명료하게 답하는 하나의 질문으로 계속 되돌아갑니다. 신경망에게 "추론하라"고 요구할 때, 그것이 모방하는 목표는 무엇인가? 그 답은 최소 고정점, 즉 규칙이 강제하는 귀결의 정확하고 건전하고 완전한 집합이며, 우리 엔진이 계산하는 동시에 인증하는 47개의 원자입니다. 그 목표가 $P \vdash A \iff P \vDash A$ 라는 보장을 지닌 기계적 절차에 의해 정의되기 때문에, 우리는 항상 올바른 답을 진술할 수 있고 학습된 추론기를 그것에 견주어 채점할 수 있습니다. 모델이 곧 레이블입니다. 그리고 전방 연쇄는 우리에게 답뿐 아니라 증명도 건네줍니다. citesTransitively(p3, p1) 뒤의 길이 2짜리 트리는 그 사실이 왜 성립하는지에 대한 감사 가능한 설명이며, 어떤 사실이 나타나는 물결은 그 설명이 얼마나 깊이 이어지는지를 알려주는 지표입니다. 그런 사슬 없이 같은 사실을 예측하는 신경망 모델은 더 빠르고 잡음에 강하지만 해명할 수 없으며, 그 도출이야말로 기호 쪽이 이 하이브리드에 가져다주는 해명 가능성입니다. 추론을 미분 가능하게 만드는 이후의 모든 권은, 근본적으로 이 고정점을 근사하면서도 증명의 흔적을 어떻게든 유지하려는 시도입니다.

핵심 용어

추론 규칙(inference rule) — 전제로부터 결론으로 나아가는 정당화된 움직임. 추론의 가장 작은 단계.
전건 긍정법(modus ponens) — $P$ 와 $P \to Q$ 로부터 $Q$ 를 결론짓는다. 전방 연쇄가 계속해서 발화시키는, 참을 보존하는 움직임.
혼 규칙(Horn rule) — 하나의 양성 헤드 원자와 양성 본문 원자들의 논리곱으로 이루어진 규칙으로, "본문 전체가 성립하면 헤드가 성립한다"로 읽는다. 사실(fact)은 본문이 비어 있는 경우다.
치환( $\sigma$ , substitution) — 규칙의 변수를 상수에 대응시켜 본문이 알려진 사실과 맞아떨어지게 만드는 대응. $b\sigma$ 는 그것을 적용한 뒤의 원자 $b$ 다.
단일화(unification) — 두 원자를 동일하게 만드는 치환을 찾는 기본 연산으로, 논항 하나하나씩(먼저 술어와 항수, 그다음 각 항 쌍) 판정하며 서로 다른 두 상수에서 충돌한다. 이어서 apply_sub가 치환된 원자를 만든다.
전방 연쇄(forward chaining) — 자료 주도적 추론: 적용 가능한 모든 규칙을 발화시키고, 새로운 사실이 더 이상 나타나지 않을 때까지 반복한다.
즉각귀결 연산자( $T_P$ , immediate-consequence operator) — 한 차례의 스윕, $T_P(S) = S \cup \{h\sigma : S \text{ 안에서 } \sigma \text{에 의해 어떤 규칙의 본문이 충족됨}\}$ . 이는 팽창적이며( $S \subseteq T_P(S)$ ) 단조적이다( $S \subseteq S' \Rightarrow T_P(S) \subseteq T_P(S')$ ).
허브랜드 기저(Herbrand base) — 프로그램의 술어와 상수로부터 만들 수 있는 모든 접지 원자의 유한한 집합. 우리 세계에서는 $|B| = 1404$ 이며, 이것이 스윕 횟수의 상한이 된다.
고정점 / 최소 고정점(fixpoint / least fixpoint, lfp) — $T_P$ 에 의해 변하지 않는 사실 집합. 기저 사실로부터 도달 가능한 최소의 것이 프로그램의 의미이며, 최소 허브랜드 모델과 같다.
증명 / 도출(proof / derivation) — 원자들의 유한한 수열로, 각 원자는 기저 사실이거나 본문 원자가 더 앞에 등장하는 규칙의 헤드다. 도출된 사실 뒤에 있는 발화의 자취.
귀결( $\vDash$ , entailment) 대 도출( $\vdash$ , derivation) — $P \vDash A$ : 모든 모델에서 참임. $P \vdash A$ : 전방 연쇄에 의해 산출됨. 건전성과 완전성이 이 둘을 일치시킨다.
건전성(soundness) — $P \vdash A \Rightarrow P \vDash A$ : 절차는 귀결되는 사실만을 도출한다.
완전성(completeness) — $P \vDash A \Rightarrow P \vdash A$ : 절차는 귀결되는 사실을 모두 도출한다.
후방 연쇄(backward chaining) — 목표 주도적 추론: 질의에서 시작해 사실에 접지될 때까지 그것을 하위 목표들로 줄여 나간다.

이 논의가 향하는 곳

이제 우리는 세계를 앞으로 키워 나가고, 그 성장으로부터 증명을 읽어낼 수 있습니다. 그러나 전방 연쇄는 먼저 모든 것을 도출한 뒤에야 하나의 질문에 답하며, 이는 마음에 둔 목표가 하나뿐이고 등 뒤에 거대한 세계가 있을 때는 적합하지 않은 방식입니다. 다음 장인 리졸루션과 SLD는 화살표를 거꾸로 돌립니다. 그것은 하나의 목표에서 시작해, 여기서 우리가 만든 것과 동일한 단일화 기본 연산을 사용하여 그것을 확립할 수 있는 규칙들을 거슬러 작업하며, 예/아니오만이 아니라 증명 트리를 반환합니다. 이는 Prolog가 그 위에 세워진, 그리고 폐포가 아니라 질의가 우리가 원하는 것일 때 이 책의 나머지 부분이 의지하는, 감사 가능하고 목표 지향적인 추론입니다.

동반 코드: examples/logic/forward_chain.py는 즉각귀결 연산자 t_p와 고정점 구동기 least_fixpoint를 순수 파이썬으로 구현하며, examples/logic/kb.py의 학술 세계 사실과 규칙, 그리고 examples/logic/unify.py의 단일화 기본 연산 unify / apply_sub 위에서 동작한다. python3 examples/logic/forward_chain.py를 실행하면 [23, 41, 47, 47] 물결 자취와 세 개의 추이적 인용을 포함하여 이 장의 모든 수치를 재현할 수 있다.

이 장에서 다루는 내용​

추론 규칙: 추론의 가장 작은 움직임​

단일화: 규칙을 사실과 맞추는 기본 연산​

전방 연쇄의 형식화: 즉각귀결 연산자​

루프가 반드시 멈추는 이유​

한 차례의 스윕, 그리고 세 개의 증명​

조인: 한 번에 하나씩 결속하기​

물결은 곧 증명의 깊이다​

건전성과 완전성: 이 모델을 신뢰할 수 있는 이유​

증명의 두 방향, 그리고 고정점이 향하는 곳​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 논의가 향하는 곳​