arXiv cs.AI· Hans-Martin Will·· 12 小时前AI 评分18
Eigenius：面向构造性机构（constructive institutions）的类型化知识存储理论
Typed Knowledge over Constructive Institutions
AI 导读
该著作提出 Eigenius——一种建立在构造性机构之上的类型化知识存储理论，其核心是一个带累积宇宙、命题内涵宇宙、归纳族和内涵恒等类型的依赖类型理论。与数学或程序验证中只需命题成立不同，Eigenius 将证明无关性设为带显式见证的公理而非转换规则，从而保留"谁在何种假设下、通过何种推导或外部工具确立该主张"的记录。
正文 · 原文
Abstract:Type theories designed for mathematics or program verification need only that a proposition holds; proof irrelevance in conversion erases, at the kernel level, how a claim was established. A persistent knowledge store, by contrast, must retain that record: who established a claim, by which derivation or external tool, and under which assumptions. This volume presents the theory of Eigenius---a store of typed knowledge over constructive institutions---and develops its metatheory from that requirement.
The kernel theory is a dependent type theory with cumulative universes, an impredicative universe of propositions, inductive families, and an intensional identity type. Proof irrelevance is an axiom with an explicit witness rather than a conversion rule, so proofs of a proposition are provably equal yet remain distinct terms. Definitional equality is joinability under an orthogonal rewriting system---confluent, injective on type formers, and decidable by a type-free test---while a separate subsumption judgment covers universe cumulativity, codomain-covariant function types, and declared class inclusions.
We prove consistency via a set-theoretic model; develop a justification logic over the kernel's propositions to track evidence and support; organize environments as an institution so that store extensions are signature morphisms and external verdicts enter via comorphisms; formulate a typed knowledge-graph theory with records, classes, and refinements; and prove the correctness of conversion, normalization by evaluation, and bidirectional type checking relative to termination. A Lean 4 formalization accompanies the volume.
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Databases (cs.DB) |
| ACM classes: | F.4.1; I.2.3; I.2.4 |
| Cite as: | arXiv:2611.07432 [cs.LO] |
| (or arXiv:2611.07432v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2611.07432 arXiv-issued DOI via DataCite (pending registration) |
|
| Related DOI: | https://doi.org/10.5281/zenodo.23964990
DOI(s) linking to related resources |
Submission history
From: Hans-Martin Will [view email]
[v1]
Thu, 5 Nov 2026 04:28:30 UTC (213 KB)
来源：arXiv cs.AI · arxiv.org