# 判定域間的信息穿越：跨域映射、保真、分裂、合併與不可比性

**English Title:** Information Crossing Between Judgment Domains: Cross-Domain Mapping, Preservation, Splitting, Merging, and Incomparability  
**Series:** Domain-Transition Information Logic, Paper V  
**Author:** Neo.K  
**Collaborator:** Aletheia (GPT-5.6 Sol)  
**Institution:** EveMissLab / 一言諾科技有限公司  
**Version:** v0.1  
**Date:** 2026-08-10  
**Status:** Series II — Cross-Domain Mapping Paper

## 摘要

Series II 前四篇已建立：Q4 局部資訊狀態、歷史路徑算子、對象重分類，以及 transition-boundary information。本文進一步處理本系列最初的另一個核心命題：

\[
\boxed{
\text{信息從一個判定域進入另一個判定域時，究竟發生了什麼？}
}
\]

令來源判定域為：

\[
\mathcal J_A,
\]

目標判定域為：

\[
\mathcal J_B.
\]

本文將跨域轉換表示為一個有型別的 bridge：

\[
\boxed{
\mathcal M_{A\to B}:
\mathfrak K_A
\rightharpoonup
\mathfrak K_B,
}
\]

其中 \(\mathfrak K_A,\mathfrak K_B\) 分別是兩個判定域中的可判定知識物件空間，而 \(\rightharpoonup\) 明確允許映射為 partial。跨域過程不應被簡化成「翻譯」；同一來源資訊可能被完整保留、重新編碼、嵌入更豐富空間、投影成較粗表示、拆成多個目標概念、由多個來源概念合併、重新詮釋，或根本缺乏合法對應。

本文提出九種第一階 bridge type：

\[
\boxed{
IDENTITY,\;
EQUIVALENT,\;
EMBED,\;
PROJECT,\;
SPLIT,\;
MERGE,\;
REINTERPRET,\;
PARTIAL,\;
INCOMPARABLE.
}
\]

並將「保真」改寫成 query-relative preservation。對查詢集合 \(\mathcal Q\)，若來源與目標經 bridge 後的相關回答保持一致，則：

\[
\boxed{
\mathcal M_{A\to B}
\text{ preserves }
\mathcal Q.
}
\]

這避免要求所有跨域映射都必須是全域雙射。本文進一步定義 bridge fiber、information collapse、distinction loss、round-trip defect、reconstruction debt 與 Domain Bridge Certificate。

Institution Theory 已提供一個高度相關的抽象框架：signature translation 與 model reduct 若滿足 satisfaction condition，則真值在「換記號」後保持；近年的 Coq formalization 也已形式化部分 institution machinery 與 satisfaction condition。Abstract Interpretation 則透過 abstraction / concretization 與 Galois connections 處理 sound abstraction，並明確接受 abstraction 可能犧牲部分區分能力。OWL 與 SKOS 更直接區分 individual identity、class equivalence、exact match 與 close match，顯示跨知識系統的 mapping 強度本來就不應只有一種。

本文因此不宣稱首次提出 logic translation、ontology alignment、abstraction、Galois connection 或 semantic mapping。本文較窄的工作是：把跨域映射接入 DTIL 已有的 Semantic Identity、Classification State、Q4 State、History 與 Transition Boundary，使「一份信息穿越判定域後，究竟保留了哪些判定能力、丟掉了哪些 distinction、又新增了哪些 distinction」成為可保存與可驗證的歷史物件。

本文的核心命題是：

\[
\boxed{
\text{cross-domain sameness is preservation-relative, not label-relative}.
}
\]

以及：

\[
\boxed{
\text{a successful translation does not imply a lossless translation}.
}
\]

**關鍵詞：** Judgment Domain；Cross-Domain Mapping；Information Loss；Institution Theory；Abstract Interpretation；Galois Connection；Ontology Mapping；DTIL；Semantic Preservation；Domain Bridge

---

# 1. 問題：信息真的能「直接搬過去」嗎？

假設在來源判定域：

\[
\mathcal J_A
\]

有一個知識物件：

\[
K_A.
\]

系統希望把它放進：

\[
\mathcal J_B.
\]

最天真的寫法是：

\[
K_A
\rightarrow
K_B.
\]

但這隱含了大量未檢查假設：

1. A 和 B 的對象類型相同嗎？
2. 兩邊使用相同分類嗎？
3. 同一符號是否表示同一概念？
4. A 中的 distinction 在 B 中存在嗎？
5. B 是否比 A 更粗？
6. B 是否比 A 更細？
7. A 的 truth / support 狀態能直接搬過去嗎？
8. A 的 history 在 B 中仍可表達嗎？
9. 映射能否反向？
10. 一個 A 概念是否會在 B 中分裂成多個概念？

因此：

\[
\boxed{
\text{cross-domain transfer}
\neq
\text{copy}.
}
\]

---

# 2. 判定域不是只有 Vocabulary

沿用：

\[
\mathcal J
\]

作為 Judgment Domain。

它至少可以包含：

\[
\boxed{
\mathcal J
=
(
\mathcal O,
\mathcal L,
\mathcal R,
\mathcal D,
\Theta,
\mathcal Q
).
}
\]

其中：

- \(\mathcal O\)：允許的 object types；
- \(\mathcal L\)：classification / concept vocabulary；
- \(\mathcal R\)：relations / operators；
- \(\mathcal D\)：definitions；
- \(\Theta\)：thresholds / decision policies；
- \(\mathcal Q\)：被允許或重要的 query family。

因此「換判定域」可能同時改變：

\[
\boxed{
\text{language}
+
\text{objects}
+
\text{rules}
+
\text{questions}.
}
\]

---

# 3. 跨域知識物件

令：

\[
\boxed{
K_A
=
(
\Psi_A,
\Phi_A,
\Gamma_A,
\nu_A,
E_A,
H_A
)
}
\]

表示來源域中的一個知識物件。

其中：

- \(\Psi_A\)：semantic identity；
- \(\Phi_A\)：formal / structural identity；
- \(\Gamma_A\)：classification state；
- \(\nu_A\)：Q4 state；
- \(E_A\)：evidence state；
- \(H_A\)：history。

跨域映射：

\[
\boxed{
\mathcal M_{A\to B}(K_A)
=
K_B.
}
\]

但：

\[
K_B
\]

不必與：

\[
K_A
\]

逐欄相同。

---

# 4. Bridge 是有型別的

本文定義：

