论文标题
简单的数据集用于证明方法建议在isabelle/hol中推荐（数据集说明）
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
论文作者
论文摘要
最近，越来越多的研究人员应用了机器学习，以协助交互式定理掠夺者的用户。但是，基本的逻辑和证明文件的深奥结构的表现性会阻碍机器学习从业人员在正式逻辑方面通常没有太多专业知识，更不用说伊莎贝尔/Hol，无法在该领域取得大规模的成功。在此数据描述中，我们提供了一个简单的数据集，该数据集包含有关超过400K证明方法应用程序的数据以及每种格式的100多个提取功能，该格式可以轻松处理，而无需任何有关正式逻辑的知识。我们的简单数据格式使机器学习从业人员可以尝试机器学习工具来预测Isabelle/HOL中的证明方法，而无需逻辑领域专业知识。
Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from achieving a large scale success in this field. In this data description, we present a simple dataset that contains data on over 400k proof method applications along with over 100 extracted features for each in a format that can be processed easily without any knowledge about formal logic. Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL without requiring domain expertise in logic.
