완비 규칙: CR1–CR4와 바닥 규칙

📍 현재 위치: 3부 · EL 완성 알고리즘 — 9장. 정규화는 열네 개의 TBox 공리 전부를 역할 사슬을 더한 단 네 가지 모양의 열여섯 개 공리로 평탄화했습니다; 이제 우리는 그 평탄화된 모양들을 온톨로지가 함의하는 모든 것을 말해 줄 때까지 몇 번이고 발동시키는 엔진에 먹입니다.

정규화는 지루하지만 필수적인 작업을 해냈습니다: 추론기가 앞으로 살펴볼 모든 공리가 작고 고정된 패턴 집합 중 하나와 일치하도록 보장하여, 추론기가 깊이 중첩된 개념을 파싱할 필요가 결코 없도록 만든 것입니다. 이 장은 그 패턴들을 받아먹는 추론기를 만듭니다. 그것은 놀라울 만큼 작습니다 — 여섯 개의 이름 붙은 완비 규칙(CR1–CR4, CR⊥, CRχ)과 사소한 역할-포함 복사 규칙 하나를 발동시키는 while 루프 단 하나뿐입니다 — 그런데도 이것은 EL 계열 서술 논리 전체를 위한 완전한 분류기이며, 이는 수십만 개의 클래스를 지닌 생물의학 온톨로지 뒤에 있는 바로 그 논리입니다. 이 모든 요령은 개념에 대해 추론하기를 멈추고, 더 이상 자라지 않을 때까지 두 개의 표를 키우는 일을 시작하는 데에 있습니다.

쉽게 말하면

어느 학과 안의 소문 네트워크를 상상해 보십시오. 각 사람은 카드에 두 개의 목록을 적어 둡니다: "내가 몰래 회원으로 있는 동아리들"과 "나와 어떤 종류의 인연이 있다고 알려진 사람들"입니다. 당신은 모두에게 학과 내규를 나누어 줍니다 — "체스 동아리의 회원은 누구나 게임 동호회의 회원이기도 하다", "교수를 지도하는 사람은 누구나 연구자를 지도하는 셈이다" — 그리고 그들이 소문을 퍼뜨리게 둡니다. 어떤 규칙 때문에 누군가 아직 적어 두지 않았던 동아리나 인연을 추가할 수 있게 될 때마다, 그들은 그것을 카드에 휘갈겨 적습니다. 아무도 아무것도 지우지 않습니다. 당신은 한 차례의 온전한 소문 순회가 그 누구의 카드에도 단 한 줄도 새로 추가하지 못할 때까지 그 방을 웅성거리게 둡니다. 바로 그 순간 방은 포화(saturated) 상태가 됩니다: 내규로부터 따라 나오는 모든 회원 자격과 모든 인연이 이제 다 적혀 있으며, 어떤 결론이든 카드에서 곧바로 읽어낼 수 있습니다. 그 포화 상태가 바로 답이며, 완비 규칙은 바로 그 내규입니다.

이 장에서 다루는 내용

여러분이 포화시킬 두 개의 표 — $S(A)$ 는 $A$ 가 그 일종이라고 알려진 기본 개념(basic concept)들이고, $R(r)$ 은 $\exists r$ 엣지로 이어진 개념 쌍들입니다; 둘 다 거의 텅 빈 상태에서 시작해 오직 자라나기만 합니다.
한 블록 안의 여섯 규칙 — 정규형 NF1–NF4에 하나씩 대응하는 CR1–CR4, 그리고 바닥 규칙 CR⊥과 역할 사슬 규칙 CRχ.
엔진 그 자체 — 동반 파일에 있는 실제 while changed 루프, 그리고 "changed"가 정확히 1권의 전방 연쇄가 사용한 고정점 검사 $T(X) = X$ 인 이유.
손으로 해 보는 도출 — 공리 (4)와 (5)가 CR3에 이어 CR4를 거쳐 역할을 통해 Professor ⊑ Researcher를 어떻게 다시 도출하는지, 그리고 역할 사슬이 어떻게 grandAdvisor 엣지를 만들어 내는지.
제 몫을 톡톡히 해내는 바닥 규칙 — 분리성이 어떻게 ⊥ ∈ S(TenuredStudent)를 만들어 내는지, 그리고 그 뒤 ⊥가 advises를 따라 거꾸로 기어가 TenuredStudentAdvisor를 어떻게 단죄하는지.
측정된 고정점 — 학계 세계는 세 라운드 만에 $|S| = 39$ , $|R| = 7$ 에 자리 잡으며, 이는 실제 실행 결과에서 인용되어 규칙별 표로 요약됩니다.
아직 풀리지 않은 부분 — 이 규칙들이 참인 것들을 명백히 도출해 내기는 하지만, 그것들이 참인 포섭 관계를 전부 도출하며, 오직 참인 것만 도출할까요? 그것이 바로 건전성과 완전성이며, 다음 장의 주제입니다.

두 개의 표: S(A)와 R(r)

