정규화: 정규형으로의 환원

📍 현재 위치: 3부 · EL 완성 알고리즘 — 8장. 추론의 복잡도는 EL 포섭(subsumption)이 다항 시간(polynomial time)에 결정 가능하다고 약속했습니다; 이 장은 그 약속을 현금화하는 알고리즘의 첫걸음을 내딛습니다 — 고정된 규칙 집합이 기계적으로 발화할 수 있도록 온톨로지를 다시 짜 맞추는 것입니다.

지난 장은 EL 추론이 저렴하다는 것을 알려 주었습니다. 이 장은 어떻게 그런지를 보여 주기 시작합니다. 다음 장의 완성 규칙(completion rules)이 용어 체계를 고정점(fixpoint)까지 갈아 넣기 전에, 추론기는 일부러 거의 지루하다시피 한 일을 합니다: 모든 공리를 몇 안 되는 고정된 형태 중 하나로 다시 씁니다. 아직 아무것도 증명되지 않았습니다; 온톨로지는 그저 다시 짜 맞춰질 뿐입니다 — 마치 이상하게 접힌 편지 더미를, 사무원이 읽지 않고도 도장을 찍을 수 있는 표준 빈칸 채우기 양식으로 평평하게 펴는 것과 같습니다. 그 평평하게 펴는 작업이 바로 정규화(normalization)이며, 이것이 이후 나머지 기계 장치가 각 단계마다 상수 시간(constant time)에 돌아가게 만드는 이유입니다.

쉽게 말하면

오직 네 가지 종류의 양식에만 도장을 찍을 수 있는 세관원을 상상해 보십시오. 당신은 중첩된 절로 가득한 장황한 손글씨 요청서를 들고 옵니다("논문의 저자를 지도하는 사람은 누구나 사람으로 친다"). 세관원은 그것을 산문으로 읽어 주지 않습니다. 대신 빈칸이 하나씩 있는 네 개의 빈 템플릿을 건네고, 당신의 요청을 그 위에 다시 옮겨 적게 합니다 — 그리고 한 구절이 너무 길어서 한 줄에 들어가지 않을 때마다, 당신은 그것을 위한 짧은 참조 코드를 고안해 내고, 그 코드가 뜻하는 바를 별도의 양식에 따로 적어 둡니다. 모든 요청이 표준 템플릿 위에 놓이고 나면, 도장 찍기는 즉각적이고 아무 생각도 필요 없는 일이 됩니다. 정규화는 서류가 아니라 논리 공리에 대해 이루어지는, 바로 이 다시 옮겨 적는 단계입니다.

이 장에서 다루는 내용

• 애초에 왜 정규화하는가 — 완성 규칙은 공리의 형태를 상수 시간에 알아보아야 합니다; 임의로 중첩된 개념은 규칙을 다루기 힘들게 만들 것이므로, 정규화는 다항 시간 보장의 대가를 미리 치르는 단순화 전처리입니다.
• 네 가지 정규형(normal form) — NF1부터 NF4까지를 먼저 평범한 말로, 그다음 실제 서술 논리(description logic) 표기법으로 풀어내고, 손대지 않고 그대로 남겨 두는 역할 사슬(role chain)도 함께 다룹니다.
• 기본 개념(basic concept) — 정규형이 담을 수 있도록 허용된 "잎" 조각들: 개념 이름, ⊤(최상위), 또는 ⊥(바닥).
• 새 이름(fresh name)과 보수적 확장(conservative extension) — 복합 부분 개념을 위해 새로운 기호 Ĉ를 고안하는 것이, 원래 어휘에 관해 어떤 새로운 귀결도 더하지 않는 이유.
• 작업 목록(worklist)으로서의 재작성 규칙 — 동반 코드에 담긴 여섯 개 절(clause)로 이루어진 루프로, 각 공리를 꺼내어 문제가 되는 조각을 나누거나 이름 붙이고, 모든 것이 정규형이 될 때까지 남은 부분을 다시 밀어 넣습니다.
• 정규화된 학계 세계 — 일부러 정규형이 아니게 만든 두 개의 공리가 정확히 두 개의 새 이름을 강제하는 과정, 그리고 실제 실행 결과: 열네 개의 공리가 열여섯 개로 불어납니다.

추론하기 전에 정규화하는 이유