\[
\boxed{
\mathcal B_{A\to B}
=
(
\mathcal M,
\tau,
\mathcal P,
\mathcal L,
\mathcal V
)
}
\]

其中：

- \(\mathcal M\)：mapping；
- \(\tau\)：bridge type；
- \(\mathcal P\)：preservation profile；
- \(\mathcal L\)：loss / gain profile；
- \(\mathcal V\)：verification status。

所以 bridge 本身也是：

\[
\boxed{
\text{first-class knowledge object}.
}
\]

---

# 5. 九種第一階 Bridge Type

定義：

\[
\boxed{
\mathcal T_B
=
\{
IDENTITY,
EQUIVALENT,
EMBED,
PROJECT,
SPLIT,
MERGE,
REINTERPRET,
PARTIAL,
INCOMPARABLE
\}.
}
\]

它們不是互相絕對排他的宇宙分類，而是第一版 runtime taxonomy。

---

# 6. IDENTITY

若：

\[
\mathcal J_A
\]

和：

\[
\mathcal J_B
\]

在指定工作範圍內其實是同一判定域，只是 instance / version pointer 不同，

則：

\[
\boxed{
\tau=IDENTITY.
}
\]

要求：

\[
\mathcal M
\approx
Id.
\]

---

# 7. EQUIVALENT

若兩域表示不同，

但在指定 query family：

\[
\mathcal Q
\]

下不可區分：

\[
\boxed{
Ans_A(q,K)
=
Ans_B(q,\mathcal M(K))
}
\]

對所有：

\[
q\in\mathcal Q,
\]

則：

\[
\boxed{
\mathcal J_A
\equiv_{\mathcal Q}
\mathcal J_B.
}
\]

這是 query-relative equivalence。

---

# 8. Equivalent 不要求字面相同

OWL 2 已明確區分 structural equivalence 與 semantic equivalence；兩個 class expressions 即使結構不同，也可能語義等價。OWL 的 `EquivalentClasses` 表示 class expressions 在該 ontology semantics 下具有相同 extension。

因此：

\[
\boxed{
\text{same structure}
\neq
\text{same semantics}
}
\]

且：

\[
\boxed{
\text{different structure}
\not\Rightarrow
\text{different semantics}.
}
\]

這與 Series I / Bridge Paper 的基本區分一致。

---

# 9. EMBED

若：

\[
\mathcal J_B
\]

比：

\[
\mathcal J_A
\]

更豐富，

而 A 的 distinction 可以被嵌入 B：

\[
\boxed{
\iota_{A\to B}:
\mathfrak K_A
\hookrightarrow
\mathfrak K_B,
}
\]

則：

\[
\tau=EMBED.
\]

理想情況下：

\[
\iota
\]

是 injective，

不同來源 object 不被合併。

---

# 10. EMBED 可以增加目標資訊

如果 B 有更多分類維度，

來源：

\[
K_A
\]

進入 B 後可能得到：

\[
K_B
=
\iota(K_A)
+
\text{new distinctions}.
\]

所以：

\[
\boxed{
\text{information crossing}
}
\]

不一定只有 loss。

也可能：

\[
\boxed{
\text{gain through target-domain enrichment}.
}
\]

---

# 11. PROJECT

若：

\[
\mathcal J_B
\]

比 A 更粗，

則可能有：

\[
\boxed{
\pi_{A\to B}:
\mathfrak K_A
\twoheadrightarrow
\mathfrak K_B.
}
\]

多個 A states 被投影成同一 B state。

這是：

\[
\boxed{
\tau=PROJECT.
}
\]

---

# 12. Projection 的 Information Loss

若：

\[
K_1\neq K_2
\]

但：

\[
\pi(K_1)
=
\pi(K_2),
\]

則 B 無法再區分這兩個來源狀態。

所以定義：

\[
\boxed{
K_1
\sim_{\pi}
K_2
\iff
\pi(K_1)=\pi(K_2).
}
\]

這是由 projection 誘導的 indistinguishability relation。

---

# 13. Bridge Fiber

對目標 object：

\[
y\in\mathfrak K_B,
\]

定義：

\[
\boxed{
Fib_{\mathcal M}(y)
=
\{
x\in\mathfrak K_A:
\mathcal M(x)=y
\}.
}
\]

若：

\[
|Fib_{\mathcal M}(y)|>1,
\]

代表多個來源 distinction 被合併。

因此：

\[
\boxed{
\text{nontrivial fiber}
=
\text{potential information collapse}.
}
\]

---

# 14. Distinction Loss

來源中可區分的：

\[
x_1\neq_A x_2
\]

如果到了 B：

\[
\mathcal M(x_1)
=
_B
\mathcal M(x_2),
\]

則定義：

\[
\boxed{
Loss_D(x_1,x_2\mid\mathcal M)=1.
}
\]

這裡 loss 不是 byte 數量，

而是：

\[
\boxed{
\text{loss of a judgment-relevant distinction}.
}
\]

---

# 15. SPLIT

一個來源概念：

\[
X_A
\]

在目標域可能需要拆成：

\[
Y_{B,1},
Y_{B,2},
\ldots,Y_{B,n}.
\]

因此：

\[
\boxed{
\mathcal M(X_A)
=
\{
Y_{B,1},\ldots,Y_{B,n}
\}.
}
\]

稱：

\[
\tau=SPLIT.
\]

---

# 16. Split 為什麼發生？

可能因：

- B 有更細 taxonomy；
- B 把 A 原本混在一起的概念拆開；
- target context 要求額外 distinction；
- source term 本身多義。

因此 Split 不必代表 A 錯。

它可能只是：

\[
\boxed{
\text{target domain is more discriminating}.
}
\]

---

# 17. MERGE

反方向，

來源多個概念：

\[
X_{A,1},X_{A,2}
\]

在 B 中都變成：

\[
Y_B.
\]

即：

\[
\boxed{
\mathcal M(X_{A,1})
=
\mathcal M(X_{A,2})
=
Y_B.
}
\]

稱：

\[
\tau=MERGE.
\]

它本質上具有：

\[
\boxed{
\text{many-to-one collapse}.
}
\]

---

# 18. Split / Merge 不一定互為完美逆運算

如果：

\[
X_A
\mapsto
\{Y_1,Y_2\},
\]

之後：

\[
\{Y_1,Y_2\}
\mapsto
X'_A,
\]

不保證：

\[
X'_A=X_A.
\]

因為 split 過程可能加入新的 distinction，

merge 過程又可能使用不同規則。

因此：

\[
\boxed{
MERGE\circ SPLIT
\neq
Id
}
\]