완성 알고리즘은 정확히 두 개의 자료 구조를 유지하며, 이를 이해하는 것이 싸움의 대부분입니다. 기호가 등장하기 전에 표기법을 이렇게 읽어 두십시오: $S$ 와 $R$ 을 추론기가 결코 지우지 않고 써 넣기만 하는 두 개의 원장(ledger)이라고 생각하십시오.

첫 번째 원장인 $S(A)$ 는 — 각 기본 개념(basic concept) $A$ (개념 이름, 또는 특별한 ⊤"모든 것" 혹은 ⊥"아무것도 아님")마다 — $A$ 가 현재 그것에 포섭된다고 알려진 기본 개념들의 집합을 담고 있습니다. $B \in S(A)$ 를 " $A \sqsubseteq B$ "라는, 즉 " $A$ 인 모든 것은 $B$ 이기도 하다"는 상시적 주장으로 읽으십시오. 그래서 $S(\text{Professor})$ 는 문자 그대로 교수가 증명 가능하게 그 일종인 모든 것들의 목록입니다.

두 번째 원장인 $R(r)$ 은 — 각 역할(role) $r$ 마다 — 모든 $A$ 가 어떤 $B$ 와 $r$ -엣지로 이어진다고 알려진 개념 쌍 $(A, B)$ 의 집합을 담고 있습니다. $(A, B) \in R(r)$ 을 " $A \sqsubseteq \exists r.B$ ", 즉 "모든 $A$ 는 적어도 하나의 $B$ 와 관계 $r$ 을 맺는다"로 읽으십시오. 그래서 $(\text{Professor}, \text{Student}) \in R(\text{advises})$ 는 모든 교수가 어떤 학생을 지도한다는, 도출된 사실을 기록합니다.

두 원장 모두 가장 작은 정직한 값에서 시작합니다. 모든 개념은 그 자신의 일종이자 ⊤의 일종이므로, 우리는 다음과 같이 씨앗을 뿌립니다

S(A) \;=\; \{\, A,\ \top \,\} \qquad\text{for every basic concept } A,

그리고 모든 역할에 대해 $R(r) = \varnothing$ 으로 시작합니다 — 어떤 규칙도 발동하기 전에는 알려진 엣지가 없습니다. 동반 파일에서 이것은 두 줄입니다(el_completion.py, 185–189번째 줄): S = {a: {a, TOP} for a in names}와 R = {}. 학계 세계에는 12개의 기본 개념 키가 있습니다 — 정규화된 공리에까지 살아남는 8개의 이름 붙은 개념과, 정규화가 발명해 낸 2개의 새 이름 $\_N1, \_N2$ , 그리고 ⊤와 ⊥ — 그래서 씨앗은 이미 23개의 포섭 항목(⊤ 자신의 집합은 그저 $\{\top\}$ 뿐이라, 쌍별 개수보다 하나 적습니다)과 0개의 역할 쌍을 담고 있습니다. 그 $(23, 0)$ 이 바로 우리가 끝에서 읽어낼 포화 추적의 출발선입니다.

네 가지 정규형에 대응하는 여섯 개의 규칙

각 완비 규칙은 존재하면-추가한다 형태의 함의입니다: 특정 항목들이 이미 원장에 들어 있고 그에 맞는 공리가 존재하면, 항목을 하나 더 추가합니다. 여섯 규칙 중 네 개는 정규화가 만들어 낸 네 가지 정규형 NF1–NF4에 일대일로 대응합니다; 나머지 두 개는 분리성(⊥)과 역할 사슬을 처리합니다. 다음이 그 전체 집합입니다 [1], 여기서 $A', B', C$ 는 기본 개념 범위를, $r, s, t$ 는 역할 범위를 나타냅니다:

\begin{aligned} \textbf{CR1:}\;\; A' \in S(A),\; A' \sqsubseteq B \;&\Longrightarrow\; B \in S(A) \\ \textbf{CR2:}\;\; A_1, A_2 \in S(A),\; A_1 \sqcap A_2 \sqsubseteq B \;&\Longrightarrow\; B \in S(A) \\ \textbf{CR3:}\;\; A' \in S(A),\; A' \sqsubseteq \exists r.B \;&\Longrightarrow\; (A, B) \in R(r) \\ \textbf{CR4:}\;\; (A, B) \in R(r),\; B' \in S(B),\; \exists r.B' \sqsubseteq C \;&\Longrightarrow\; C \in S(A) \\ \textbf{CR}\bot\textbf{:}\;\; (A, B) \in R(r),\; \bot \in S(B) \;&\Longrightarrow\; \bot \in S(A) \\ \textbf{CR}\chi\textbf{:}\;\; (A, B) \in R(r),\; (B, C) \in R(s),\; r \circ s \sqsubseteq t \;&\Longrightarrow\; (A, C) \in R(t) \end{aligned}