2권의 엔진은 완성 알고리즘(completion algorithm)입니다 — 고정점까지 반복되는 단조 연산자(monotone operator)로, 1권의 전방 연쇄 연산자(forward-chaining operator)와 같은 형태이되, 이제는 포섭 사실들 위에서 작동합니다(el_completion.py 32–33번째 줄). 매 회 지날 때마다 공리들을 훑어보고, 패턴이 충족되는 공리마다 새로운 귀결을 기록합니다. 그 훑어보기가 저렴하려면, 규칙은 "이 공리가 여기에 적용되는가?"를 O(1) — 즉 온톨로지의 크기와 무관한 상수 시간 — 에 판단해야 합니다. 다음과 같은 공리는

$$\exists \text{advises}.(\exists \text{authored}.\text{Paper}) \sqsubseteq \text{Person}$$

상수 시간에 매칭될 수 없습니다: 존재 제한(existential restriction) 안에 또 다른 존재 제한이 중첩되어 있어서, 규칙이 발화할 때마다 그 구조 안으로 재귀적으로 파고들어야 하기 때문입니다. 해결책은 추론이 시작되기 전에, 모든 공리가 이미 파고들 중첩이 전혀 없는 몇 가지 평평한 형태 중 하나를 갖도록 보장하는 것입니다. 그러면 각 완성 규칙은 고정된 템플릿에 대한 단 한 번의 패턴 매칭이 됩니다. 정규화란 바로 이 보장을, 미리 한 번에 사들이는 것입니다 [1].

정규화는 중첩된 공리들을 네 개의 고정된 템플릿으로 평평하게 펴면서, 복합 부분 개념을 위해 새 이름 _N1과 _N2를 고안해 내고, 그 결과 학계 세계의 열네 개 공리는 열여섯 개가 됩니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

네 가지 정규형

EL에서 하나의 개념은 이름(name, Professor처럼 대문자로 시작하는 원자), 모든 개체가 속하는 최상위 개념 ⊤, 아무것도 속하지 않는 바닥 개념 ⊥, 혹은 EL의 두 구성자 — 논리곱(conjunction) $C \sqcap D$("$C$이면서 동시에 $D$")와 존재 제한(existential restriction) $\exists r.C$("역할 $r$을 통해 어떤 $C$와 관계 맺는다") — 로 만들어진 복합 개념일 수 있습니다. 문제는 복합 개념이 임의로 깊이 중첩될 수 있다는 것입니다. 정규형(normal form)은 바로 그 중첩을 금지합니다: 정규형이란, 오직 기본 개념만을 자리에 담을 수 있는 정확히 네 개의 공리 템플릿 중 하나입니다.

기본(basic) 개념은 가장 단순한 종류입니다 — 이름, ⊤, 또는 ⊥이며, 그 위에 아무 구성자도 얹혀 있지 않습니다. 동반 코드는 이를 한 줄로 정의합니다(ontology.py 92–95번째 줄):

def is_basic(c) -> bool:
    """A *basic* concept is a name or ⊤/⊥ — the only thing allowed on the "leaf"
    positions of the four EL normal forms."""
    return is_name(c)

"기본"이라는 개념을 갖추었으니, 이제 네 가지 형태를 살펴보겠습니다. $A \sqsubseteq B$는 "모든 $A$는 $B$이다"로 읽으십시오(기호 ⊑는 포섭(subsumption), 즉 하위 클래스 관계입니다); $A_1 \sqcap A_2$는 "$A_1$이면서 동시에 $A_2$"로; 그리고 $\exists r.B$는 "advises/authored/… 어떤 $B$"로 읽으십시오. 문자 $A, A_1, A_2, B$는 각각 기본 개념을 나타내고, $r$은 역할을 나타냅니다:

$$\text{NF1: } A \sqsubseteq B \qquad \text{NF2: } A_1 \sqcap A_2 \sqsubseteq B \qquad \text{NF3: } A \sqsubseteq \exists r.B \qquad \text{NF4: } \exists r.B \sqsubseteq A$$

태그	정규형	말로 풀면
NF1	$A \sqsubseteq B$	하나의 기본 개념이 다른 기본 개념 아래에 놓인다
NF2	$A_1 \sqcap A_2 \sqsubseteq B$	기본 개념들의 논리곱이 기본 개념 아래에 놓인다
NF3	$A \sqsubseteq \exists r.B$	기본 개념이 기본 채움(filler)을 가진 존재 제한 아래에 놓인다
NF4	$\exists r.B \sqsubseteq A$	기본 채움을 가진 존재 제한이 기본 개념 아래에 놓인다

