数据集概述
本数据集为2021年4月16日发布的Isabelle2021版本形式证明档案（Archive of Formal Proofs）的元数据，包含每个条目（entry）的结构化信息，涉及会话名称、标题、作者、日期、主题、摘要等核心属性，为形式化验证研究提供结构化参考资料。
文件详解
- 文件名称：metadata.json
- 文件格式：JSON
- 字段映射介绍：
- session：必填，字符串，Isabelle会话名称
- title：必填，字符串，形式证明档案条目标题
- authors：必填，字符串数组，按提交顺序排列的作者列表
- contributors：可选，字符串数组，贡献者列表
- date：必填，字符串，提交日期（ISO 8601格式YYYY-MM-DD）
- topics：必填，字符串数组，主题列表
- abstract：必填，字符串，条目摘要（可能包含HTML、MathJax和换行符）
- extra：可选，键值对，额外信息（多为变更历史）
- license：必填，字符串，许可协议（BSD或LGPL）
- olderReleases：可选，对象数组，历史版本及对应Isabelle版本
- dependencies：可选，字符串数组，依赖的会话名称
- theories：可选，字符串数组，按执行顺序排列的理论文件列表
数据来源
https://foss.heptapod.net/isa-afp/afp-2021 @ 679cb16760ca490e5bd161495ad9cb5b629d16a6
适用场景
- 形式化验证资源管理：用于Isabelle2021形式证明档案条目的结构化检索与管理
- 形式化证明主题分析：基于topics字段分析形式化证明领域的研究热点分布
- 形式化验证依赖关系研究：通过dependencies字段分析证明条目间的依赖网络
- 形式化验证历史版本追溯：利用olderReleases字段追踪证明条目的版本演进与Isabelle版本适配情况