하나씩 해독해 봅시다. CR1은 NF1 공리 $A' \sqsubseteq B$ 를 따라가는 포섭(subsumption)의 이행성(transitivity)입니다: $A$ 가 이미 $A'$ 라고 알려져 있고, 모든 $A'$ 가 $B$ 라면, $A$ 는 $B$ 입니다. CR2는 논리곱(NF2 공리 $A_1 \sqcap A_2 \sqsubseteq B$ )을 처리합니다: $A$ 가 $A_1$ 이자 동시에 $A_2$ 라고 알려져 있다면, 그것은 $B$ 를 물려받습니다. CR3은 NF3 공리 $A' \sqsubseteq \exists r.B$ 로부터 역할 엣지를 도입합니다: $A$ 가 $A'$ 임을 아는 것은 우리가 $A$ 가 $B$ 로 향하는 $r$ -엣지를 가진다고 기록할 수 있게 해 줍니다. CR4는 미묘한 규칙입니다 — NF4 공리 $\exists r.B' \sqsubseteq C$ 를 사용한 존재 한정의 소거입니다: $A$ 가 어떤 $B$ 로 향하는 $r$ -엣지를 가지고 있고, 그 $B$ 가 $B'$ 라고 알려져 있으며, $B'$ 로 향하는 $r$ -엣지를 가진 것은 무엇이든 $C$ 여야 한다면, $A$ 는 $C$ 입니다. 이 규칙은 엣지 원장을 읽고 포섭자 원장에 다시 써 넣는데, 이것이 바로 정보가 $R$ 에서 다시 $S$ 로 흘러 들어가는 방식입니다. CR⊥, 즉 바닥 규칙은 엣지를 가로질러 충족 불가능성을 전파합니다: $A$ 가 불가능하다고 밝혀진 $B$ ( $\bot \in S(B)$ )로 향하는 $r$ -엣지를 가지고 있다면, $A$ 역시 불가능합니다 — 존재할 수 없는 것으로 향하는 엣지를 가질 수는 없기 때문입니다. CRχ, 즉 역할 사슬 규칙은 공리 $r \circ s \sqsubseteq t$ 를 통해 두 엣지를 합성합니다: $A$ 에서 $B$ 로 향하는 $r$ -엣지 다음에 $B$ 에서 $C$ 로 향하는 $s$ -엣지가 이어지면 $A$ 에서 $C$ 로 향하는 $t$ -엣지가 생겨납니다.

완성 엔진: 여섯 규칙이 정규화된 공리를 읽고 두 개의 원장 S(A)와 R(r)을 키워 나가며, 한 차례 전체 순회가 아무것도 추가하지 못할 때까지 순환합니다 — 학계 세계가 39개의 포섭자 항목과 7개의 역할 엣지를 보유하는 고정점입니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

엔진: 아무것도 바뀌지 않을 때까지 모든 규칙을 발동하다

위의 규칙들은 선언적입니다 — 그것들은 무엇을 추가해도 되는지는 말하지만, 언제 그렇게 하는지는 말하지 않습니다. 엔진은 가능한 가장 단순한 제어 구조로 그 "언제"를 제공합니다: 한 차례의 전체 순회가 아무것도 추가하지 못할 때까지 모든 규칙을 계속 발동시키는 루프입니다. 먼저 그것은 정규화된 공리들을 모양별로 나누어 담아, 각 규칙이 자신이 맞출 수 있는 공리만 훑도록 합니다(el_completion.py, 190–196번째 줄):

    # Bucket the axioms by shape so each rule scans only what it needs.
    nf1 = [a for a in normalized if a[0] == "nf1"]
    nf2 = [a for a in normalized if a[0] == "nf2"]
    nf3 = [a for a in normalized if a[0] == "nf3"]
    nf4 = [a for a in normalized if a[0] == "nf4"]
    chains = [a for a in normalized if a[0] == "chain"]
    rsubs = [a for a in normalized if a[0] == "rsub"]

그다음은 고정점 루프입니다. 단 하나의 불리언 값 changed는 현재 순회 동안 어떤 규칙이든 어떤 항목이든 추가했는지를 기록합니다; 루프는 그 값이 참으로 남아 있는 동안만 정확히 반복됩니다(el_completion.py, 211–244번째 줄):

    changed = True
    while changed:
        changed = False

        # CR1: A' ∈ S(A), A' ⊑ B  ⟹  B ∈ S(A)
        for _, a_prime, b in nf1:
            for A in names:
                if a_prime in S[A] and b not in S[A]:
                    S[A].add(b); changed = True

        # CR2: A1, A2 ∈ S(A), A1 ⊓ A2 ⊑ B  ⟹  B ∈ S(A)
        for _, conj, b in nf2:
            for A in names:
                if b not in S[A] and all(c in S[A] for c in conj):
                    S[A].add(b); changed = True

        # CR3: A' ∈ S(A), A' ⊑ ∃r.B  ⟹  (A, B) ∈ R(r)
        for _, a_prime, r, b in nf3:
            for A in names:
                if a_prime in S[A]:
                    if add_r(r, (A, b)):
                        changed = True

        # CR4: (A, B) ∈ R(r), B' ∈ S(B), ∃r.B' ⊑ C  ⟹  C ∈ S(A)
        for _, r, b_prime, c in nf4:
            for (A, B) in list(R.get(r, ())):
                if b_prime in S[B] and c not in S[A]:
                    S[A].add(c); changed = True

        # CR⊥ (the bottom rule): (A, B) ∈ R(r), ⊥ ∈ S(B)  ⟹  ⊥ ∈ S(A)
        for r, pairs in list(R.items()):
            for (A, B) in list(pairs):
                if BOT in S[B] and BOT not in S[A]:
                    S[A].add(BOT); changed = True