一般完全可能。

---

# 19. REINTERPRET

如果同一 surface content 在目標域中被重新賦予另一套 semantic role：

\[
\Psi_A
\neq
\Psi_B,
\]

則：

\[
\boxed{
\tau=REINTERPRET.
}
\]

這不是普通 translation。

---

# 20. Reinterpretation 可能形式完全合法

例如相同符號：

\[
X
\]

在 A、B 中都有定義，

但：

\[
\rho_A(X)\neq\rho_B(X).
\]

所以：

\[
\boxed{
\text{surface-preserving crossing}
}
\]

反而可能是最危險的一種 crossing。

---

# 21. PARTIAL

若只有部分來源 object 可被合法映射：

\[
\boxed{
\mathcal M:
\mathfrak K_A
\rightharpoonup
\mathfrak K_B,
}
\]

則：

\[
\tau=PARTIAL.
\]

對：

\[
x\notin Dom(\mathcal M)
\]

不應猜一個目標值。

應明確標：

```text
UNMAPPED
```

---

# 22. INCOMPARABLE

若目前缺乏：

- shared object identity；
- semantic bridge；
- query-preserving translation；
- defensible alignment；

則：

\[
\boxed{
\tau=INCOMPARABLE.
}
\]

這是一個合法結果。

不是 mapping failure 必須被 AI「補完」。

---

# 23. 不可比不是未知的同義詞

`UNKNOWN` 表示：

> 目前不知道 mapping。

`INCOMPARABLE` 表示：

> 在指定 criteria / query family 下，沒有足夠結構建立所要求的比較。

因此：

\[
\boxed{
UNKNOWN
\neq
INCOMPARABLE.
}
\]

---

# 24. SKOS 提供 Mapping Strength 的現成啟發

SKOS 明確區分：

- `exactMatch`；
- `closeMatch`。

`exactMatch` 表示可在廣泛資訊檢索應用中高度可信地交換使用；

`closeMatch` 則只是足夠相似，並不主張完全等同。

OWL 又有：

- `sameAs`：individual identity；
- `equivalentClass`：class extension equivalence。

因此：

\[
\boxed{
\text{identity}
\neq
\text{class equivalence}
\neq
\text{exact conceptual match}
\neq
\text{close match}.
}
\]

這正支持 typed bridge，而不是 `same=true/false`。

---

# 25. Institution Theory 的核心啟發

Institution Theory 以 signatures、sentences、models 與 satisfaction relation 抽象描述邏輯系統。

對 signature morphism：

\[
\sigma:
\Sigma_A
\rightarrow
\Sigma_B,
\]

sentence translation 與 model reduct 必須滿足 satisfaction condition：

\[
\boxed{
M_B
\models_B
Sen(\sigma)(\varphi)
\iff
Mod(\sigma)(M_B)
\models_A
\varphi.
}
\]

其直覺常被概括為：

\[
\boxed{
\text{truth is invariant under change of notation}.
}
\]

近年的 Coq 工作已形式化部分 institution theory、institution morphisms 與 satisfaction conditions。

---

# 26. DTIL 與 Institution Theory 的關係

如果：

\[
\mathcal J_A,\mathcal J_B
\]

本身是可形式化 logic domains，

Institution Theory 可以作為：

\[
\boxed{
\text{truth-preserving bridge criterion}.
}
\]

但 DTIL 的 Judgment Domain 更寬，

還可能包含：

- thresholds；
- semantic referents；
- historical operators；
- classification policies；
- non-formal human criteria。

因此：

\[
\boxed{
\text{Institution}
}
\]

可作為某些 \(\mathcal J\) 的形式子結構，

但不必等同全部 Judgment Domain。

---

# 27. Satisfaction Preservation

對 bridge：

\[
\mathcal M_{A\to B},
\]

若對指定命題族：

\[
\Phi_Q
\]

有：

\[
\boxed{
Sat_A(\phi,K)
=
Sat_B(
\mathcal M_\phi(\phi),
\mathcal M_K(K)
)
}
\]

則可以標：

```text
SATISFACTION_PRESERVING
```

這是一種很強的 bridge property。

---

# 28. 但 Satisfaction Preservation 仍可能不保留全部資訊

一個 translation 可以保持指定 formula 的 satisfaction，

但不保證：

- 所有 source distinctions；
- 所有 classification；
- provenance；
- history；
- semantic nuance；

都可逆保存。

因此：

\[
\boxed{
\text{truth preservation}
\neq
\text{information preservation}.
}
\]

---

# 29. Abstract Interpretation 的核心啟發

Abstract Interpretation 使用：

\[
\alpha:
C\rightarrow A
\]

與：

\[
\gamma:
A\rightarrow C
\]

在 concrete domain 與 abstract domain 間建立關係。

Galois connection 提供一種 sound abstraction / concretization 框架。

這種框架的核心精神是：

\[
\boxed{
\text{abstraction may deliberately forget distinctions while preserving sound reasoning properties}.
}
\]

---

# 30. DTIL 的 Project Bridge 可借用這種思想

如果：

\[
\mathcal J_B
\]

是 A 的 abstraction，

可以定義：

\[
\alpha_{A\to B}
\]

以及可能的：

\[
\gamma_{B\to A}.
\]

但：

\[
\gamma(\alpha(x))
\]

通常不需要等於：

\[
x.
\]

因此：

\[
\boxed{
\text{round trip may reconstruct a safe envelope, not the original state}.
}
\]

---

# 31. Round-Trip Mapping

若存在：

\[
\mathcal M_{A\to B}
\]

和：

\[
\mathcal M_{B\to A},
\]

定義：

\[
\boxed{
RT_A
=
\mathcal M_{B\to A}
\circ
\mathcal M_{A\to B}.
}
\]

理想 identity bridge：

\[
RT_A=Id_A.
\]

一般則：

\[
RT_A\neq Id_A.
\]

---

# 32. Round-Trip Defect

定義：

\[
\boxed{
D_{RT}(x)
=
\Delta_A(
x,
RT_A(x)
).
}
\]

它回答：

> 信息去 B 再回 A 後，和原本差多少？

\[
D_{RT}
\]

仍是一個 typed difference，

不是預設 scalar。

---

# 33. Lossless Bridge

若對指定子域：

\[
S\subseteq\mathfrak K_A
\]

以及 query family：

\[
\mathcal Q
\]

有：

\[
RT_A(x)
\equiv_{\mathcal Q}
x
\]

對所有：

\[
x\in S,
\]

則稱：

