Eigenius：基于构造性机构的有类型知识库理论
Typed Knowledge over Constructive Institutions
AI 导读
arXiv 论文提出 Eigenius——一个建立在构造性机构之上的有类型知识存储理论。其内核是带累积宇宙、非直谓命题宇宙、归纳族与内涵恒等类型的依赖类型论，证明无关性作为带显式见证的公理而非转换规则，从而保留命题由谁、以何种推导及何种假设建立。论文给出集合论模型一致性证明、证据追踪论证逻辑、知识图谱理论及转换与双向类型检查正确性证明，并附 Lean 4 形式化。
正文 · 原文
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