The Isabelle Archive of Formal Proofs has grown to a significant size in the past years. It makes up for an impressive body of research, which enables a number of statistical approaches to various aspects in theorem proving, and has not yet been utilized exhaustively. However, the growing size also poses some challenges to address: Material becomes increasingly harder to find, reusability and ease of understanding become more important. This thesis abstract summarizes my research plans on those topics and briefly touches on preliminary results, which indicate that the node in-degree of the dependency graph of the archive follows a scale-free distribution.
翻译：过去几年来,伊莎贝尔正式证据档案已发展到相当大的规模,它构成大量令人印象深刻的研究,使许多统计方法能够证明理论的各个方面,但尚未加以详尽利用,然而,日益扩大的规模也带来了一些需要应对的挑战:材料越来越难找到,可恢复性和理解的便利性越来越重要。这个理论摘要概述了我关于这些专题的研究计划,并简要地介绍了初步结果,这表明档案依赖度图的节点在无比例分布之后。
相关内容
微信扫码咨询专知VIP会员