\[
\boxed{
\mathcal M
\text{ is lossless relative to }
(S,\mathcal Q).
}
\]

不是絕對「無損」。

---

# 34. Query-Relative Preservation

定義：

\[
\boxed{
Pres_{\mathcal Q}(
\mathcal M
)=1
}
\]

若：

\[
\forall q\in\mathcal Q,
\quad
Ans_A(q,K)
=
Ans_B(
\mu_Q(q),
\mathcal M(K)
).
\]

其中：

\[
\mu_Q
\]

是 query translation。

這是一個比「所有內容完全一樣」更實用的保真定義。

---

# 35. 為什麼 Query 必須一起翻譯？

如果 A 問：

> X 是否屬於 subclass \(Y_1\)？

但 B 根本沒有：

\[
Y_1
\]

這個 distinction，

那麼不能只搬 K，

還必須問：

\[
\boxed{
\text{the query itself has a target-domain meaning?}
}
\]

所以 bridge 至少有：

\[
\boxed{
\mathcal M_K
+
\mathcal M_Q.
}
\]

---

# 36. Query 不可映射

可能：

\[
q_A
\]

在 B 中沒有合法 query：

\[
\mu_Q(q_A)
\]

不存在。

則：

```text
QUERY_UNMAPPABLE
```

而不是：

```text
answer = false
```

因此：

\[
\boxed{
\text{cannot ask}
\neq
\text{answer is no}.
}
\]

---

# 37. Distinction Preservation Profile

定義：

\[
\boxed{
\mathcal P_D(\mathcal M)
=
(
P_O,
P_\Psi,
P_\Phi,
P_\Gamma,
P_\nu,
P_E,
P_H,
P_Q
).
}
\]

其中分別表示：

- object identity preservation；
- semantic identity；
- formal structure；
- classification；
- Q4 state；
- evidence；
- history；
- query answerability。

---

# 38. Preservation 不一定全為布林值

每項可以是：

```text
PRESERVED
PARTIALLY_PRESERVED
COLLAPSED
SPLIT
REINTERPRETED
UNMAPPED
UNKNOWN
```

因此：

\[
\boxed{
\text{preservation is typed, not binary}.
}
\]

---

# 39. Q4 State 可以跨域直接搬嗎？

一般不行。

因為：

\[
\nu_A(P)
\]

是相對：

\[
\mathcal J_A.
\]

所以：

\[
\boxed{
\nu_A(P)=\mathbf Y
}
\]

不能自動推出：

\[
\boxed{
\nu_B(\mathcal M(P))=\mathbf Y.
}
\]

除非 bridge 已證明相關判定與 evidence semantics 被保留。

---

# 40. Source-Y 可以變 Target-U

例如：

A 有充分資料與規則證明：

\[
P.
\]

所以：

\[
\nu_A(P)=\mathbf Y.
\]

但 B 缺少對應 evidence relation 或 query vocabulary。

則：

\[
\nu_B(\mathcal M(P))=\mathbf U
\]

完全可能。

這不是 P 從真變未知。

而是：

\[
\boxed{
\text{target domain cannot reconstruct the source judgment}.
}
\]

---

# 41. Source-Y 也可能變 Target-B

如果 B 的 merge 將兩個來源 distinction 合併，

而其中一個支持、

另一個反對，

則 target representation 可能出現：

\[
\mathbf B.
\]

因此：

\[
\boxed{
\text{projection can manufacture local conflict from collapsed distinctions}.
}
\]

這不是 world 產生矛盾，

而可能是 mapping artifact。

---

# 42. Mapping-Induced Conflict

定義：

\[
\boxed{
\mathbf B_{\mathrm{map}}
}
\]

表示：

> target local conflict 主要來自 cross-domain merge / projection。

它應與原本：

\[
\mathbf B_{\mathrm{source}}
\]

分開。

---

# 43. Mapping-Induced Uncertainty

同樣可定義：

\[
\boxed{
\mathbf U_{\mathrm{map}}
}
\]

表示：

> source 有資訊，但 target bridge 沒有足夠能力重建。

所以：

\[
\boxed{
\text{target uncertainty}
\neq
\text{source ignorance}.
}
\]

---

# 44. Classification Mapping

對：

\[
\Gamma_A(\omega),
\]

bridge 可能：

\[
\boxed{
\mu_\Gamma:
2^{\mathcal L_A}
\rightarrow
2^{\mathcal L_B}.
}
\]

這個 mapping 可以：

- preserve；
- split；
- merge；
- refine；
- generalize；
- drop classes。

---

# 45. Split Classification

若：

\[
X_A
\mapsto
\{Y_1,Y_2\},
\]

不能直接把：

\[
X_A
\]

視為：

\[
Y_1
\]

或：

\[
Y_2.
\]

必須保存：

```text
mapping_type = SPLIT
```

以及 split rule。

---

# 46. Merge Classification

若：

\[
X_1,X_2
\mapsto
Y,
\]

則 B 中：

\[
Y
\]

不能反向唯一恢復：

\[
X_1
\]

或：

\[
X_2.
\]

所以：

\[
\boxed{
\text{merge creates inverse ambiguity}.
}
\]

---

# 47. Semantic Crossing

對：

\[
\Psi_A
\rightarrow
\Psi_B,
\]

最重要問題不是：

> 字是不是一樣？

而是：

\[
\boxed{
\rho_A
\stackrel{?}{\sim}
\rho_B.
}
\]

即 pre-symbolic referent / conceptual target 是否仍然對應。

---

# 48. Surface-Preserving Semantic Loss

可能：

\[
s_A=s_B,
\]

但：

\[
\rho_A\neq\rho_B.
\]

這是：

\[
\boxed{
\text{same word, different target}.
}
\]

所以 surface-preserving bridge 反而可能是 REINTERPRET。

---

# 49. Surface-Changing Semantic Preservation

也可能：

\[
s_A\neq s_B,
\]

但：

\[
\rho_A\approx\rho_B,
\]

\[
d_A\approx d_B.
\]

這是：

\[
\boxed{
\text{translation with semantic preservation}.
}
\]

---

# 50. History Crossing

來源 history：

\[
H_A
\]

進入 B 後可能只有：

\[
H_B.
\]

如果 B 不支援某些歷史 operator，

例如：

\[
Again,
ReturnCause,
BoundaryRevision,
\]

則：

\[
\boxed{
\text{current-state transfer may succeed while history transfer fails}.
}
\]

---

# 51. History-Preserving Bridge

對 operator set：

\[
\mathcal O_H,
\]

若：