네 가지 형태 바깥에 있으면서 그저 그대로 유지되는 것이 두 가지 있습니다: 역할 사슬 $r \circ s \sqsubseteq t$("$r$을 한 다음 $s$를 하는 것은 $t$를 하는 것으로 친다", ∘는 "합성한"으로 읽습니다)와 단순 역할 포함(role inclusion) $r \sqsubseteq s$입니다. 이들은 이미 평평합니다 — 그 자리는 개념이 아니라 역할 이름이기 때문입니다 — 그러므로 정규화할 것이 아무것도 없습니다. 다음 장의 완성 규칙은 대략 그 표의 각 행마다 하나씩의 매처(matcher)를 가지며, 여기에 사슬과 바닥 개념을 위한 매처가 더해집니다. 그리고 모든 매처가 O(1)인 이유는 정확히, 모든 자리가 기본임이 보장되어 있기 때문입니다.

새 이름: 보수적 확장

위의 형태들은 엄격하므로, 실제 공리 대부분은 이를 위반합니다. 자리 안에 들어갈 자격이 없는 $\exists \text{authored}.\text{Paper}$ 같은 복합 부분 개념을 어떻게 처리해야 할까요? 이름을 붙여 치워 버립니다. 완전히 새로운 개념 이름 — $\hat{C}$라고 부릅시다 — 을 고안해 내고, 그것이 그 복합 개념을 뜻한다고 선언한 다음, 자리에 그 이름을 대신 넣습니다. 동반 코드는 작은 카운터로 이런 이름들을 주조합니다(el_completion.py 54–66번째 줄):

class _Fresh:
    """A factory of fresh, internal concept names ``_N1, _N2, ...`` introduced to
    stand for the compound subconcepts that normalization must name away."""

    def __init__(self):
        self.n = 0
        self.names = []

    def __call__(self) -> str:
        self.n += 1
        name = f"_N{self.n}"
        self.names.append(name)
        return name

우려되는 바는 뻔합니다: 온톨로지에 새로운 기호를 덧붙이는 것이 그것이 말하는 바를 바꾸지는 않을까요? 그렇지 않으며, 그 이유에는 이름이 있습니다. 정규화는 보수적 확장(conservative extension)입니다 [2]: 다시 쓰인 TBox $T'$는 시작했던 TBox $T$가 함의했던 것과 정확히 같은, 원래 이름들 사이의 포섭 관계만을 함의합니다. (어떤 $\hat{C}$도 나오기 전, 처음 시작했던 개념과 역할들인) 원래 어휘를 $\Sigma$라고 쓰면, 그 보장은 다음과 같습니다

$$T \models (A \sqsubseteq B) \quad\Longleftrightarrow\quad T' \models (A \sqsubseteq B) \qquad \text{for all } A, B \in \Sigma.$$

정의 $\hat{C} \equiv \exists \text{authored}.\text{Paper}$를 추가하는 것은 오직 $\hat{C}$를 언급하는 새로운 사실만을 만들어 낼 수 있을 뿐입니다; 그것이 두 개의 옛 이름 사이에 새로운 관계를 지어낼 수는 결코 없는데, $\hat{C}$가 새 이름이기 때문입니다 — 다른 어떤 것도 그것을 참조하지 않습니다. (실제로는 코드가 훨씬 더 알뜰합니다: 복합 개념이 ⊑의 왼쪽에 나왔는지 오른쪽에 나왔는지에 따라, 그 극성이 요구하는 동치 관계의 한쪽 방향만을 — 여기서는 $\exists \text{authored}.\text{Paper} \sqsubseteq \hat{C}$만을 — 추가하며, 이것만으로도 함의를 보존하는 데 충분합니다.) 그러므로 분류(classification)는 완성된 모델에서 그 답을 곧바로 읽어 내고, _N으로 시작하는 이름은 무엇이든 그저 숨기기만 하면 되며, 숨겨진 이름들이 눈에 보이는 이름들에 관해 아무것도 바꾸지 않았다는 것을 확신할 수 있습니다.

작업 목록으로서의 재작성 규칙

