명제 논리: 참, 거짓, 그리고 귀결

📍 현재 위치: 1부 · 밑바닥부터의 논리 — 3장. 순서와 격자는 우리에게 순위(rank), 단조 사상(monotone map), 그리고 커져 가는 집합의 최소 상계(least upper bound)를 주었습니다; 이제 우리는 그 장치를 가장 작은 논리 — "~로부터 귀결된다"가 정확한 의미를 갖는 최초의 장소 — 위에 사용하며, 최소 고정점이 기계가 실제로 추론하는 방식으로 되돌아오는 것을 지켜봅니다.

여러분이 신뢰하는 모든 논증은 어떤 결론이 어떤 전제로부터 귀결된다(follows)는 주장에 기대고 있습니다. 논리학의 근본적인 움직임은 바로 그 낱말을 정확하게 만드는 것입니다 — "맞는 말 같다"를 기계가 실행할 수 있는 검사로 바꾸어 놓는 것입니다. 그 검사가 완전히 기계적인 가장 작은 체계가 바로 명제 논리(propositional logic)입니다: 단순히 참이거나 거짓인 주장들의 세계이며, 몇 안 되는 연결사(connective)들로 서로 접합됩니다. 이는 무차별 대입(brute force)으로 판정할 수 있을 만큼 작으며, 그 무차별 대입 절차 — 모든 가능성을 열거하고 검사하는 것 — 야말로 이 시리즈의 마지막 권이 근사하는 법을 배우는 바로 그 과제입니다.

이 장은 그 체계를 빈틈없이 구축합니다. 우리는 논리식을 정확하게 정의하고, 그 의미를 트리 위의 계산으로 정의하며, 짝이 되는 코드로부터 모든 연결사의 진리표를 유도하고, "~로부터 귀결된다"를 반례 탐색으로 바꾸어 놓는 항등식을 증명한 다음, 우리가 계속 다루어 온 학계 세계 위에서 실제 추론기를 돌려 그 사실들이 물결을 이루며 고정점까지 자라나는 모습을 지켜볼 것입니다. 이 장을 마칠 때쯤이면 여러분은 작은 논리 엔진을 읽고서, 그것이 출력하는 각 숫자가 어째서 반드시 그 숫자여야 하는지를 정확히 알아볼 수 있게 될 것입니다.

쉽게 말하면

어느 학술지의 게재/반려 도장과, 모두가 동의하는 하나의 내부 규칙을 떠올려 보십시오: 논문은 참신하면서 동시에 정확할 때 정확히 채택됩니다. 이 세 가지 주장 각각에 스위치를 하나씩 달아 켜짐/꺼짐으로 만들면, 그 규칙은 손으로 직접 검사할 수 있는 기계가 됩니다. 스위치의 모든 조합을 뒤집어 가며, 각 패턴마다 "이 규칙이 성립하는가?"라고 물어보십시오. 규칙이 성립하는 패턴들의 전체 목록이 바로 그 규칙이 의미하는 모든 것입니다. 명제 논리는 그저 그것뿐입니다: 참이거나 거짓인 주장들이 "그리고", "또는", "아니다", "이면", "정확히 ~일 때"로 결합된 것 — 그리고 놀라운 성과는 "이것이 저것으로부터 귀결된다"는 것이 스위치를 계속 뒤집어 확신이 설 때까지 확인함으로써 결판날 수 있다는 것입니다. 기계는 스위치를 더 빨리 뒤집고, 규칙이 다루기 좋은 모양을 갖추었을 때는 지름길을 택함으로써 대규모로 추론합니다.

이 장에서 다루는 내용

• 원자와 연결사(atoms and connectives): 참/거짓의 구성 요소와 다섯 가지 연산자 ¬, ∧, ∨, →, ↔를 다룹니다. 각각을 먼저 평범한 말로 소개한 다음, propositional.py가 계산해 내는 정확한 진리표(truth table)에 못박습니다.
• 트리로서의 논리식(formulas as trees): 정형식(well-formed formula)의 귀납적 정의와, 짝이 되는 파일이 그것을 튜플들의 추상 구문 트리(abstract syntax tree)로 저장하는 방법을 다룹니다.
• 구조적 재귀에 의한 의미론(semantics by structural recursion): 함수로서의 진리값 할당(truth assignment), 논리식을 아래에서 위로 읽어 올라가는 evaluate 순회, 할당이 정확히 $2^n$개인 이유에 대한 유도, 그리고 실제 출력에서 그대로 인용하고 두 행을 손으로 직접 풀어 보인 "accepted ↔ (novel ∧ correct)"의 전체 진리표를 다룹니다.
• 세 가지 질문과 하나의 항등식(the three questions and one identity): 충족가능성(satisfiability), 타당성(validity), 귀결(entailment), 타당성과 불충족가능성 사이의 쌍대성(duality), 그리고 전제들이 부정된 결론과 합쳐져 불충족가능할 때 그리고 오직 그때에만 전제들이 결론을 귀결한다는 것을 한 줄 한 줄 증명하고 실제 열거로 검증하는 과정을 다룹니다.
• 혼 절과 전방 연쇄(Horn clauses and forward chaining): 추론을 분기 없이 만들어 주는 제한된 절(clause) 모양, 즉각귀결 연산자(immediate-consequence operator) $T_P$, 그것이 단조(monotone)이며 반드시 최소 고정점(least fixpoint)에 도달해야 함을 보이는 증명, 그리고 forward_chain.py에서 원자 하나하나까지 추적한 파생 물결 [23, 41, 47, 47]을 다룹니다.
• 뉴로-심볼릭 AI가 이것을 신경 쓰는 이유(why neuro-symbolic AI cares): 이러한 논리식들에 대한 충족가능성과 모델 계수(model counting)가, 4권이 미분 가능하게(differentiable) 만드는 딱 떨어지는 정답(ground truth)임을 다룹니다.

원자, 연결사, 그리고 트리로서의 논리식

원자 명제(atomic proposition), 줄여서 원자(atom)란 참 또는 거짓 둘 중 하나일 수밖에 없는, 안을 들여다볼 내부 부분이 없는 주장입니다: 이 논문은 참신하다, 이 논문은 정확하다, 이 논문은 채택된다. 우리는 이것들을 novel, correct, accepted와 같은 짧은 변수로 명명합니다. 두 진리값의 집합은 $\{\text{T}, \text{F}\}$(참과 거짓)로 표기합니다; 중괄호 $\{\ \}$는 그저 집합의 원소들을 둘러싸는 표기일 뿐이며, 나중에 기호 $\in$은 "~의 원소이다"를 뜻하게 됩니다. 그래서 "$v \in \{\text{T},\text{F}\}$"는 "$v$는 참 또는 거짓 중 하나이다"라고 읽습니다.