\[
\forall O\in\mathcal O_H:
O(H_A)
=
O_B(
\mathcal M_H(H_A)
),
\]

則稱：

\[
\boxed{
\mathcal M_H
\text{ preserves }
\mathcal O_H.
}
\]

這是 query-relative history preservation。

---

# 52. 「又」可能在跨域後消失

來源：

\[
H_A
=
(Y,N,Y)
\]

有：

\[
Again_Y=1.
\]

如果 B 只保存 current state：

\[
Y,
\]

則：

\[
Again_Y
\]

無法恢復。

所以：

\[
\boxed{
\text{endpoint-preserving bridge}
\not\Rightarrow
\text{history-preserving bridge}.
}
\]

---

# 53. Crossing Boundary 本身也要進 History

跨域事件：

\[
\mathcal J_A
\xrightarrow{\mathcal M}
\mathcal J_B
\]

應建立：

\[
\boxed{
DOMAIN\_CROSSING
}
\]

transition record。

它至少保存：

- source domain；
- target domain；
- bridge ID；
- mapping type；
- preservation profile；
- loss / gain；
- verification。

---

# 54. Domain-Crossing Difference Packet

定義：

\[
\boxed{
\Delta_{A\to B}
=
(
\Delta_\Psi,
\Delta_\Phi,
\Delta_\Gamma,
\Delta_\nu,
\Delta_E,
\Delta_H
).
}
\]

注意：

\[
\Delta J
\]

在跨域中當然成立，

所以改由：

\[
(\mathcal J_A,\mathcal J_B,\mathcal M)
\]

直接表示。

---

# 55. Cross-Domain Judgment Friction

定義：

\[
\boxed{
\mathfrak F_{A\to B}
=
\mathcal F(
K_A,
K_B,
\mathcal B_{A\to B},
\Delta_{A\to B}
).
}
\]

它衡量的不是：

> A 與 B 有多不同？

而是：

> **這次穿越為了讓 A 的資訊可在 B 中使用，發生了哪些結構變化？**

---

# 56. Friction 與 Loss 不同

可能：

\[
\mathfrak F\gg0
\]

但：

\[
Loss=0.
\]

例如完整可逆的 representation change：

\[
A\leftrightarrow B.
\]

雖然格式差異巨大，

資訊完全可恢復。

因此：

\[
\boxed{
\text{difference}
\neq
\text{loss}.
}
\]

---

# 57. Loss 與 Error 也不同

有意 abstraction：

\[
A\rightarrow B
\]

可能 deliberately 丟掉 detail，

但對指定 query：

\[
\mathcal Q
\]

仍完全 sound。

所以：

\[
\boxed{
\text{lossy}
\neq
\text{wrong}.
}
\]

---

# 58. Information Gain 也不等於 Bridge 幻覺

如果 B 增加 target-native distinctions，

必須區分：

### Derived Gain

由 B 的規則合法推導的新資訊。

### Assumed Gain

由人工或模型新增但未驗證的資訊。

因此：

\[
\boxed{
\text{target enrichment}
\neq
\text{free information creation}.
}
\]

---

# 59. Gain Provenance

每個 target-only distinction：

```text
origin = TARGET_RULE
origin = EXTERNAL_EVIDENCE
origin = MODEL_INFERENCE
origin = HUMAN_ASSERTION
```

必須保留 provenance。

---

# 60. Reconstruction

如果 B 是 lossy projection，

系統想回到 A，

需要：

\[
\boxed{
\mathcal R_{B\to A}.
}
\]

但 reconstruction 可能輸出：

\[
\{x_1,x_2,\ldots\}
\]

而不是唯一 x。

---

# 61. Reconstruction Set

定義：

\[
\boxed{
Rec_A(y)
=
Fib_{\mathcal M}(y).
}
\]

如果 fiber 有多個元素，

則：

\[
\boxed{
\text{inverse reconstruction is set-valued}.
}
\]

---

# 62. Reconstruction Debt

如果 target 系統未保存足以選出來源 member 的資訊，

則建立：

\[
\boxed{
D_R(y)
=
\text{Reconstruction Debt}.
}
\]

它表示：

> 要恢復來源 distinction，還缺什麼？

---

# 63. Reconstruction Debt 可以被外部資訊清償

如果後來加入：

\[
E'
\]

使：

\[
Fib_{\mathcal M}(y)
\]

從多個候選縮成：

\[
\{x^\ast\},
\]

則：

\[
D_R
\rightarrow0.
\]

所以跨域 information loss 不一定永久不可恢復。

---

# 64. Irrecoverable Collapse

如果原來源 provenance 已消失，

又沒有其他辨識資訊，

則可能：

\[
\boxed{
D_R=\text{IRRECOVERABLE}.
}
\]

這需要和：

```text
NOT_YET_RECONSTRUCTED
```

區分。

---

# 65. Round-Trip Unit Test 是核心

每個 bridge 應盡量測：

\[
A
\rightarrow
B
\rightarrow
A.
\]

比較：

\[
K_A
\]

與：

\[
K_A'.
\]

至少輸出：

```text
round_trip:
    semantic
    classification
    q4
    history
    query_answers
```

---

# 66. Bridge Composition

若：

\[
\mathcal J_A
\xrightarrow{\mathcal M_{AB}}
\mathcal J_B
\xrightarrow{\mathcal M_{BC}}
\mathcal J_C,
\]

則：

\[
\boxed{
\mathcal M_{AC}
=
\mathcal M_{BC}
\circ
\mathcal M_{AB}.
}
\]

但 preservation profile 不可天真相乘。

---

# 67. Loss 可以累積

即使：

\[
A\to B
\]

只丟一點，

\[
B\to C
\]

又丟一點，

最終：

\[
A\to C
\]

可能失去關鍵 distinction。

所以：

\[
\boxed{
\text{small local loss}
\not\Rightarrow
\text{small global loss}.
}
\]

---

# 68. Split 後 Merge 可能造成新 Conflict

例如：

\[
X_A
\mapsto
Y_1,Y_2
\]

後，

另一 bridge 又把：

\[
Y_1,Y_2
\mapsto
Z.
\]

若兩個 branch 的 evidence status 不同，

Z 可能得到：

\[
\mathbf B.
\]

所以 bridge composition 可以創造 mapping-induced Q4 effect。

---

# 69. Bridge Non-Commutativity

若有：

\[
A\to B\to C
\]

與：

\[
A\to D\to C,
\]

兩條 route 最終可能產生不同：

\[
K_C.
\]

因此：