normalize(el_completion.py 69–154번째 줄)는 고정점까지의 작업 목록(worklist)입니다: 일반 개념 포함(general concept inclusion, GCI)들의 할 일 목록으로, 처음에는 TBox 전체로 시작해서 모든 항목이 정규형이 될 때까지 줄어듭니다. 역할 사슬과 역할 포함은 이미 평평하므로 곧바로 출력으로 향하고, 모든 GCI는 작업 목록에 올라갑니다:

    fresh = _Fresh()
    out = []
    work = []           # worklist of GCIs (L, R) still to normalize

    for ax in tbox:
        if ax[0] == "⊑":
            work.append((ax[1], ax[2]))
        elif ax[0] == "∘⊑":
            out.append(("chain", ax[1], ax[2]))
        elif ax[0] == "r⊑":
            out.append(("rsub", ax[1], ax[2]))

그런 다음 루프는 한 번에 하나씩 GCI를 꺼내어, 맞아떨어지는 첫 번째 재작성 규칙을 적용합니다. 각 재작성은 공리를 나누거나, 문제가 되는 조각 하나에 이름을 붙이며, 더 작은 GCI들을 다시 작업 목록에 밀어 넣습니다 — 그러므로 목록은 줄어들기 전에 먼저 늘어날 수도 있는데, 이는 이전 부의 고정점 오르기와 정확히 같은 모양입니다. 절은 모두 여섯 개이며, 학계 세계가 실제로 유발하는 것은 두 가지입니다: 왼쪽 존재 제한의 복합 채움에 이름을 붙이는 것과, 왼쪽 논리곱의 복합 논리곱 성분(conjunct)에 이름을 붙이는 것입니다:

        # (d) Name a compound filler of a LEFT existential (negative position):
        #     ∃r.Ĉ ⊑ R  ⟶  ∃r.A ⊑ R,  Ĉ ⊑ A   (A fresh).
        if is_some(L) and not is_basic(L[2]):
            a = fresh()
            work.append((("∃", L[1], a), R))
            work.append((L[2], a))
            continue

        # (e) Name each compound conjunct of a LEFT conjunction:
        #     ... ⊓ Ĉ ⊓ ... ⊑ R  ⟶  replace Ĉ by fresh A, add Ĉ ⊑ A.
        if is_and(L) and any(not is_basic(c) for c in L[1]):
            new_conjuncts = []
            for c in L[1]:
                if is_basic(c):
                    new_conjuncts.append(c)
                else:
                    a = fresh()
                    work.append((c, a))
                    new_conjuncts.append(a)
            work.append((("⊓", tuple(new_conjuncts)), R))
            continue

나머지 절들은 남은 형태들을 처리합니다: 오른쪽 논리곱 $L \sqsubseteq C \sqcap D$를 $L \sqsubseteq C$와 $L \sqsubseteq D$로 나누는 것, 오른쪽 존재 제한의 복합 채움에 이름을 붙이는 것, 그리고 — 오른쪽이 존재 제한인데 왼쪽이 여전히 복합적일 때 — 존재 제한 전체에 이름을 붙여서 왼쪽을 독자적으로 정규화할 수 있게 하는 것입니다. 꺼낸 GCI에 더 이상 공략할 복합 요소가 남아 있지 않으면, 마지막 절이 그것이 네 템플릿 중 무엇과 일치하는지를 읽어 내어 태그가 붙은 튜플을 내놓습니다(el_completion.py 142–152번째 줄):

        # (f) Now L and R are simple enough — emit the matching normal form.
        if is_basic(L) and is_basic(R):
            out.append(("nf1", L, R))
        elif is_and(L) and is_basic(R):
            out.append(("nf2", tuple(L[1]), R))
        elif is_basic(L) and is_some(R):
            out.append(("nf3", L, R[1], R[2]))
        elif is_some(L) and is_basic(R):
            out.append(("nf4", L[1], L[2], R))
        else:  # pragma: no cover - defensive; the rules above are exhaustive
            raise ValueError(f"cannot normalize {render(L)} ⊑ {render(R)}")

각 재작성은 대기 중인 GCI들의 전체 중첩 깊이를 엄격히 줄이므로, 작업 목록은 결코 영원히 돌 수 없습니다: TBox 크기에 선형인 시간 안에 목록은 비게 됩니다 [3].

정규화된 학계 세계

실행 중인 온톨로지의 열네 개 공리 중 열두 개는 태어날 때부터 정규형입니다. Professor ⊑ Researcher는 이미 NF1이고; Professor ⊑ ∃advises.Student는 이미 NF3입니다(그 채움 Student가 기본이기 때문입니다); Professor ⊓ Student ⊑ ⊥는 이미 NF2이고; 역할 사슬 advises ∘ advises ⊑ grandAdvisor는 손대지 않은 채로 남습니다. 정규화가 눈에 보이는 일을 하도록, 두 개의 공리는 일부러 정규형에서 벗어나게 심어 두었습니다(ontology.py 165–173번째 줄):