이 패턴은 정확히 1권의 즉시 귀결 연산자(immediate-consequence operator) $T_P$ 이며, 이제는 근거 원자(ground atom) 대신 포섭 사실 위에서 반복될 뿐입니다 [2]. 루프 본체 전체를 하나의 연산자 $T$ 로 묶어 보십시오. 이 연산자는 현재의 원장 쌍 $(S, R)$ 을 받아, 모든 규칙을 한 라운드 적용해 확대한 것을 돌려줍니다. 어떤 규칙도 결코 항목을 제거하지 않으므로 — 모든 규칙은 오직 S[A].add(...)나 add_r(...)만 호출할 뿐 결코 삭제하지 않습니다 — $T$ 는 단조(monotone)입니다: 더 큰 입력 상태는 오직 더 큰 출력 상태만 만들어 낼 수 있습니다. 그것이 바로 1권의 크나스터–타르스키(Knaster–Tarski)와 클레이니 상승(Kleene climb)이 필요로 했던 단 하나의 성질이며, 그래서 이 루프는 동일한 구성입니다: 바닥에서 씨앗을 뿌리고, 단조 함수 $T$ 를 반복해서 적용하며, 모든 규칙 아래에서 닫힌 가장 작은 상태인 최소 고정점에서 멈춥니다. 종료 검사 while changed는 고정점 조건 $T(X) = X$ 를 정확히 실행 가능한 형태로 만든 것입니다: changed는 모든 규칙을 적용해도 아무것도 추가되지 않을 때, 즉 상태가 자기 자신으로 사상될 때에만 한 차례 전체 순회 동안 False로 남습니다. 독스트링(docstring)도 한 줄로 바로 그렇게 말합니다 — "The whole thing is just a fixpoint of a monotone operator — the very same shape as the forward-chaining T_P of Volume 1"(el_completion.py, 32–33번째 줄).

두 개의 규칙 블록이 각 순회를 마무리합니다. 단순 역할-포함 규칙은 공리 $r \sqsubseteq s$ 를 따라 엣지를 복사하고; 역할 사슬 규칙 CRχ는 $r \circ s \sqsubseteq t$ 를 통해 두 엣지를 합성합니다(el_completion.py, 246–257번째 줄):

        # Simple role inclusions r ⊑ s:  (A,B) ∈ R(r)  ⟹  (A,B) ∈ R(s)
        for _, r, s in rsubs:
            for pair in list(R.get(r, ())):
                if add_r(s, pair):
                    changed = True

        # CRχ (role chain): (A,B) ∈ R(r), (B,C) ∈ R(s), r ∘ s ⊑ t  ⟹  (A,C) ∈ R(t)
        for _, (r, s), t in chains:
            for (A, B) in list(R.get(r, ())):
                for (B2, C) in list(R.get(s, ())):
                    if B == B2 and add_r(t, (A, C)):
                        changed = True

역할-포함 블록은 학계 세계에서는 아무 일도 하지 않습니다 — TBox에 $r \sqsubseteq s$ 공리가 하나도 없으므로 rsubs는 비어 있습니다 — 하지만 그것도 루프에 속하므로, 엔진은 실제로는 한 차례 순회마다 일곱 개의 규칙 블록을 발동시키며, 그중 여섯 개가 이름 붙은 규칙 CR1–CR4, CR⊥, CRχ입니다.

손으로 해 보는 도출: 역할이 Professor ⊑ Researcher를 다시 도출하다

학계 세계에서 가장 교훈적인 공리 한 쌍 위에서 두 존재 규칙이 어떻게 협력하는지 지켜보십시오. 정규화 이후, "모든 교수는 어떤 학생을 지도한다"는 공리 (4)는 NF3 공리 ("nf3", "Professor", "advises", "Student"), 즉 $\text{Professor} \sqsubseteq \exists\text{advises}.\text{Student}$ 이고, "무엇이든 지도하는 사람은 누구나 연구자이다"는 공리 (5)는 NF4 공리 ("nf4", "advises", "⊤", "Researcher"), 즉 $\exists\text{advises}.\top \sqsubseteq \text{Researcher}$ 입니다. 둘 중 어느 것도 "Professor ⊑ Researcher"를 곧바로 말하지는 않습니다; 그러나 둘이 함께 그것을 강제하며, 완비 규칙이 그것을 찾아냅니다:

CR3이 공리 (4)에서 발동합니다. 씨앗이 이미 $\text{Professor} \in S(\text{Professor})$ 를 심어 두었으므로, $A' = A = \text{Professor}$ 와 공리 $\text{Professor} \sqsubseteq \exists\text{advises}.\text{Student}$ 에 대해, CR3은 엣지 $(\text{Professor}, \text{Student})$ 를 $R(\text{advises})$ 에 추가합니다. 이제 추론기는 모든 교수가 어떤 학생을 지도한다는 것을 압니다.
CR4가 공리 (5)에서 발동합니다. 이제 우리는 $(\text{Professor}, \text{Student}) \in R(\text{advises})$ 를 가지고 있습니다; 필요한 $B' = \top$ 은 자동으로 $S(\text{Student})$ 안에 들어 있으며(⊤는 모든 씨앗에 들어 있습니다), 공리는 $\exists\text{advises}.\top \sqsubseteq \text{Researcher}$ 입니다. 그래서 CR4는 $\text{Researcher}$ 를 $S(\text{Professor})$ 에 추가합니다. 존재 한정이 소거된 것입니다: 엣지 하나와 NF4 공리 하나가 새로운 포섭자를 만들어 냈습니다.
CR1이 연쇄적으로 이어집니다. $\text{Researcher} \in S(\text{Professor})$ 와 NF1 공리 $\text{Researcher} \sqsubseteq \text{Person}$ 을 가지고, CR1은 $\text{Person}$ 을 $S(\text{Professor})$ 에 추가합니다.

추론기는 직접적인 위계 공리 (1)과는 완전히 다른 경로 — 역할을 통한 경로 — 로 $\text{Professor} \sqsubseteq \text{Researcher} \sqsubseteq \text{Person}$ 을 다시 도출해 냈으며, 두 경로는 서로 일치합니다. 포화된 원장이 정확히 이를 확인해 줍니다: S[Professor] = ['Person', 'Professor', 'Researcher', '⊤'].

역할 사슬은 바로 그 같은 엣지들 위에 올라탑니다. Dean은 (공리 8, NF1) Professor이면서 (공리 9, NF3) 어떤 Professor를 지도하므로, CR3은 $(\text{Dean}, \text{Professor})$ 를 $R(\text{advises})$ 에 넣습니다; 그리고 Dean이 CR1을 통해 Professor를 물려받으므로, 공리 (4)에 대한 CR3 역시 $(\text{Dean}, \text{Student})$ 를 그곳에 넣습니다. 이제 사슬 공리 $\text{advises} \circ \text{advises} \sqsubseteq \text{grandAdvisor}$ 와 맞추어 보는 CRχ는 $R(\text{advises})$ 안의 엣지 $(\text{Dean}, \text{Professor})$ 다음에 $R(\text{advises})$ 안의 $(\text{Professor}, \text{Student})$ 가 이어지며 가운데 개념 Professor를 공유한다는 것을 발견하고, 이 둘을 $(\text{Dean}, \text{Student}) \in R(\text{grandAdvisor})$ 로 융합합니다 — Dean은 순전히 스키마로부터 도출된, Student의 지도교수의 지도교수(grandAdvisor)인 것입니다.

제 몫을 톡톡히 해내는 바닥 규칙

지금까지의 다섯 규칙은 오직 참인 소속만을 추가할 뿐입니다. 바닥 규칙은 추론기가 모순 — 인스턴스를 전혀 가질 수 없는 개념 — 을 탐지할 수 있게 해 주는 규칙입니다. 학계 세계는 그것을 두 번 촉발하도록 일부러 꾸며져 있습니다.

첫째, TenuredStudent에서 직접적으로 나타납니다. 공리 (10)과 (11)은 그것을 교수이면서 동시에 학생으로 만듭니다 — 두 개의 NF1 공리 $\text{TenuredStudent} \sqsubseteq \text{Professor}$ 와 $\text{TenuredStudent} \sqsubseteq \text{Student}$ 로 정규화됩니다 — 한편 분리성 공리인 공리 (6)은 NF2 공리 $\text{Professor} \sqcap \text{Student} \sqsubseteq \bot$ 입니다:

CR1이 두 번 발동하여 $\text{Professor}$ 와 $\text{Student}$ 둘 다를 $S(\text{TenuredStudent})$ 에 추가합니다.
CR2가 분리성 공리에서 발동합니다: $A_1 = \text{Professor}$ 와 $A_2 = \text{Student}$ 가 둘 다 $S(\text{TenuredStudent})$ 안에 있고 공리가 $\text{Professor} \sqcap \text{Student} \sqsubseteq \bot$ 이므로, $\bot$ 을 $S(\text{TenuredStudent})$ 에 추가합니다.