연결사(connective)란 하나 또는 두 개의 진리값을 받아 하나의 진리값을 돌려주는 연산자입니다 [1]. 연결사는 다섯 가지가 있습니다. 각각은 기호를 갖기 전에 한 줄짜리 말로 된 의미를 먼저 가지며, 각각은 코드가 명시적으로 계산하는 $\{\text{T},\text{F}\}$ 위의 작은 함수 그 자체입니다:

• 부정(not, ¬): 참을 거짓으로, 거짓을 참으로 뒤집습니다. ¬novel은 "참신하지 않다"를 의미합니다. 이것이 유일한 단항(unary) 연결사입니다(인자를 하나만 받습니다).
• 논리곱(and, ∧): 양쪽 모두가 참일 때만 참입니다. novel ∧ correct.
• 논리합(or, ∨): 적어도 하나가 참이면 참입니다. 이는 포함적(inclusive) 논리합이며, 양쪽 모두 성립할 때도 참입니다.
• 함의(implies, →): 임의의 두 논리식을 A와 B라고 하면, A → B는 A가 참이고 B가 거짓인 단 한 가지 경우에만 거짓입니다; "A이면 B이다"라고 생각하십시오.
• 필요충분조건(if and only if, ↔): A ↔ B는 양쪽이 같은 진리값을 가질 때 참입니다; 쌍조건문(biconditional)이며, "정확히 ~일 때"를 뜻합니다.

각 연결사는 유한한 함수이므로, 그 전체 행동이 표 하나에 다 들어갑니다. 부정은 입력 행이 두 개이고, 네 개의 이항 연결사는 동일한 네 개의 입력 행 $(A,B)$를 공유합니다. 이 표들은 규정에 의해 정해진 것이 아니라, propositional.py의 evaluate 함수가 실제로 돌려주는 값이며, 각 열 옆에 그것을 결정하는 코드 줄을 그대로 인용합니다:

$A$	$B$	$\neg A$	$A \wedge B$	$A \vee B$	$A \to B$	$A \leftrightarrow B$
F	F	T	F	F	T	T
F	T	T	F	T	T	F
T	F	F	F	T	F	F
T	T	F	T	T	T	T

¬A 열은 오직 $A$에만 의존하며(각 두 행 쌍마다 반복됩니다) propositional.py:44의 return not evaluate(f[1], assignment)에서 나옵니다. ∧ 열은 return a and b(48행)이며, 마지막 행에서만 참입니다. ∨ 열은 return a or b(50행)이며, 첫 번째 행에서만 거짓입니다. → 열은 미묘한 경우입니다: 코드는 이를 return (not a) or b(52행)로 계산하는데, 이는 정확히 a가 참이고 b가 거짓일 때만 거짓이 되어, 세 번째 행과만 일치하고 다른 어떤 행과도 일치하지 않습니다. ↔ 열은 return a == b(54행)이며, $A$와 $B$가 일치하는 두 행에서 참입니다. →가 문자 그대로 (not a) or b로 코딩되어 있다는 사실은 혼 절에 이르렀을 때 다시 기댈 것이므로 기억해 두십시오.

논리식은 기호들이 평평하게 나열된 문자열이 아니라 하나의 트리(tree)이며, 귀납적으로(inductively) 정의됩니다 — 이는 가장 단순한 논리식이 무엇인지를 먼저 말한 다음, 더 작은 것들로부터 더 큰 것을 만드는 방법을 말한다는 뜻입니다:

• 기저 경우(base case). 모든 원자는 논리식입니다.
• 귀납 단계(inductive step). $f$가 논리식이면 $\neg f$도 논리식입니다. $f$와 $g$가 논리식이면 $f \wedge g$, $f \vee g$, $f \to g$, $f \leftrightarrow g$도 논리식입니다.
• 그 밖에는 어떤 것도 논리식이 아닙니다.

이것은 재귀적인 모양입니다: 논리식은 엄밀히 더 작은 논리식들로부터, 잎에 있는 원자에 이르기까지 만들어집니다. "논문은 참신하고 정확할 때 정확히 채택된다"는 최상위 연결사 ↔를 가지며, 그 왼쪽 가지는 단순한 원자 accepted이고 오른쪽 가지는 그 자체로 더 작은 논리식인 novel ∧ correct이며, 그 가지들은 다시 두 개의 원자입니다. 짝이 되는 파일은 이 트리를 말 그대로 구현합니다: 논리식을 중첩 튜플(nested tuple)로 저장하는데, 첫 번째 자리는 연결사의 이름을 담고 나머지 자리들은 그 구성 요소를 담습니다 — 이것이 바로 추상 구문 트리(abstract syntax tree, AST), 즉 문장을 파싱한 골격입니다. 편의를 위한 생성자(constructor) 함수들은 이를 읽기 쉽게 유지해 줍니다(propositional.py:20):

def V(name):        return ("var", name)
def Not(f):         return ("not", f)
def And(f, g):      return ("and", f, g)
def Or(f, g):       return ("or", f, g)
def Imp(f, g):      return ("imp", f, g)
def Iff(f, g):      return ("iff", f, g)

그리하여 채택에 관한 우리의 규칙은 하나의 트리로 만들어지고, 또한 그렇게 저장됩니다:

accepted = Iff(V("accepted"), And(V("novel"), V("correct")))
# the same thing as its raw tree:
# ("iff", ("var", "accepted"), ("and", ("var", "novel"), ("var", "correct")))

가장 바깥쪽 튜플이 문장 전체이고, 그 안에 ∧-하위트리가 있으며, 그 안에 다시 잎(leaf)들이 있습니다. 위의 귀납적 정의야말로 이 장의 모든 연산이 그 트리 위의 순회(walk)일 수 있는 정확한 이유입니다: 각 함수는 머리(head) 태그를 살펴보고, 자식 자리에 대해 재귀 호출을 하며, "var" 잎에서 바닥을 칩니다.

의미론: 할당과 evaluate

구문(syntax)은 그저 형태일 뿐입니다. 의미론(semantics)은 의미이며, 명제 논리에서 의미는 구체적입니다 [2]. 진리값 할당(truth assignment)이란 모든 원자를 하나의 진리값으로 대응시키는 함수 $v$입니다, 즉 $v : \text{Atoms} \to \{\text{T}, \text{F}\}$; 여기서 화살표는 그저 각 원자를 하나의 값으로 보내는 규칙에 이름을 붙인 것일 뿐입니다. 이는 모든 스위치를 한 번씩 설정하는 것입니다. 코드에서 할당은 변수 이름에서 True/False로 가는 파이썬 dict이며, 그 안에서 원자를 찾아보는 것이 평가(evaluation)의 기저 경우입니다.

