定理证明中的结构：分析与改进 Isabelle 形式化证明档案
计算机科学中的逻辑
2022-09-28 v1
摘要
Isabelle 形式化证明档案在过去几年中已增长到相当可观的规模。它构成了一个令人印象深刻的研究体系，使得针对定理证明中诸多方面的若干统计方法成为可能，且尚未被充分利用。然而，日益增长的规模也带来了一些亟待应对的挑战：素材变得愈发难以查找，可复用性与易理解性变得更为重要。本论文摘要总结了我在这些主题上的研究计划，并简要提及初步结果，表明该档案依赖图的节点入度遵循无标度分布。
引用
@article{arxiv.2209.13305,
title = {Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs},
author = {Fabian Huch},
journal= {arXiv preprint arXiv:2209.13305},
year = {2022}
}
备注
Extended abstract