\[
\boxed{
\mathcal M_{BC}\circ\mathcal M_{AB}
\neq
\mathcal M_{DC}\circ\mathcal M_{AD}
}
\]

完全可能。

所以：

\[
\boxed{
\text{cross-domain route itself is information}.
}
\]

---

# 70. Domain Path

跨多域歷史：

\[
\boxed{
P_J
=
(
\mathcal J_0,
\mathcal M_{01},
\mathcal J_1,
\mathcal M_{12},
\ldots,
\mathcal J_n
).
}
\]

這是判定域層的 path。

它可以接入 Paper II 的 Again：

> 是否又回到原判定域？

---

# 71. Domain Again

若：

\[
\mathcal J_0
\rightarrow
\mathcal J_1
\rightarrow
\mathcal J_0,
\]

則有：

\[
\boxed{
\mathsf{AgainDomain}_{\mathcal J_0}=1.
}
\]

但仍然：

\[
\boxed{
\text{domain label return}
\neq
\text{information-state reset}.
}
\]

因為跨出去又回來後，

history 與 knowledge 可能已變。

---

# 72. Domain Return Round-Trip

回到：

\[
\mathcal J_A
\]

後，

比較：

\[
K_A^{(0)}
\]

與：

\[
K_A^{(2)}.
\]

可能：

\[
K_A^{(0)}
=
_{\mathrm{classification}}
K_A^{(2)},
\]

但：

\[
K_A^{(0)}
\neq_{\mathrm{history}}
K_A^{(2)}.
\]

甚至：

\[
K_A^{(0)}
\neq_{\mathrm{semantic}}
K_A^{(2)}.
\]

---

# 73. Domain Bridge Algebra：第一版關係

本文暫時只建立 composition-level rules。

例如：

\[
IDENTITY\circ X=X.
\]

而：

\[
PROJECT\circ EMBED
\]

可能：

- lossless；
- lossy；
- identity-relative-to-\(\mathcal Q\)。

沒有單一固定結果。

所以：

\[
\boxed{
\text{bridge type composition needs side conditions}.
}
\]

---

# 74. EQUIVALENT Composition

如果：

\[
A\equiv_{\mathcal Q}B
\]

且：

\[
B\equiv_{\mathcal Q}C,
\]

在 query translations 可一致 compose 的前提下，

可期待：

\[
A\equiv_{\mathcal Q}C.
\]

但如果每一段 preservations 對不同 query set，

則不能直接傳遞。

---

# 75. Preservation Intersection

若：

\[
M_{AB}
\]

保留：

\[
\mathcal Q_1,
\]

而：

\[
M_{BC}
\]

保留：

\[
\mathcal Q_2,
\]

則最保守：

\[
\boxed{
\mathcal Q_{AC}^{pres}
\subseteq
\mathcal Q_1
\cap
\mathcal Q_2
}
\]

經適當 query translation 後成立。

---

# 76. Bridge Verification

Bridge 至少需要：

\[
\boxed{
\mathbf V_B
=
(
V_{\mathrm{object}},
V_{\mathrm{semantic}},
V_{\mathrm{query}},
V_{\mathrm{classification}},
V_{\mathrm{history}},
V_{\mathrm{roundtrip}}
).
}
\]

---

# 77. Object Verification

是否真的：

\[
\omega_A
\equiv_O
\omega_B?
\]

這是 individual identity / anchoring 問題。

OWL 的 `SameIndividual` / `sameAs` 類概念提供強 identity 語義的形式近鄰。

---

# 78. Class Equivalence 不等於 Individual Identity

OWL 清楚區分：

\[
SameIndividual
\]

與：

\[
EquivalentClasses.
\]

所以：

\[
\boxed{
\text{same object}
\neq
\text{same class extension}.
}
\]

這與 Series II / Paper III 的：

\[
I_O\neq I_C
\]

一致。

---

# 79. Class Extension Equivalence 也不等於概念意涵完全相同

OWL 舊版 reference 甚至特別提醒：兩 class descriptions 可以 extension 相同，但 intensional meaning 不一定相同。

因此：

\[
\boxed{
\text{extensional equivalence}
\neq
\text{intensional semantic identity}.
}
\]

這直接支持 DTIL 的：

\[
I_C
\neq
I_S.
\]

---

# 80. Semantic Verification

Semantic bridge 應問：

- source referent；
- target referent；
- retained distinctions；
- lost distinctions；
- new distinctions；
- known ambiguities。

輸出：

```text
ALIGNED
CLOSE
SPLIT
MERGED
RETARGETED
UNMAPPED
```

---

# 81. Query Verification

對測試 query set：

\[
\mathcal Q_{test},
\]

執行：

\[
Ans_A(q)
\]

與：

\[
Ans_B(\mu_Q(q)).
\]

比較 preservation。

這形成：

\[
\boxed{
\text{behavioral bridge test}.
}
\]

---

# 82. History Verification

給一組 history：

\[
H_A^{(1)},\ldots,H_A^{(n)},
\]

檢查：

\[
Now,
Once,
Again,
ReturnCount,
BoundaryCause
\]

在 target 是否仍可回答。

---

# 83. Bridge Certificate

本文提出：

\[
\boxed{
DBC
=
\text{Domain Bridge Certificate}.
}
\]

最小欄位：

```text
bridge_id

source_domain
target_domain

mapping_type
mapping_rules

object_mapping
semantic_mapping
classification_mapping
query_mapping
history_mapping

preservation_profile
loss_profile
gain_profile

unmapped_items
incomparable_items

round_trip_status
verification_vector

provenance
version
```

---

# 84. Bridge 也要版本化

如果 target ontology / definitions 更新，

舊 bridge 可能失效。

因此：

```text
BRIDGE-v2 --REPLACES--> BRIDGE-v1
```

而不是 overwrite。

---

# 85. Bridge Drift

定義：

\[
\boxed{
\Delta\mathcal M_t
}
\]

表示 cross-domain mapping 本身隨時間改變。

這是：

\[
\boxed{
\text{bridge drift}.
}
\]

所以不只有 knowledge drift，

連 translation / alignment rule 也會變。

---

# 86. Bridge Drift 會改寫歷史解釋

同一筆過去資訊：

\[
K_A
\]

用：

\[
M^{(1)}
\]

映射可能得到：

\[
K_B^{(1)}.
\]

後來 bridge 更新：

\[
M^{(2)}
\]

可能得到：

\[
K_B^{(2)}.
\]

所以：

\[
\boxed{
\text{historical cross-domain interpretation is version-dependent}.
}
\]