할당이 주어지면, 논리식은 계산 가능한 단 하나의 진리값을 가지며, 이는 트리를 잎에서부터 위로 훑어 올라가며 찾아냅니다: 각 원자를 할당에서 찾아본 다음, 각 연결사의 표를 그 자식들이 돌려준 값에 적용합니다. 이것이 구조적 재귀(structural recursion)입니다 — 논리식의 귀납적 정의를 그대로 따라가는 재귀이며, evaluate 함수 그 자체입니다(propositional.py:38):

def evaluate(f, assignment: dict) -> bool:
    """Truth value of ``f`` under an assignment of variables to True/False."""
    op = f[0]
    if op == "var":
        return assignment[f[1]]
    if op == "not":
        return not evaluate(f[1], assignment)
    a = evaluate(f[1], assignment)
    b = evaluate(f[2], assignment)
    if op == "and":
        return a and b
    if op == "or":
        return a or b
    if op == "imp":
        return (not a) or b
    if op == "iff":
        return a == b
    raise ValueError(f"unknown connective: {op}")

"var" 가지는 기저 경우입니다(스위치를 읽습니다); 그 밖의 각 가지는 귀납 단계의 한 줄입니다(이미 계산된 자식들의 값에 연결사 하나를 적용합니다). 재귀는 언제나 엄밀히 더 작은 하위 논리식으로 내려가므로 반드시 종료하며, 위의 연결사 표들이 규정하는 진리값을 정확히 돌려줍니다.

손으로 직접 재귀 풀어 보기. accepted가 거짓, correct가 참, novel이 참인 할당 $v_4$를 예로 들어, 채택 트리 위에서 evaluate를 아래에서 위로 실행해 보겠습니다:

1. 가장 안쪽, evaluate(("and", novel, correct), v_4): a = evaluate(novel) = T, b = evaluate(correct) = T로 설정한 다음 T and T = T를 돌려줍니다.
2. 바깥쪽, evaluate(("iff", accepted, ...), v_4): a = evaluate(accepted) = F, b = T(방금 계산된 값)로 설정한 다음 a == b, 즉 F == T를 돌려주며, 이는 F입니다.

그러므로 $v_4$ 아래에서는 규칙 전체가 거짓입니다: 논문이 참신하고 정확한데도 채택 도장이 찍히지 않은, 내부 규칙에 대한 진짜 위반입니다. 이를 모두 참인 할당 $v_8$과 대조해 보십시오: ∧-노드는 T and T = T를 돌려주고, ↔-노드는 T == T = T를 돌려주므로 규칙이 성립합니다. 이 두 가지 자취는 우리가 곧 열거할 표의 두 행입니다.

행은 몇 개나 될까요? 논리식은 유한히 많은 원자를 언급합니다; 그 개수를 $n = |\text{vars}(f)|$라고 부릅시다. 여기서 세로선 $|\cdot|$는 집합의 크기를 나타냅니다. 각 원자는 독립적으로 참이거나 거짓이므로 두 가지 선택지를 가지며, 서로 다른 원자들에 대한 선택은 독립적으로 이루어지므로, 전체 할당의 개수는 다음 곱입니다

$$\underbrace{2 \times 2 \times \cdots \times 2}_{n \text{ factors}} \;=\; 2^{n}.$$

assignments 생성기(generator)는 정확히 이것들을 만들어 냅니다 — 표준 라이브러리의 itertools.product에서 나온 튜플 하나하나로, product라는 맨 이름으로 임포트되어(17행) propositional.py:61에서 product([False, True], repeat=len(vs))로 호출됩니다. 이는 정의상 길이 $n$인 참/거짓 튜플 전체로 이루어진 $2^n$개짜리 집합입니다. 그 모든 것에 대해 논리식을 평가(evaluate)하면 그 문장의 의미 전체를 남김없이 적어낸 셈이 됩니다. 그 표가 바로 진리표(truth table)입니다. 우리의 채택 규칙은 $n = 3$개의 원자를 가지므로 $2^3 = 8$개의 행을 갖습니다. propositional.py를 실행하면(세 원자를 알파벳 순으로 정렬한 accepted, correct, novel) 다음이 출력됩니다:

accepted | correct | novel || f
-------------------------------
F | F | F || T
F | F | T || T
F | T | F || T
F | T | T || F
T | F | F || F
T | F | T || F
T | T | F || F
T | T | T || T
entails accepted -> novel: True

각 행을 규칙에 비추어 읽어 보십시오. 마지막 행 — accepted, correct, novel이 모두 참인 경우 — 은 양변이 일치하므로 f가 T가 되고, 아무것도 참이 아닌 첫 번째 행도 마찬가지입니다(양변 모두 거짓이며, 거짓 ↔ 거짓은 T입니다). 규칙은 네 개의 행에서 깨집니다: F | T | T는 우리가 자취를 따라간 $v_4$이며(참신하고 정확한데도 채택되지 않음), T | F | F는 둘 다 아닌데도 채택 도장이 찍혔으며, T | F | T와 T | T | F는 둘 다 채택 도장이 찍혔지만 논문이 참신하면서 동시에 정확한 것은 아닙니다 — 앞의 것은 정확성이 빠졌고, 뒤의 것은 참신함이 빠졌습니다. 논리식을 참으로 만드는 할당을 그 논리식의 모델(model)이라 부르므로, 이 표는 이 규칙이 네 개의 모델과 네 개의 반례를 갖는다고 말해 줍니다.

구체화된 의미: 논리식은 잎이 참-또는-거짓 원자인 트리이고, 그 진리표는 모든 스위치 설정에 대한 열거이며, 전방 연쇄는 더 이상 새로운 것이 나타나지 않을 때까지 물결처럼 학계 세계의 사실들을 바깥으로 키워 나갑니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

세 가지 질문, 그리고 그것들을 하나로 묶는 항등식

모든 논리식의 의미가 유한한 표가 되고 나면, 세 가지 고전적인 질문은 그 표 위에서의 기계적인 검사가 됩니다 [3]. 논리식은 적어도 하나의 할당이 그것을 참으로 만들면 — 즉 모델을 가지면 — 충족가능(satisfiable)합니다. 모든 할당이 그것을 참으로 만들어 결코 실패할 수 없다면 타당(valid)하다고 하며, 이를 항진식(tautology)이라 부릅니다. 각각은 할당들에 대한 한 줄짜리 반복문입니다(propositional.py:70와 :74):

def is_satisfiable(f) -> bool:
    return any(evaluate(f, a) for a in assignments(variables(f)))

