提出Eigenius类型化知识库理论并附Lean形式化
热点事件持续更新
提出Eigenius类型化知识库理论并附Lean形式化
1 篇报道1 个报道来源3 小时前更新
先了解这件事
AI 综述
Hans-Martin Will 在 arXiv（2611.07432）发布论文，提出建立在构造性机构之上的 Eigenius 有类型知识存储理论，并附 Lean 4 形式化。 该理论内核是带累积宇宙、非直谓命题宇宙、归纳族与内涵恒等类型的依赖类型论；证明无关性被作为带显式见证的公理而非转换规则，从而保留命题由谁、以何种推导及何种假设建立。论文给出基于集合论模型的一致性证明，以及证据追踪论证逻辑、知识图谱理论和转换与双向类型检查的正确性证明。
AI 根据报道生成 · 2 小时前更新
最新进展11月6日 13:00
Eigenius：基于构造性机构的有类型知识库理论报道时间线
沿着报道，了解事件的不同侧面。
11月6日
- arXiv cs.AIEigenius：基于构造性机构的有类型知识库理论
arXiv 论文提出 Eigenius——一个建立在构造性机构之上的有类型知识存储理论。其内核是带累积宇宙、非直谓命题宇宙、归纳族与内涵恒等类型的依赖类型论，证明无关性作为带显式见证的公理而非转换规则，从而保留命题由谁、以何种推导及何种假设建立。论文给出集合论模型一致性证明、证据追踪论证逻辑、知识图谱理论及转换与双向类型检查正确性证明，并附 Lean 4 形式化。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。