---

# 87. 不要靜默重算歷史

如果 bridge 更新，

舊 target record 不應直接被默默改寫。

而應：

```text
K-B-v2 --REINTERPRETS--> K-B-v1
```

並保存：

```text
bridge_version = ...
```

---

# 88. Crossing Debt

如果大量 information 已跨域，

但：

- semantic mapping 未審核；
- round trip 未測；
- history 未保存；

則可以定義：

\[
\boxed{
D_X
=
\text{Crossing Debt}.
}
\]

高 downstream-impact bridge 優先清償。

---

# 89. Information Loss Ledger

每次 bridge 可保存：

```text
lost:
    distinctions
    queries
    provenance
    history
    class_resolution

gained:
    distinctions
    derived_relations
    target_native_annotations
```

因此 loss / gain 不再只是口頭描述。

---

# 90. 最小 Runtime Schema

```text
JudgmentDomain:
    domain_id
    object_types
    vocabulary
    rules
    definitions
    query_family
    version

DomainBridge:
    bridge_id
    source_domain
    target_domain
    bridge_type
    mapping_rules
    preservation_profile
    loss_profile
    verification
    version

CrossingEvent:
    source_object
    source_state
    bridge_id
    target_state
    difference_packet
    round_trip_test
    timestamp
```

---

# 91. Minimal Crossing Algorithm

```text
cross(K_A, bridge):
    validate_bridge_domain(
        K_A,
        bridge.source_domain
    )

    mapped = apply_mapping(
        K_A,
        bridge.mapping_rules
    )

    if mapped is undefined:
        return UNMAPPED

    K_B = evaluate_in_target_domain(
        mapped,
        bridge.target_domain
    )

    preservation = compare_preservation(
        K_A,
        K_B,
        bridge
    )

    loss_gain = compute_loss_gain(
        K_A,
        K_B,
        bridge
    )

    certificate = issue_domain_bridge_record(
        K_A,
        K_B,
        preservation,
        loss_gain
    )

    append_domain_crossing_history(
        certificate
    )

    return K_B
```

---

# 92. Unit Test 1：Pure Re-encoding

A：

```text
label = YES
```

B：

```text
label = Y
```

semantic / query / history 完全保留。

要求：

```text
bridge_type = EQUIVALENT
loss = NONE_RELATIVE_TO_TEST_QUERIES
```

---

# 93. Unit Test 2：Projection Loss

A 分：

\[
X_1,X_2.
\]

B 只有：

\[
X.
\]

且：

\[
X_1,X_2\mapsto X.
\]

要求：

```text
bridge_type = MERGE
distinction_loss = true
round_trip_unique = false
```

---

# 94. Unit Test 3：Split

A：

\[
X.
\]

B：

\[
Y_1,Y_2.
\]

要求：

```text
bridge_type = SPLIT
target_selection_requires_context = true
```

若兩者都合法則保存 set-valued mapping。

---

# 95. Unit Test 4：Source Y → Target U

A 可證：

\[
P.
\]

B 缺少對應 predicate / evidence route。

要求：

```text
source_q4 = Y
target_q4 = U
reason = MAPPING_INFORMATION_INSUFFICIENT
```

而不是：

```text
claim_became_false = true
```

---

# 96. Unit Test 5：Mapping-Induced B

A 中：

\[
P_1=Y,
\]

\[
P_2=N.
\]

B 將：

\[
P_1,P_2
\]

合併為：

\[
P.
\]

要求：

```text
target_q4 = B
conflict_origin = MAPPING_COLLAPSE
```

---

# 97. Unit Test 6：History Loss

A：

\[
H=(Y,N,Y).
\]

B bridge 只傳 current state。

要求：

```text
current_preserved = true
again_preserved = false
history_loss = true
```

---

# 98. Unit Test 7：Round Trip

A：

\[
X_1.
\]

A→B：

\[
X_1\mapsto X.
\]

B→A：

\[
X\mapsto\{X_1,X_2\}.
\]

要求：

```text
round_trip_exact = false
reconstruction_set_size = 2
```

---

# 99. Unit Test 8：Semantic Reinterpretation

相同 surface label：

\[
X_A=X_B
\]

但：

\[
\rho_A\neq\rho_B.
\]

要求：

```text
surface_equal = true
bridge_type = REINTERPRET
semantic_preserved = false
```

---

# 100. Unit Test 9：Incomparable

A 的 query 依賴 distinction：

\[
R_A
\]

而 B 沒有任何可表達對應。

要求：

```text
query_mapping = UNAVAILABLE
comparison_status = INCOMPARABLE_FOR_QUERY
```

不是：

```text
answer = false
```

---

# 101. Unit Test 10：Domain Again

歷史：

\[
J_A
\rightarrow
J_B
\rightarrow
J_A.
\]

要求：

\[
AgainDomain_{J_A}=1.
\]

但若 round trip 有 loss：

```text
domain_return = true
information_reset = false
```

---

# 102. Unit Test 11：Bridge Version Drift

同一 source state：

\[
K_A.
\]

使用：

\[
M_1
\]

和：

\[
M_2
\]

得到不同 target state。

要求：

```text
bridge_drift = true
historical_records_keep_original_bridge_version = true
```

---

# 103. Unit Test 12：Exact Match 不等於 Same Individual

source / target concepts 被標為 exact conceptual match，

但 object anchors 不同。

要求：

```text
concept_match = EXACT
object_identity = NOT_ESTABLISHED
```

這避免把概念對應偷換成 individual identity。

---

# 104. 與 Institution Theory 的學術位置

Institution Theory 已提供跨 signatures / logics 的 satisfaction-preserving translation 抽象，並有長期 algebraic-specification 與 heterogeneous-logic 應用。近年亦已有 Coq 中的 institution-theoretic formalization。

因此本文不宣稱：

- 首次提出 logic translation；
- 首次提出 truth-preserving translation；
- 首次提出 satisfaction condition。

本文借用其啟發建立：

\[
\boxed{
\text{formal-truth-preservation lane}
}
\]

作為某些 Judgment Domain bridges 的強驗證方式。

---

# 105. 與 Abstract Interpretation 的學術位置

Abstract Interpretation 與 Galois connections 已成熟研究 abstraction / concretization、sound approximation 與 mechanized semantics；2026 年也仍有工作從 proof theory 角度研究 abstraction 所保留的 logical connectives 與 proof rules。

因此本文不宣稱：

- 首次提出 lossy abstraction；
- 首次提出 Galois connection；
- 首次提出 sound projection。