$$(13)\quad \exists \text{advises}.(\exists \text{authored}.\text{Paper}) \sqsubseteq \text{Person}$$ $$(14)\quad \text{Person} \sqcap \exists \text{authored}.\text{Paper} \sqsubseteq \text{Researcher}$$

공리 (13)은 채움 $\exists \text{authored}.\text{Paper}$가 복합적인 왼쪽 존재 제한이므로, 절 (d)가 발화합니다: 채움을 위해 _N2를 주조하여, $\exists \text{advises}.\_N2 \sqsubseteq \text{Person}$(NF4)과 $\exists \text{authored}.\text{Paper} \sqsubseteq \_N2$(역시 NF4)를 남깁니다. 공리 (14)는 복합 논리곱 성분을 가진 왼쪽 논리곱이므로, 절 (e)가 발화합니다: 그 성분을 위해 _N1을 주조하여, $\text{Person} \sqcap \_N1 \sqsubseteq \text{Researcher}$(NF2)와 $\exists \text{authored}.\text{Paper} \sqsubseteq \_N1$(NF4)을 남깁니다. 이 두 공리에 대해 코드가 실제로 내놓는 네 개의 태그된 튜플은 다음과 같습니다:

('nf2', ('Person', '_N1'), 'Researcher')      # Person ⊓ _N1 ⊑ Researcher   (from axiom 14)
('nf4', 'authored', 'Paper', '_N1')            # ∃authored.Paper ⊑ _N1        (from axiom 14)
('nf4', 'authored', 'Paper', '_N2')            # ∃authored.Paper ⊑ _N2        (from axiom 13)
('nf4', 'advises', '_N2', 'Person')            # ∃advises._N2 ⊑ Person        (from axiom 13)

_N1과 _N2가 같은 복합 개념, 즉 $\exists \text{authored}.\text{Paper}$를 줄인 것임에 주목하십시오 — 정규화기는 하나를 공유하는 대신, 각 출현마다 별도의 새 이름을 주조합니다. 그것이 바로 정규형이 아닌 두 공리가 하나가 아니라 두 개의 새 이름을 대가로 치르는 이유입니다. 모듈을 실행하면 집계와 형태별 통계가 출력됩니다(el_completion.py 328–334번째 줄):

normalization: 14 axioms → 16 normal-form axioms, introducing 2 fresh names ['_N1', '_N2']
  by normal form: {'chain': 1, 'nf1': 6, 'nf2': 2, 'nf3': 3, 'nf4': 4}

이미 정규형인 열두 개의 공리에, (13)과 (14)에서 만들어진 네 개를 더하면 열여섯 개가 되며, 이 통계가 보고하는 그대로 각 형태에 걸쳐 분포합니다:

정규형	공리 형태	개수
사슬(chain)	$r \circ s \sqsubseteq t$	1
NF1	$A \sqsubseteq B$	6
NF2	$A_1 \sqcap A_2 \sqsubseteq B$	2
NF3	$A \sqsubseteq \exists r.B$	3
NF4	$\exists r.B \sqsubseteq A$	4
전체		16

이제 TBox는 열여섯 개의 평평한 템플릿과 하나의 역할 사슬에 지나지 않습니다 — 완성 규칙이 발화당 상수 시간에 씹어 넘길 수 있는 형태입니다.

아직 풀리지 않은 부분

이 장의 정직한 한계는, 정규화가 어떤 추론도 전혀 하지 않는다는 것입니다. 정규화는 단 하나의 포섭도 결정하지 않았습니다; TenuredStudent가 충족 불가능(unsatisfiable)하다는 것도, Dean ⊑ Researcher라는 것도 알아채지 못했습니다. 정규화는 그저 온톨로지를 다시 짜 맞추었을 뿐이며, 중첩된 공리 두 개를 평평한 공리 네 개와 새로 고안한 이름 두 개로 바꾸었을 뿐입니다. 진정한 추론 — 새로운 ⊑ 사실 하나하나 — 은 아직 오지 않았으며, 그것은 오직 완성 규칙이 이 정규화된 공리들을 고정점까지 포화(saturate)시킬 때에만 옵니다. 우리가 발견한 작은 중복(하나의 복합 개념에 두 개의 이름)은 바로 그 같은 겸손함의 증상입니다: 정규화는 의미론적 기억이 전혀 없는 구문적 절차이므로 동등한 부분 개념들을 하나로 접어 넣지 않으며, 더 똑똑한 추론기라면 그 일을 뒤이어 오는 추론 단계에게 맡깁니다. 정규화는 평평하고 믿음직한 활주로이며, 비행은 다음 장의 몫입니다.

