Hans-Martin Will提出Eigenius类型化知识存储理论

1. 12:28
   arXiv · cs.AI

   Eigenius：面向构造性机构的类型化知识存储理论

   Eigenius 提出一种面向构造性机构的类型化知识存储理论，其内核为带累积宇宙、命题不可预测宇宙、归纳族和内涵身份类型的依赖类型理论。证明不可相关性以带显式见证的公理形式存在而非转换规则，使命题的证明可证相等却仍是不同项；定义等价性基于正交重写系统的可连接性，一致性经集合论模型证明。该理论还包含追踪证据与支持的 justification logic、以机构组织环境使存储扩展成为签名态射、带记录/类/细化的类型化知识图谱理论，并附 Lean 4 形式化。

趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。