$\bot \in S(\text{TenuredStudent})$ 를 갖는다는 것은 "TenuredStudent ⊑ ⊥"를 뜻합니다 — 그 개념은 충족 불가능(unsatisfiable)하며, 모든 모델에서 증명 가능하게 공집합입니다. 이것은 "하나의 클래스를 양립할 수 없는 두 가지 방식으로 모델링했다"는 전형적인 버그로, EL 추론기가 대신 잡아 주는 바로 그것입니다.

둘째, 더 미묘하게도, ⊥가 역할을 따라 거꾸로 전파되어 TenuredStudentAdvisor에까지 이릅니다. 공리 (12)는 NF3 공리 $\text{TenuredStudentAdvisor} \sqsubseteq \exists\text{advises}.\text{TenuredStudent}$ 입니다:

CR3이 발동하여 엣지 $(\text{TenuredStudentAdvisor}, \text{TenuredStudent})$ 를 $R(\text{advises})$ 에 추가합니다.
CR⊥이 발동합니다. $R(\text{advises})$ 안의 그 엣지와, 2단계에서 나온 $\bot \in S(\text{TenuredStudent})$ 를 가지고, 바닥 규칙은 $\bot$ 을 $S(\text{TenuredStudentAdvisor})$ 에 추가합니다.

그 추론은 빈틈이 없습니다: TenuredStudentAdvisor는 정의상 반드시 어떤 TenuredStudent를 지도해야 하는데, TenuredStudent는 존재할 수 없으므로, TenuredStudentAdvisor 역시 존재할 수 없습니다. 포화된 원장은 정확히 이것을 기록합니다: S[TenuredStudentAdvisor]는 ⊥를 담고 있으며, 최종 분류는 두 개념 모두를 충족 불가능하다고 보고합니다. 단일 순회가 아니라 고정점을 필요로 하게 만드는 순서 의존성에 주목하십시오: 3단계의 엣지와 2단계의 공허함(emptiness)이 CR⊥이 발동하기 전에 둘 다 존재해야 하므로, 엔진은 그런 상호작용 하나하나가 기회를 얻을 때까지 계속 순환해야 합니다.

측정된 고정점

이 모듈을 학계 세계에 대해 실행하면 포화가 라운드마다 자라나 고정점에 이르는 과정을 출력합니다 — 이는 python3 el_completion.py의 실제 커밋된 출력입니다:

saturation reached a fixpoint in 3 rounds
  round : |S| |R|  (derived subsumers, derived role pairs)
      0 :  23   0
      1 :  34   7
      2 :  39   7
      3 :  39   7

두 열을 각각 올라간 뒤 평평해지는 두 개의 상승 사슬로 읽으십시오 — 1권의 사실 개수 [23, 41, 47, 47]과 같은 파도 모양이지만, 여기서는 두 원장이 발맞추어 오르지는 않는다는 점이 다릅니다: 엣지 원장 $R$ 은 포섭자 원장 $S$ 보다 꼬박 한 라운드 앞서 고정점에 도달합니다. 포섭자 원장은 $23 \to 34 \to 39 \to 39$ 로 오르고; 엣지 원장은 $0 \to 7 \to 7 \to 7$ 로 오릅니다. 1라운드가 거의 모든 일을 해내는데, 고정된 규칙 순서 CR1→CR2→CR3→CR4→CR⊥→CRχ가 한 순회 안에서 일찍 추가된 사실이 같은 순회 안에서 나중 규칙에 공급되도록 해 주기 때문입니다. 한 라운드 만에 그것은 7개의 역할 엣지 전부(CR3에서 나온 다섯 개의 advises 엣지, 그리고 — 일단 그것들이 존재하면 — CRχ에서 나온 두 개의 grandAdvisor 엣지)와 1라운드의 새 포섭자 11개 전부를 만들어 내며, 그 11개에는 이미 어려운 사례들이 포함되어 있습니다: $\text{Professor} \sqsubseteq \text{Researcher}$ (위계 공리로부터 CR1이 직접 추가했고, 역할을 통해 CR4로도 다시 도출 가능합니다), 그리고 두 개 모두의 충족 불가능 표시 — 분리성 공리에 대한 CR2에서 나온 $\bot \in S(\text{TenuredStudent})$ 와, advises를 따라 거꾸로 기어간 CR⊥에서 나온 $\bot \in S(\text{TenuredStudentAdvisor})$ 입니다. 2라운드는 1라운드가 돌아갈 여지를 남겨 둔 CR1 연쇄만을 발동시킵니다: Dean, Professor, Student, TenuredStudent, TenuredStudentAdvisor는 각각 이미 Researcher를 지니고 있으므로, NF1 공리 $\text{Researcher} \sqsubseteq \text{Person}$ 이 다섯 모두에 Person을 추가합니다 — 마지막 5개의 포섭자이며, 그 외에는 아무것도 없습니다. 3라운드는 모든 규칙을 한 번 더 발동시키지만 아무것도 추가하지 못하며, 그렇게 고정점에 도달했음을 증명합니다: $39 = 39$ 이고 $7 = 7$ 이라는 것은 엔진이 스스로 끝났음을 인증하는 것입니다. 학계 세계는 $|S| = 39$ , $|R| = 7$ 에서 포화됩니다.