왜 중요한가

여기서의 움직임 — 기계적인 연산자가 일률적으로 작동할 수 있도록, 임의의 구조를 작고 고정된 템플릿 집합으로 환원하는 것 — 은 EL만의 특이한 습성이 아니라, 신경-기호(neuro-symbolic) AI에서 가장 뿌리 깊게 되풀이되는 습관 중 하나입니다. 논리적 구조를 입력으로 받는 신경 추론기는, 완성 규칙과 똑같은 이유로 그 입력이 정규(canonical) 형태이기를 필요로 합니다: 고정된 항수(arity)를 가지고 중첩이 없는 인코딩이야말로, 학습되었든 손으로 작성되었든 하나의 연산자가 깊이에 따라 특별 취급을 하지 않고도 어디에나 적용될 수 있게 해 주는 것입니다. 이후의 권들이 온톨로지를 임베딩이나 미분 가능한 증명기(differentiable prover)에 먹일 때에도, 그들은 바로 여기와 똑같은 동기로 먼저 정규화를 할 것입니다 — 고정된 템플릿은 기호적 규칙과 신경망 층이 함께 작동할 수 있는 공유된 기층입니다. 정확한 형태를 올바로 만들어 내고, 그것이 아무 의미도 바꾸지 않았음을 아는 것(보수적 확장 보장)이야말로, 더 부드럽고 학습된 어떤 재구성이든 그에 견주어 평가받아야 할 바로 그 잣대입니다.

핵심 용어

• 정규화(Normalization) — 모든 공리가 네 가지 정규형 또는 역할 사슬 중 하나가 되도록 TBox를 다시 쓰는 것으로, 복합 부분 개념을 위해 새 이름을 도입합니다.
• 정규형(Normal form, NF1–NF4) — 허용되는 네 개의 공리 템플릿: $A \sqsubseteq B$, $A_1 \sqcap A_2 \sqsubseteq B$, $A \sqsubseteq \exists r.B$, $\exists r.B \sqsubseteq A$이며, 모든 자리는 기본 개념입니다.
• 기본 개념(Basic concept) — 정규형이 담을 수 있는 잎 조각: 개념 이름, ⊤(최상위), 또는 ⊥(바닥)이며, 그 위에 구성자가 얹혀 있지 않습니다.
• 새 이름(Fresh name, $\hat{C}$) — 복합 부분 개념을 줄여서 하나의 자리를 차지할 수 있게 해 주는, 완전히 새로운 기호(_N1, _N2, …).
• 보수적 확장(Conservative extension) — 다시 쓰인 TBox가 원래 이름들 사이에서 원본과 정확히 같은 포섭 관계만을 함의한다는 보장으로, 이로써 새 이름은 옛 어휘에 대해 어떤 새로운 귀결도 더하지 않습니다.
• 작업 목록(Worklist) — 아직 정규형이 아닌 GCI들의 줄어드는 할 일 목록으로, normalize가 꺼내어 나누거나 이름 붙이고, 비워질 때까지 다시 밀어 넣습니다.
• 역할 사슬(Role chain) — 복합 역할 포함 $r \circ s \sqsubseteq t$이며, 이미 평평하므로 그대로 유지됩니다.

이 장이 이끄는 곳

이제 온톨로지는 열여섯 개의 평평한 공리이며, 각각은 규칙이 안을 들여다볼 필요 없이 매칭할 수 있는 형태입니다 — 그러나 아직 단 하나의 포섭도 결정되지 않았습니다. 다음 장인 완성 규칙은 이 템플릿들을 추론으로 바꿉니다: 두 개의 자료 구조 $S(A)$와 $R(r)$을 정의하고, 새로운 것이 더 이상 나타나지 않을 때까지 규칙 CR1–CR4, 바닥 규칙, 역할 사슬 규칙을 발화시킨 다음, 포화된 결과로부터 곧바로 — TenuredStudent의 충족 불가능성을 포함한 — 학계 세계의 완전한 분류를 읽어 냅니다. 정규화가 활주로를 놓았다면, 완성은 마침내 이륙하는 추론입니다.