def is_valid(f) -> bool:
    """Valid = true under *every* assignment (a tautology)."""
    return all(evaluate(f, a) for a in assignments(variables(f)))

파이썬의 any는 어떤 할당이든 하나가 $f$를 충족시키는 순간 참을 돌려주고, all은 실패하는 것이 하나도 없을 때만 참을 돌려줍니다. 충족가능성과 타당성은 같은 열거의 양 끝이며, 한 줄로 증명할 수 있는 작은 쌍대성(duality)으로 이어져 있습니다. 논리식 $f$는 그것을 거짓으로 만드는 할당이 하나도 없을 때 정확히 타당합니다; 어떤 할당이 $f$를 거짓으로 만드는 것은 정확히 그것이 $\neg f$를 참으로 만들 때이므로, "$f$는 타당하다"는 "$\neg f$는 모델이 없다", 즉 "$\neg f$는 불충족가능하다"와 같은 진술입니다. 다음 동치들의 사슬을 읽어 보십시오:

$$f \text{ valid} \iff \text{no } v \text{ has } v(f)=\text{F} \iff \text{no } v \text{ has } v(\neg f)=\text{T} \iff \neg f \text{ unsatisfiable}.$$

여기서 기호 $\iff$는 "논리적으로 같은 진술이다"를 뜻하며, 한쪽이 참인 경우와 다른 쪽이 참인 경우가 정확히 일치함을 말합니다. 이 쌍대성 덕분에 하나의 절차로 두 질문 모두에 답할 수 있습니다: 충족가능성 검사기를 만들면, 부정한 다음 모델이 없는지 확인함으로써 타당성도 검사할 수 있습니다.

세 번째 질문은 "~로부터 귀결된다"를 형식화합니다. 전제들의 집합은, 전제들의 모든 모델이 결론의 모델이기도 할 때 결론을 귀결(entail)합니다: 전제들이 모두 성립할 때마다 결론은 결코 실패할 수 없습니다. 우리는 이를 이중 turnstile 기호로 $\{\phi_1, \ldots, \phi_k\} \models C$라고 쓰며, "전제들이 $C$를 귀결한다"라고 읽습니다. (이중 막대 $\models$는 모든 모델에서의 참에 관한 의미론적(semantic) 귀결이며, 증명 규칙에 의한 구문론적(syntactic) 도출가능성을 뜻하는 단일 turnstile $\vdash$와는 의도적으로 구별됩니다 — 후자는 뒤의 장 추론과 증명에서 전개됩니다. 이 논리에서 둘이 일치한다는 것은 정의가 아니라 하나의 정리입니다.)

귀결을 검사하려면 단 하나의 반례(counterexample)를 찾아 나서면 됩니다: 모든 전제를 참으로, 결론을 거짓으로 만드는 할당 말입니다. 그런 것이 존재하지 않는다면 귀결이 성립합니다. 이는 전제들이 부정된 결론과 함께 모델을 전혀 갖지 않는다는 것, 즉 그것들이 불충족가능하다는 것과 같은 말입니다. 그 동치야말로 이 분야 전체를 떠받치는 항등식이며, 제대로 된 증명을 받을 자격이 있습니다. $P$가 모든 전제의 논리곱을 줄여 부르는 이름이라고 합시다. 그러면:

$$\begin{aligned} P \models C &\iff \text{every } v \text{ with } v(P)=\text{T} \text{ has } v(C)=\text{T} \\ &\iff \text{no } v \text{ has } v(P)=\text{T} \text{ and } v(C)=\text{F} \\ &\iff \text{no } v \text{ has } v(P)=\text{T} \text{ and } v(\neg C)=\text{T} \\ &\iff \text{no } v \text{ has } v(P \wedge \neg C)=\text{T} \\ &\iff (P \wedge \neg C) \text{ is unsatisfiable}. \end{aligned}$$

첫 번째 줄은 정의입니다. 두 번째 줄은 "모든 경우가 충족한다"를 "위반하는 경우가 하나도 없다"로 다시 씁니다(전칭 진술은 존재 진술의 부정입니다). 세 번째 줄은 부정 표에서 나오는 $v(C)=\text{F} \iff v(\neg C)=\text{T}$를 사용합니다. 네 번째 줄은 ∧ 표를 사용합니다: 논리곱은 두 논리곱 항이 모두 참일 때 정확히 참이므로, "$v(P)=\text{T}$이고 $v(\neg C)=\text{T}$"는 정확히 "$v(P \wedge \neg C)=\text{T}$"입니다. 다섯 번째 줄은 불충족가능성의 정의입니다. 그리하여: 전제들은, (전제들 ∧ ¬C)가 불충족가능할 때 그리고 오직 그때에만 C를 귀결한다. entails 함수는 정확히 이 반례 찾기입니다(propositional.py:79):

def entails(premises: list, conclusion) -> bool:
    """Do the premises logically entail the conclusion? True iff every model of
    all premises is also a model of the conclusion — checked as the
    unsatisfiability of (premises ∧ ¬conclusion)."""
    vs = set(variables(conclusion))
    for p in premises:
        vs |= variables(p)
    for a in assignments(vs):
        if all(evaluate(p, a) for p in premises) and not evaluate(conclusion, a):
            return False
    return True

이 함수는 먼저 결론이나 어느 전제에든 나타나는 모든 원자를 집합 vs에 모으며, vs |= variables(p)라는 즉석(in-place) 집합 합집합(union)으로 각 전제의 원자들을 접어 넣습니다(이는 그 원자들을 vs에 추가합니다). 그런 다음 vs에 대한 모든 할당을 열거합니다. 87행의 조건 all(...premises...) and not evaluate(conclusion, a)는 증명의 두 번째 줄을 그대로 코드로 옮긴 반례 검사입니다: 전제가 모두 참이고 동시에 결론이 거짓인 경우. 그런 할당이 처음 나타나는 순간 False를 돌려줍니다; 반복문이 그런 것을 하나도 찾지 못한 채 끝나면 True를 돌려줍니다.

진행 중인 예시에서 실제로 반례 찾기를 해보기. 위 실행 결과의 마지막 줄이 그것을 실제로 보여줍니다: entails accepted -> novel: True. 말로 풀면: 채택 규칙 $P_1 = (\text{accepted} \leftrightarrow (\text{novel} \wedge \text{correct}))$와, 별개의 사실 $P_2 = \text{accepted}$가 주어졌을 때, 그 논문이 novel이라는 것이 따라 나올까요? 전제 집합은 $\{P_1, P_2\}$이고 결론은 novel입니다. 세 원자 모두가 등장하므로, 같은 여덟 개의 할당을 열거하며 각각에 대해 반례 조건을 확인합니다:

#	accepted	correct	novel	$P_1$	$P_2$	두 전제 모두?	결론 novel	반례인가?
1	F	F	F	T	F	아니오	F	아니오
2	F	F	T	T	F	아니오	T	아니오
3	F	T	F	T	F	아니오	F	아니오
4	F	T	T	F	F	아니오	T	아니오
5	T	F	F	F	T	아니오	F	아니오
6	T	F	T	F	T	아니오	T	아니오
7	T	T	F	F	T	아니오	F	아니오
8	T	T	T	T	T	예	T	아니오

반례가 되려면 같은 행에서 "두 전제 모두 = 예"이면서 동시에 "결론 = F"여야 합니다. 두 열을 훑어보면, 전제들이 함께 성립하는 행은 정확히 8행 하나뿐이며, 그곳에서는 결론 novel이 참이므로 반례가 아닙니다. 두 전제를 모두 충족시키면서 novel을 거짓으로 남겨두는 행은 하나도 없으므로, 반복문은 아무것도 찾지 못하고 entails는 True를 돌려줍니다. 항등식도 그대로 들어맞습니다: 전제들의 유일한 모델(8행)은 novel이 참이므로 그곳에서 $\neg\text{novel}$은 거짓이고, 따라서 $P_1 \wedge P_2 \wedge \neg\text{novel}$은 모든 행에서 거짓이며, 이는 정확히 항등식이 예측하는 불충족가능성입니다. 우리는 타당한 추론에 관한 질문을 어떤 탐색이 비어 있는지에 관한 질문으로 바꾸어 놓았으며, 이러한 환원 — 추론을 (불)충족가능성으로 보는 것 — 이야말로 기계가 원자들이 의미하는 바를 한 마디도 이해하지 못한 채로도 추론할 수 있게 해주는 것입니다.

혼 절: 추론을 값싸게 만드는 모양

2의 n제곱 개의 할당을 모두 열거하는 것은 옳긴 하지만 큰 논리식에서는 가망이 없습니다. 여기서 벗어나는 길은 논리식의 모양을 제한하는 것입니다. 리터럴(literal)이란 원자이거나 그 부정입니다(예를 들어 novel 또는 ¬novel). 절(clause)이란 리터럴들의 "논리합"(or)입니다. 혼 절(Horn clause)이란 양의 리터럴을 많아야 하나만 갖는 절 — 부정되지 않은 원자를 많아야 하나만 갖고, 나머지는 모두 부정되어 있는 절입니다.

그 정의는 다시 써 보기 전까지는 난해하게 들리며, 그 다시 쓰기는 이미 손에 쥔 연결사 표들만으로도 해낼 수 있는 유도입니다. "professor(x)이면 researcher(x)이다"라는 규칙을 예로 들어봅시다. professor(x)는 "x는 교수이다"라고 읽으며, x는 임의의 개체를 나타내는 자리표시자입니다(1차 논리 표기법은 다음 장에서 풀어낼 것입니다; 지금은 채워 넣은 professor(alice)를 그저 하나의 평범한 원자로 읽으면 됩니다). 이 규칙의 자연스러운 함의 형태는 $(\text{professor} \to \text{researcher})$입니다. 이제 이를 절로 풀어헤쳐 봅시다. 코드가 →를 (not a) or b, 즉 실질 함의(material implication)로 계산한다는 것을 떠올려 보십시오:

$$A \to B \;\equiv\; \neg A \vee B.$$