그 원장들에서 답을 읽어내면(분류(Classification)의 주제입니다) 이름 붙은 개념들 사이의 8개 포섭 관계와 2개의 충족 불가능한 개념이 나옵니다:

unsatisfiable concepts (2): ['TenuredStudent', 'TenuredStudentAdvisor']
derived role edges R:
  advises: [('Dean', 'Professor'), ('Dean', 'Student'), ('Professor', 'Student'), ('TenuredStudent', 'Student'), ('TenuredStudentAdvisor', 'TenuredStudent')]
  grandAdvisor: [('Dean', 'Student'), ('TenuredStudentAdvisor', 'Student')]

다음은 전체 규칙집을 표로 정리한 것으로, 각 행은 그것이 소비하는 정규형, 이미 존재해야 할 항목, 그리고 그것이 추가하는 항목에 맞추어져 있습니다:

규칙	소비	전제조건 (원장에 이미 있음)	추가
CR1	NF1 $A' \sqsubseteq B$	$A' \in S(A)$	$B \in S(A)$
CR2	NF2 $A_1 \sqcap A_2 \sqsubseteq B$	$A_1, A_2 \in S(A)$	$B \in S(A)$
CR3	NF3 $A' \sqsubseteq \exists r.B$	$A' \in S(A)$	$(A, B) \in R(r)$
CR4	NF4 $\exists r.B' \sqsubseteq C$	$(A, B) \in R(r)$ 그리고 $B' \in S(B)$	$C \in S(A)$
CR⊥	분리성 (⊥)	$(A, B) \in R(r)$ 그리고 $\bot \in S(B)$	$\bot \in S(A)$
CRχ	사슬 $r \circ s \sqsubseteq t$	$(A, B) \in R(r)$ 그리고 $(B, C) \in R(s)$	$(A, C) \in R(t)$

이 엔진이 장난감 이상으로 중요한 이유는 바로 그 비용에 있습니다. $n$ 개의 기본 개념 이름이 있을 때, $S$ 는 최대 $n$ 개의 키를 가지고 각 키는 최대 $n$ 개의 포섭자를 담으므로 $|S| = O(n^2)$ 입니다; 각 $R(r)$ 은 최대 $n^2$ 개의 쌍을 담습니다. 규칙이 한 번 발동할 때마다 결코 줄어들지 않고 $O(n^2)$ 로 유계인 원장에 적어도 하나의 항목을 추가하므로, 루프는 오직 다항식 개수만큼의 생산적인 라운드만 실행합니다 — 전체 분류는 다항식적이며, 실제로는 3차 시간 $O(n^3)$ 입니다 [3]. ⊓와 ∃만을 남겨 둠으로써 EL에 공학적으로 심어진 그 다항식 상한이야말로, EL 추론기가 수십만 개의 클래스를 지닌 온톨로지인 SNOMED CT와 Gene Ontology를 몇 초 만에 분류할 수 있는 바로 그 이유입니다.

아직 풀리지 않은 부분

위의 모든 내용은 이 규칙들이 명백히 참인 것들을 도출해 내는 모습을 보여 줍니다: 각 규칙은 국소적으로 자명한 함의이며, 우리는 그것들이 협력하여 눈으로 검증할 수 있는 세계에서 올바른 답에 이르는 모습을 지켜보았습니다. 그러나 "이 예제에서 명백히 참이다"는 그 무엇에 대한 증명도 되지 못하며, 바로 이 지점에서 두 가지 진짜 질문이 열린 채로 남습니다. 첫째, 건전성(soundness): 이 규칙들이 추가하는 모든 항목이 TBox의 모든 모델에서 참으로 성립하는 포섭 관계에 정말로 대응할까요 — 아니면 규칙들의 불운한 상호작용이 실제로는 함의되지 않는 $B \in S(A)$ 를 만들어 낼 수도 있을까요? 둘째, 더 어려운 문제로, 완전성(completeness): 아무것도 바뀌지 않아 루프가 멈추었을 때, 그것이 정말로 함의된 포섭 관계를 모두 찾아낸 것일까요 — 아니면 공리들로부터 진짜로 따라 나오지만 이 규칙들의 어떤 순서로도 결코 $S(A)$ 에 써 넣을 수 없는 어떤 $A \sqsubseteq B$ 가 있을 수도 있을까요? 건전하지만 불완전한 추론기는 진짜 결론을 조용히 놓칠 것이고, 완전하지만 건전하지 않은 추론기는 거짓 결론을 주장할 것입니다. 어느 쪽 실패도 통과하는 예제 하나만으로는 보이지 않습니다. 이 규칙들이 정확히 옳다는 주장 — 참인 포섭 관계를 전부, 그리고 오직 그것만 도출한다는 주장 — 은 반드시 얻어 내야 하는 정리이며, 그것을 얻어 내는 일이 바로 다음 장 전체의 임무입니다.

