arXiv cs.AI· Hans-Martin Will·· 11 小时前AI 评分18
Eigenius：面向构造性机构（constructive institutions）的类型化知识存储理论
Typed Knowledge over Constructive Institutions
AI 导读
该著作提出 Eigenius——一种建立在构造性机构之上的类型化知识存储理论，其核心是一个带累积宇宙、命题内涵宇宙、归纳族和内涵恒等类型的依赖类型理论。与数学或程序验证中只需命题成立不同，Eigenius 将证明无关性设为带显式见证的公理而非转换规则，从而保留"谁在何种假设下、通过何种推导或外部工具确立该主张"的记录。
正文 · AI 翻译
摘要：为数学或程序验证设计的类型理论只要求命题成立；转换中的证明无关性在内核层面抹去了主张是如何被确立的。相比之下，持久的知识存储必须保留这一记录：谁确立了某一主张、通过何种推导或外部工具、以及在哪些假设之下。本卷呈现 Eigenius 的理论——一个基于构造性制度的类型化知识存储——并从这一需求出发发展其元理论。
内核理论是一个依赖类型理论，具有累积宇宙、命题的非直谓宇宙、归纳族和内涵同一类型。证明无关性是一条带有显式见证的公理，而非转换规则，因此一个命题的证明可证相等，却仍是不同的项。定义相等性是在正交重写系统下的可连接性——合流、在类型构造子上单射、且可由无类型测试判定——而一个独立的包含判断涵盖宇宙累积性、余域协变的函数类型以及已声明的类包含。
我们通过集合论模型证明一致性；在内核的命题之上发展一种辩护逻辑以追踪证据与支持；将环境组织为一个制度，使存储扩展成为签名态射，外部裁决通过余态射进入；构建一个具有记录、类和细化的类型化知识图理论；并证明转换、按值求值归一化和双向类型检查相对于终止性的正确性。本卷附有 Lean 4 形式化。
| 主题： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI）；数据库（cs.DB） |
| ACM 分类： | F.4.1；I.2.3；I.2.4 |
| 引用为： | arXiv:2611.07432 [cs.LO] |
| （或 arXiv:2611.07432v1 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2611.07432 由 DataCite 颁发的 arXiv DOI（待注册） |
|
| 相关 DOI： | https://doi.org/10.5281/zenodo.23964990
链接到相关资源的 DOI |
提交历史
来自：Hans-Martin Will [查看电子邮件]
[v1]
2026年11月5日星期四 04:28:30 UTC（213 KB）
来源：arXiv cs.AI · arxiv.org