몇 가지 조건을 가진 규칙, 예를 들어 $(b_1 \wedge b_2) \to h$의 경우, 같은 동치식을 적용한 다음 드모르간의 법칙(De Morgan's law), 즉 항등식 $\neg(P \wedge Q) \equiv \neg P \vee \neg Q$("둘 다는 아니다"는 "적어도 하나는 아니다"와 같다)를 적용합니다 — 이 법칙 자체도 그저 진리표의 두 열이 서로 일치한다는 것일 뿐입니다:

$$(b_1 \wedge b_2) \to h \;\equiv\; \neg(b_1 \wedge b_2) \vee h \;\equiv\; (\neg b_1 \vee \neg b_2) \vee h \;\equiv\; \neg b_1 \vee \neg b_2 \vee h.$$

그 결과는 정확히 하나의 양의 리터럴 — 머리(head) $h$ — 을 갖고, 몸체(body) 조건들은 부정되어 나타나는 하나의 절입니다. 그것이 바로 혼 절이며, 이를 거꾸로 읽으면, 양의 리터럴을 하나 가진 모든 혼 절은 "양의 조건들의 논리곱이 하나의 양의 머리를 함의한다"는 함의입니다. 순수한 사실은 몸체가 빈 특수한 경우입니다(양의 리터럴 하나, 부정 리터럴 없음). kb.py의 학계 세계는 전적으로 이 모양으로만 만들어져 있습니다(kb.py:73):

RULES: list[tuple] = [
    # A professor or a student is a researcher; a researcher is a person.
    (("researcher", "X"), [("professor", "X")]),
    (("researcher", "X"), [("student", "X")]),
    (("person", "X"), [("researcher", "X")]),
    # Grand-advising = advising composed with advising (a role chain).
    (("grandAdvisor", "X", "Z"), [("advises", "X", "Y"), ("advises", "Y", "Z")]),
    # ...
    # Transitive closure of citation — the rule that *needs* a fixpoint, because
    # its own head feeds its own body.
    (("citesTransitively", "A", "B"), [("cites", "A", "B")]),
    (("citesTransitively", "A", "C"),
     [("cites", "A", "B"), ("citesTransitively", "B", "C")]),
]

각 쌍은 (head, body)이며, body의 모든 원자가 이미 성립할 때마다 head를 이끌어냅니다.

이제 이 제한의 진짜 보상을 살펴봅시다. 일반적인 논리식의 경우, 충족가능성을 판정하려면 분기(branch)를 해야 할 수도 있습니다 — 어떤 원자를 참이라고 추측하고 탐색하다가, 되돌아가서 이번에는 거짓이라고 추측하는 식으로 말입니다. 이 분기야말로 지수적 폭발의 원천입니다. 혼 규칙은 결코 그런 추측을 강제하지 않는데, 그 이유는 "사실을 추가하는 것은 결코 해가 되지 않는다"보다 더 미묘합니다. 확정적(definite) 혼 절들의 집합은 언제나 유일한 최소 모델(least model)을 가지며, 전방 연쇄는 몸체 원자 $b_1, b_2$가 모두 존재하게 되면 그때 강제된 머리(forced head) $h$를 추가하기만 함으로써 충족시키는 할당에 도달합니다: 원자를 참인지 거짓인지 추측하는 일도, 이미 추가한 것을 철회하는 일도 결코 없습니다. 고립된 양의 추가 하나만으로 모든 절이 저절로 보존된다는 것은 사실이 아닙니다. 단독 규칙 $\text{rain} \to \text{wet}$, 즉 절 $\neg\text{rain} \vee \text{wet}$는 두 원자가 모두 거짓인 동안에는 충족됩니다($\neg\text{rain}$ 리터럴이 그것을 떠받칩니다). 하지만 rain만 단독으로 참으로 단언하면 이는 $\neg\text{T} \vee \text{F} = \text{F}$로 뒤집혀 절을 깨뜨리며, wet까지 함께 추가되어야 비로소 회복됩니다. 실제로 성립하는 것은 고정점 불변량입니다: 전방 연쇄가 수렴해 가는 집합인 최소 고정점은 모든 절을 한꺼번에 충족시킵니다. 그러므로 할 수 있는 일은 언제나 단 하나, 강제된 귀결을 추가하는 것뿐이며, 어디에서도 경우 나누기가 필요하지 않습니다. (이 규칙들은 X와 같은 변수를 담고 있으므로 엄밀히는 1차(first-order) 규칙 — 다음 장의 주제 — 이지만, 모든 변수를 특정 개체로 치환하여 변수가 하나도 남지 않은 각 접지(ground) 인스턴스는 명제 논리의 혼 절이며, 추론 원리는 동일합니다.)

전방 연쇄: 최소 고정점으로서의 추론

여기서 이전 장에서 다룬 격자(lattice) 장치가 결실을 맺습니다. 전방 연쇄(forward chaining)는 $T_P$라고 쓰는 즉각귀결 연산자(immediate-consequence operator)를 반복해서 적용함으로써 규칙들이 이끌어낼 수 있는 모든 것을 계산합니다(아래첨자 $P$는 연산자가 그 위에서 발화하는 고정된 규칙 집합인 프로그램(program)의 이름입니다). 집합 구성(set-builder) 표기법으로, 현재 사실 집합 $I$ 위에서:

$$T_P(I) \;=\; I \,\cup\, \bigl\{\, \text{head}\cdot\sigma \;:\; (\text{head}, \text{body}) \in P \text{ and every atom of } \text{body}\cdot\sigma \in I \,\bigr\},$$

여기서 $\cup$은 집합 합집합(둘 중 어느 쪽에라도 속하는 모든 것)이고, $\sigma$(시그마)는 규칙의 변수를 개체로 치환하는 치환(substitution)이며, $\text{body}\cdot\sigma$는 그 치환을 적용한 몸체(body)를 뜻합니다. 말로 풀면: 이미 가진 모든 것을 그대로 유지하고, 변수를 어떤 식으로든 묶었을 때 몸체가 이미 존재하는 모든 규칙의 머리(head)를 추가합니다. 한 번의 적용은 몇 줄이면 됩니다(forward_chain.py:42):

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

out = set(facts)는 우리가 유지하는 $I$입니다($\cup\, I$ 부분); _match_body는 몸체의 원자들이 현재 사실들과 맞아떨어지는 모든 방법을 찾아내며, 그 각각이 치환 sub($\sigma$)를 돌려줍니다; 그리고 apply_sub(head, sub)는 그 바인딩들을 머리에 채워 넣어 파생된 접지 원자, 즉 집합 구성 표기의 $\text{head}\cdot\sigma$를 만들어 냅니다.

어째서 $T_P$를 반복하면 반드시 최소 고정점에서 멈추는가. 두 가지 성질이 모든 일을 해내며, 둘 다 순서와 격자로 곧장 이어집니다 — 그곳에서는 대상이 부분집합 관계 $\subseteq$로 순서 지어진 사실들의 집합이었습니다("$I \subseteq J$"는 $I$의 모든 사실이 $J$에도 있다는 뜻입니다).

첫째, $T_P$는 팽창적(inflationary)입니다: $I \subseteq T_P(I)$인데, 그 이유는 연산자가 set(facts)에서 시작해 오직 out.add(...)만 호출할 뿐 결코 제거하지 않기 때문입니다. 사실 집합을 키울 수는 있어도 줄일 수는 없습니다.

둘째, $T_P$는 단조(monotone)입니다: $I \subseteq J$이면 $T_P(I) \subseteq T_P(J)$입니다. 증명: $a \in T_P(I)$인 임의의 원자 $a$를 취합니다. $a \in I$이면 $a \in J \subseteq T_P(J)$입니다; 그렇지 않으면 $a = \text{head}\cdot\sigma$이고 어떤 규칙의 $\sigma$ 아래의 몸체가 $I$ 안에 있는 경우인데, $I \subseteq J$이므로 그 동일한 몸체는 $J$ 안에도 있고, 따라서 그 규칙은 $J$ 위에서도 발화하여 $a \in T_P(J)$입니다. 어느 경우든 $a \in T_P(J)$이며, 이것이 바로 $\subseteq$가 요구하는 것입니다.

이제 기본 사실 $I_0$에서 시작해 $I_{k+1} = T_P(I_k)$로 두고 반복해 봅시다. 팽창성 덕분에 그 결과들은 증가하는 사슬을 이룹니다,

$$I_0 \;\subseteq\; I_1 \;\subseteq\; I_2 \;\subseteq\; \cdots$$

모든 $I_k$는 유한히 많은 술어와 개체로부터 만들 수 있는 모든 접지 원자의 유한 집합(허브랜드 기저, Herbrand base)의 부분집합입니다. 유한 집합의 부분집합들로 이루어진 증가하는 사슬은 영원히 커질 수 없습니다; 어느 단계 $k$에서는 반드시 추가를 멈추어 $I_{k+1} = I_k$가 됩니다. 그 시점에서 $I_k$는 $T_P(I_k) = I_k$를 만족합니다 — 연산자가 자기 자신으로 사상하는 집합, 즉 고정점(fixpoint)입니다. $T_P$가 단조이고 우리가 가능한 가장 작은 집합(주어진 사실들)에서 시작해 오직 강제된 귀결만을 추가했으므로, 이것은 최소 고정점, $\mathrm{lfp}(T_P)$이며, 커져 가는 사슬의 최소 상계(least upper bound)입니다 — 바로 이전 장에서 마련해 둔 그 구성입니다. 그곳에 도달하는 것은 평범한 반복문입니다(forward_chain.py:52):

def least_fixpoint(facts, rules, trace: bool = False):
    """Iterate T_P from ``facts`` until it stops growing. Returns the least
    fixpoint (a ``set`` of ground atoms). With ``trace=True`` also returns the
    per-round size, which shows the derivation "waves" of the chase."""
    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

61행의 검사 nxt == current는 고정점 조건 $T_P(I_k) = I_k$를 실행 가능하게 만든 것입니다: 어느 한 패스가 아무것도 추가하지 않는 순간, 반복문은 반환합니다. 위의 논증에 따르면 그 이후로는 결코 더 추가될 수 없기 때문입니다.

단계별로 직접 풀어 본 자취. forward_chain.py를 학계 세계에 대해 실행하면 고정점(fixpoint)에 세 라운드 만에 도달합니다:

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, 41, 47, 47]$은 사슬 $|I_0|, |I_1|, |I_2|, |I_3|$을 숫자로 나타낸 것입니다. 이 실행은 완전히 재현 가능하므로, 각 물결을 열어젖혀 그것이 추가하는 원자 하나하나에 이름을 붙일 수 있습니다:

물결 1 (23 → 41, 18개의 원자를 추가). 몸체가 기본 사실만으로 충족되는 모든 규칙이 발화합니다:

• researcher 원자 5개, researcher(X) :- professor(X)와 researcher(X) :- student(X)(kb.py:75)에서: 두 명의 교수 alice, bob과 세 명의 학생 carol, dave, erin.
• grandAdvisor 원자 3개, grandAdvisor(X,Z) :- advises(X,Y), advises(Y,Z)(kb.py:79)에서, 두 단계짜리 지도 사슬마다 하나씩: alice→carol(bob을 거쳐), alice→dave(bob을 거쳐), bob→erin(carol을 거쳐).
• colleague 원자 8개, X != Y 가드를 가진 소속 기관 공유 규칙(kb.py:82)에서: mit 쌍(alice, bob)이 양방향으로 2개, cmu 세 사람 carol, dave, erin이 서로 다른 순서쌍 6개를 모두 만들어 합계 8개.
• citesTransitively 원자 2개, 기본 규칙 citesTransitively(A,B) :- cites(A,B)(kb.py:86)에서: 직접 인용 두 건 p2→p1과 p3→p2가 추이적 관계로 격상됨.

즉 $5 + 3 + 8 + 2 = 18$개의 새 원자로, $23 + 18 = 41$에 이릅니다.

물결 2 (41 → 47, 6개의 원자를 추가). 이제 몸체가 물결 1의 출력을 필요로 했던 규칙들이 마침내 발화할 수 있습니다:

• person 원자 5개, person(X) :- researcher(X)(kb.py:77)에서, 사람마다 하나씩. 이것들은 researcher가 아직 존재하지 않았으므로 물결 1에서는 나타날 수 없었습니다; 자신의 전제가 파생되기까지 정확히 한 라운드를 기다립니다.
• citesTransitively 원자 1개, p3→p1, 재귀 규칙 citesTransitively(A,C) :- cites(A,B), citesTransitively(B,C)(kb.py:87)에서. 이는 물결 1에서 비로소 파생된 citesTransitively(p2,p1)과, 기본 사실 cites(p3,p2)를 함께 필요로 합니다.

즉 $5 + 1 = 6$개의 새 원자로, $41 + 6 = 47$에 이릅니다.

물결 3 (47 → 47, 0개를 추가). 모든 규칙의 몸체가 이미 존재하는 원자들로 이미 충족되어 있으므로, t_p는 입력과 같은 집합을 돌려주고, nxt == current가 성립하며, 반복문이 멈춥니다. 전체적으로, 주어진 23개로부터 24개의 원자가 파생되었습니다(47 atoms total, 24 derived 줄).

citesTransitively 원자들은 어째서 한 번의 훑기가 아니라 진짜로 고정점이 필요한지를 보여줍니다. citesTransitively p3 p1 — 논문 p3가 p2를 거쳐 p1에 도달하는 것 — 은 citesTransitively p2 p1이 존재한 다음에야 비로소 파생될 수 있습니다. 왜냐하면 추이성 규칙이 자기 자신의 머리를 자기 자신의 몸체로 다시 되먹이기 때문입니다: 규칙이 자기 꼬리를 붙잡을 때까지 뒤쫓는 것이며, 최소 고정점은 마침내 그것을 붙잡는 지점입니다. 또한 전체 계산이 가장 깊은 규칙 사슬보다 한 라운드 더 걸려서야 안정된다는 점도 눈여겨보십시오 — 이것이 바로 두 번의 변화의 물결($I_0 \to I_1 \to I_2$)이 아무것도 추가하지 않는 세 번째 확인용 패스($I_2 \to I_3$)를 필요로 하는 이유입니다. 바로 이 동일한 엔진이 데이터로그(Datalog) 추론기의 형태이며, 2권에서는 온톨로지(ontology)가 귀결하는 바를 계산하는 기술 논리(description logic) 완성 알고리즘의 형태이기도 합니다.

아직 풀리지 않은 부분

위의 모든 것은 조용히 비용이 큰 사실 하나에 기대고 있습니다: 우리의 결정 절차들은 열거(enumerate)한다는 것입니다. is_valid, is_satisfiable, entails는 모두 모든 할당에 대해 반복하며, 원자가 $n$개면 그 수는 $2^n$개입니다. 그 증가는 무자비합니다: 원자가 $n = 60$개만 되어도 그 수 $2^{60} \approx 1.15 \times 10^{18}$은 이미 우주 전체의 나이를 초 단위로 센 값인 약 $4.4 \times 10^{17}$초를 넘어서므로, 초당 할당 하나씩을 검사하는 검사기는 빅뱅 이후로도 아직 끝내지 못했을 것입니다. 혼(Horn) 제한은 그 특수한 경우는 구해냅니다(혼 충족가능성은, 방금 우리가 자취를 따라간 바로 그 전방 연쇄에 의해 분기 없이 거의 선형 시간에 결정 가능합니다). 하지만 일반적인 불리언 충족가능성 문제(Boolean satisfiability problem, SAT)는 NP-완전(NP-complete)입니다. NP란 비결정적 다항 시간(nondeterministic polynomial time), 즉 후보 답을 빠르게 확인하기는 쉽지만 찾아내기는 어려워 보이는 문제들의 부류입니다; NP-완전이라는 것은 SAT가 그 부류 안에서 가장 어려운 축에 속한다는 뜻이며, 따라서 SAT에 대한 효율적인 방법이 있다면 그 부류 전체를 풀어낼 수 있다는 뜻입니다. 앞으로 다가올 것에 있어 더 나쁜 소식은, 모델을 하나 찾는 것이 아니라 세는 것 — 모델 계수(model counting), 즉 #SAT — 은 계수 부류(counting class) #P에서 가장 어려운 문제들만큼이나 어려운, #P-난해(#P-hard)라는 점이며, 단순히 충족가능성을 판정하는 것보다도 한층 더 어렵습니다. 가장 어려운 논리식들에 대해 어떤 방법이든 근본적으로 열거보다 나은 성능을 낼 수 있는지는 P 대 NP(P versus NP) 문제입니다(P는 결정적 다항 시간(deterministic polynomial time), 즉 기계가 실제로 빠르게 풀어낼 수 있는 문제들을 가리키며, 이는 그저 확인만 가능한 NP의 문제들과 대비됩니다) — 컴퓨터 과학에서 가장 유명한 미해결 문제이며, 진정으로 풀리지 않았습니다. 그리하여 명제 논리는 우리에게 완벽하게 딱 떨어지는 참의 개념과 그것을 결정하는 무차별 대입(brute-force) 방법을 건네주는 동시에, 같은 숨결로 무차별 대입이 결코 규모를 감당할 수 없는 벽도 함께 건네줍니다.