왜 중요한가

완성 알고리즘은 1권이 추상적으로 세워 둔 "고정점으로서의 추론"이라는 이야기 전체의 구체적인 보상입니다. 그것은 산업 강도의 서술 논리 추론기가 신비로운 정리 증명 오라클이 아니라, 여러분이 전방 연쇄로부터 이미 이해하고 있는 것과 똑같은 단조 연산자 상승이며, 단지 근거 원자 대신 포섭 사실과 역할 엣지 위에서 반복될 뿐임을 보여 줍니다. 신경-기호 AI에게 이것은 학습된 추론기가 반드시 맞혀야 할 명료하고 검증 가능한 목표입니다: 미분 가능한 모델이나 임베딩 기반 모델이 "온톨로지에 대해 추론한다"고 주장할 때, 이 엔진이 도출하는 39개의 포섭자 항목과 7개의 엣지가 바로 그 모델이 재현해야 할 정답(ground truth)이며, TenuredStudentAdvisor의 충족 불가능성은 유연한(soft) 모델이 놓치기 쉬운 바로 그런 종류의 장거리, 역할을 통한 모순 추론입니다. 정확한 알고리즘이 무엇을 계산하는지 — 그리고 다음 장에서는 그것이 왜 정확히 옳은지 — 를 정확히 아는 것이야말로, 신경망 근사가 올바른 고정점에 도달했는지 아니면 그저 그럴듯해 보이는 것에 도달했는지를 말할 수 있게 해 주는 것입니다.

핵심 용어

$S(A)$ (포섭자 원장, subsumer ledger) — $A$ 가 그것에 포섭된다고 알려진 기본 개념들의 집합; $B \in S(A)$ 는 $A \sqsubseteq B$ 를 뜻합니다. $\{A, \top\}$ 으로 씨앗이 뿌려집니다.
$R(r)$ (엣지 원장, edge ledger) — $A \sqsubseteq \exists r.B$ 를 만족하는 개념 쌍 $(A, B)$ 의 집합; 빈 상태로 씨앗이 뿌려집니다.
완성 / 포화(Completion / saturation) — 한 차례 전체 순회가 아무것도 추가하지 못할 때까지 규칙을 발동시키는 것; $T_P$ 와 같은 모양을 한 단조 연산자의 최소 고정점입니다.
CR1–CR4 — 정규형 NF1–NF4에 대응하는 네 개의 규칙: 포섭의 이행성, 논리곱, 존재 한정의 도입(엣지를 씀), 존재 한정의 소거(엣지를 읽고 포섭자를 씀).
CR⊥ (바닥 규칙) — 역할 엣지를 가로질러 ⊥를 거꾸로 전파합니다: 불가능한 개념으로 향하는 엣지는 그 출발점도 불가능하게 만듭니다.
CRχ (역할 사슬 규칙) — $r \circ s \sqsubseteq t$ 를 통해 두 엣지를 합성합니다.
충족 불가능한 개념(Unsatisfiable concept) — $\bot \in S(A)$ 인 개념; 모든 모델에서 증명 가능하게 공집합입니다(TenuredStudent, TenuredStudentAdvisor).
고정점 / while changed — $T(X) = X$ 의 실행 가능한 형태입니다: 한 라운드 전체가 아무것도 추가하지 못하면 포화가 완료되었음이 인증됩니다.

이 장이 이끄는 곳

우리는 멈추고, 저렴하며, 학계 세계에 대해 올바른 답을 내놓는 엔진을 갖게 되었습니다 — 하지만 "한 예제에서 올바르다"는 것은 약속이지 증명이 아닙니다. 다음 장인 건전성과 완전성은 그 약속을 지킵니다: 그것은 이 규칙들이 참인 포섭 관계만을 도출한다는 것(건전성, 모든 규칙이 함의를 보존함을 보임으로써)과 참인 포섭 관계를 전부 도출한다는 것(완전성, 포화된 원장으로부터 표준 모델(canonical model)을 구축하여 그 안에서 규칙이 도출하지 못한 것은 무엇이든 명백히 거짓임을 보임으로써)을 증명합니다. 그 한 쌍의 증명이야말로 완성 알고리즘을 "여기서는 작동했던 루프"에서 "신뢰할 수 있는 결정 절차"로 격상시키는 것 — 추론기를 추론기라고 부를 만한 가치가 있게 만드는 보증입니다.

이 장에서 다루는 내용​

두 개의 표: S(A)와 R(r)​

네 가지 정규형에 대응하는 여섯 개의 규칙​

엔진: 아무것도 바뀌지 않을 때까지 모든 규칙을 발동하다​

손으로 해 보는 도출: 역할이 Professor ⊑ Researcher를 다시 도출하다​

제 몫을 톡톡히 해내는 바닥 규칙​

측정된 고정점​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 장이 이끄는 곳​