本文借用其核心精神區分：

\[
\boxed{
\text{lossy but sound}
}
\]

與：

\[
\boxed{
\text{incorrect mapping}.
}
\]

---

# 106. 與 Ontology Mapping / SKOS 的學術位置

OWL / SKOS 已提供多種不同強度的 identity / equivalence / mapping relations。

因此本文不宣稱：

> 跨 ontology mapping 不只有一種。

本文較窄的工作是把 mapping strength 接到：

\[
\boxed{
\Psi,\Phi,\Gamma,\nu,E,H
}
\]

的 DTIL information-state object，

並把 loss / gain / history / Q4 effect 一併記錄。

---

# 107. 本篇八個核心結果

### Result 1

\[
\boxed{
\text{cross-domain transfer}
\neq
\text{copy}.
}
\]

### Result 2

\[
\boxed{
\text{bridge type must be explicit}.
}
\]

### Result 3

\[
\boxed{
\text{preservation is query-relative}.
}
\]

### Result 4

\[
\boxed{
\text{truth preservation}
\neq
\text{information preservation}.
}
\]

### Result 5

\[
\boxed{
\text{difference}
\neq
\text{loss}
\neq
\text{error}.
}
\]

### Result 6

\[
\boxed{
\nu_A=\mathbf Y
\not\Rightarrow
\nu_B=\mathbf Y.
}
\]

Q4 state 不能無條件跨域複製。

### Result 7

\[
\boxed{
\text{endpoint preservation}
\not\Rightarrow
\text{history preservation}.
}
\]

### Result 8

\[
\boxed{
\text{cross-domain route itself is part of information history}.
}
\]

---

# 108. 研究邊界

本文不主張：

1. 所有 Judgment Domains 都能建立 formal bridge；
2. 所有 bridge 都可被完整驗證；
3. query-relative preservation 足以描述所有語義保真；
4. Galois connection 適合所有跨域映射；
5. OWL / SKOS mapping relations 等同 DTIL bridge types；
6. information loss 可以永遠量化成單一 scalar；
7. target gain 一定是真正新資訊；
8. round-trip success 等同 semantic identity；
9. INCOMPARABLE 是永久狀態；
10. 本文已建立完整 category-theoretic domain-bridge algebra。

本文建立的是：

\[
\boxed{
\text{a typed cross-judgment-domain mapping layer for DTIL}.
}
\]

---

# 109. 結論：信息穿越判定域，不是搬家，而是經過一座橋

Series II / Paper I 讓同一命題可以在不同：

\[
\mathcal J
\]

下有不同局部資訊狀態。

Paper II 加入歷史：

\[
Once,\ Still,\ Again.
\]

Paper III 區分：

\[
\text{Q4 state change}
\]

與：

\[
\text{reclassification}.
\]

Paper IV 把：

\[
\text{transition boundary}
\]

本身變成資訊物件。

Paper V 現在進一步指出：

\[
\boxed{
\text{information crossing a judgment domain boundary must pass through a typed bridge}.
}
\]

所以：

\[
\mathcal J_A
\rightarrow
\mathcal J_B
\]

不再被理解成：

> 把 A 的答案複製到 B。

而是：

\[
\boxed{
K_A
\xrightarrow{
\mathcal B_{A\to B}
}
K_B,
}
\]

其中 bridge 必須回答：

> 哪些 object 被視為同一個？  
> 哪些語義被保留？  
> 哪些 class 被 split / merge？  
> 哪些 query 還能問？  
> Q4 state 是否仍有相同意義？  
> history 能不能重建？  
> 有哪些 distinction 被壓掉？  
> 目標域新增了什麼？  
> 能不能回到來源？  
> 回去後還是不是原來那個資訊狀態？

因此：

\[
\boxed{
\text{a successful crossing}
}
\]

不等於：

\[
\boxed{
\text{a lossless crossing}.
}
\]

最強的 bridge 可以滿足：

\[
\text{truth preservation},
\]

甚至：

\[
\text{query preservation},
\]

但仍可能不保存：

\[
\text{history},
\quad
\text{provenance},
\quad
\text{intensional distinction}.
\]

而最弱的情況甚至應允許：

\[
\boxed{
INCOMPARABLE.
}
\]

也就是：

> 不是「翻譯失敗所以硬猜」，而是承認目前沒有一座足以支撐該比較的橋。

因此本文最終把「信息從一個判定域進入另一個判定域」收斂成：

\[
\boxed{
\text{Crossing}
=
\text{Mapping}
+
\text{Preservation}
+
\text{Loss/Gain}
+
\text{Verification}
+
\text{History}.
}
\]

這讓判定域本身不再只是靜態 context，

而形成：

\[
\boxed{
\text{a network of partially connected information spaces}.
}
\]

下一篇將進入 **Series II / Paper VI：MIF Historical Composition and Unbounded State Configurations**，把目前：

\[
Q4
+
Again
+
Reclassification
+
Boundary
+
Domain Crossing
\]

正式組合成長程歷史：

\[
\boxed{
\mathcal H
=
(
\Sigma_0,
\mathcal T_1,
\Sigma_1,
\mathcal T_2,
\ldots
)
}
\]

並處理：

- repeated reversal；
- recurrence；
- LOOP；
- stabilization；
- domain cycling；
- semantic drift accumulation；
- potentially unbounded historical configurations。

---

## 參考文獻

W3C. *OWL 2 Web Ontology Language Structural Specification and Functional-Style Syntax (Second Edition)*.

W3C. *OWL 2 Web Ontology Language RDF-Based Semantics (Second Edition)*.

W3C. *SKOS Simple Knowledge Organization System Reference*.

Reynolds, C., & Monahan, R. (2024). *Reasoning about logical systems in the Coq proof assistant*. Science of Computer Programming, 233, 103054.

Goguen, J. A., & Burstall, R. M. (1992). *Institutions: Abstract Model Theory for Specification and Programming*. Journal of the ACM.

Darais, D., & Van Horn, D. (2015). *Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory*. arXiv:1511.06965.

D'Silva, V., Palmigiano, A., Tzimoulis, A., & Urban, C. (2026). *A Proof-Theoretic Approach to Abstract Interpretation*. arXiv:2605.26591.

Kent, R. E. (2024). *Truth Factors*. arXiv:2404.14470.

Jiménez-Ruiz, E., Agibetov, A., Chen, J., Samwald, M., & Cross, V. (2020). *Dividing the Ontology Alignment Task with Semantic Embeddings and Logic-based Modules*. arXiv:2003.05370.