왜 중요한가

바로 그 벽이 뉴로-심볼릭 AI가 들어서는 지점입니다. 이 장이 정의한 과제들 — 이 논리식이 충족가능한가, 그리고 그 할당들 중 몇 개가 모델인가 — 은 학습 시스템이 자신의 예측이 규칙을 따르기를 원할 때 필요로 하는 바로 그 정확한 연산들입니다. 4권은 모델 계수를 가져다 미분 가능하게(differentiable) 만듭니다: 충족시키는 할당들을 열거로 세는 대신, 매끄럽고 가중치가 부여된 근사인 가중 모델 계수(weighted model counting, WMC)를 계산하고, 논리적 제약을 신경망이 그것에 맞서 학습될 수 있는 의미 손실(semantic loss)로 바꾸어, 신경망을 기호적 검사기(symbolic checker)가 받아들일 만한 출력 쪽으로 슬며시 밀어붙입니다. 여기서 정의된 딱 떨어지는 SAT/계수 답은 완화(relaxation)가 목표로 삼는 정답(ground truth)입니다: 먼저 정확히 못박아 두지 않은 양은 근사할 수 없습니다. 명제 논리는 "무엇이 귀결되는가"가 더 이상 의견이 아니라 하나의 숫자가 되는 지점이며, 그 숫자야말로 이후 신경(neural) 쪽이 더듬어 다가가는 법을 배우게 되는 대상입니다.

핵심 용어

• 원자(Atom) / 원자 명제(atomic proposition): 단순히 참이거나 거짓인, 들여다볼 내부 부분이 없는 주장입니다(novel, accepted).
• 연결사(Connective): 진리값에 대한 연산자이며, 각각 고정된 표를 갖습니다: 부정(not, ¬), 논리곱(and, ∧), 논리합(or, ∨), 함의(implies, →, (not a) or b로 코딩됨), 필요충분조건(if-and-only-if, ↔).
• 논리식(Formula) / 추상 구문 트리(abstract syntax tree, AST): 원자와 연결사로부터 귀납적으로 정의된 문장이며, 첫 번째 자리가 연결사의 이름을 담는 중첩 튜플로 저장됩니다.
• 진리값 할당(Truth assignment) / 모델(model): 원자에서 참/거짓으로 가는 함수입니다; 모델이란 논리식을 참으로 만드는 할당입니다. 원자가 $n$개인 논리식은 $2^n$개의 할당을 갖습니다.
• 충족가능(Satisfiable) / 타당(valid, 항진식): 적어도 하나의 모델을 가짐 / 모든 할당 아래에서 참임을 뜻합니다; $f$는 $\neg f$가 불충족가능할 때 정확히 타당합니다.
• 귀결(Entailment, $\models$): 전제들의 모든 모델이 $C$의 모델이기도 할 때 전제들은 $C$를 귀결합니다; 이는 (전제들 ∧ ¬C)가 불충족가능할 때와 같습니다.
• 리터럴(Literal) / 절(clause) / 혼 절(Horn clause): 원자이거나 그 부정; 리터럴들의 "논리합"; 양의 리터럴을 많아야 하나만 갖는 절로, "조건들의 논리곱이 하나의 머리를 함의한다"와 동치이며, 이는 추론을 분기 없이 만들어 줍니다.
• 즉각귀결 연산자(Immediate-consequence operator, $T_P$) / 최소 고정점(least fixpoint): 적용 가능한 모든 규칙을 한 번씩 발화시키는, 팽창적이며 단조인 사상입니다; 유한한 정의역 위에서 이를 반복하면 반드시 자기 자신을 재생산하는 가장 작은 사실 집합에 도달하며, 이는 혼 프로그램의 의미이자 전방 연쇄로 계산됩니다.
• SAT / 모델 계수(Model counting): 불리언 충족가능성(NP-완전)과, 더 어려운 문제인 모델 세기(#P-난해)입니다; 4권이 가중 모델 계수로 근사하는 딱 떨어지는 정답입니다.

이 다음으로 이어지는 것

명제 논리는 우리에게 정확한 "~로부터 귀결된다"를 주었습니다 — 하지만 곧바로 느껴지는 대가가 있었습니다: 그것은 주장의 내부를 들여다볼 수 없습니다. alice_advises_bob이 참이라고 말할 수는 있지만, "학생을 지도하는 모든 교수는 연구자이다"는 표현할 수 없습니다. 객체, 관계, "모든"이라는 개념이 전혀 없기 때문입니다. 다음 장인 1차 논리: 객체, 관계, 한정사는 바로 그 장치 — 개체들에 걸쳐 있는 변수, 그것들 사이에 성립하는 관계, 그리고 한정사(quantifier) ∀("모든 ~에 대하여")와 ∃("어떤 ~가 존재한다") — 를 더하여, 이 장의 평평한 원자들을 학계 세계 규칙들이(우리가 계속 마주쳤던 X, Y, Z가) 처음부터 은밀히 그 안에 쓰여 있던 구조화된 술어(predicate)로 바꾸어 놓습니다.

---

짝이 되는 코드: examples/logic/propositional.py는 연결사들과 evaluate, is_satisfiable, is_valid, entails를 순수한 열거로 구현합니다; examples/logic/forward_chain.py는 examples/logic/kb.py의 혼 규칙들 위에서 $T_P$와 least_fixpoint를 구현합니다. python3 examples/logic/propositional.py를 실행하면 진리표와 귀결 검사를 재현할 수 있고, python3 examples/logic/forward_chain.py를 실행하면 [23, 41, 47, 47] 파생 물결과 위에서 인용한 세 개의 citesTransitively 원자를 재현할 수 있습니다.