Simple Dataset for Proof Method Recommendation in Isabelle/HOL

本数据集名为‘Simple Dataset for Proof Method Recommendation in Isabelle/HOL’，由捷克技术大学和因斯布鲁克大学的Yutaka Nagashima创建。数据集包含425,334条关于证明方法应用的数据，每条数据附带超过100个提取特征，无需逻辑领域专业知识即可处理。创建过程涉及应用113个断言到证明方法调用，构建数据集以支持机器学习算法预测Isabelle/HOL中的证明方法。该数据集主要应用于机器学习领域，旨在通过预测合适的证明方法，辅助用户在Isabelle/HOL中进行有效的证明。

This dataset, named "Simple Dataset for Proof Method Recommendation in Isabelle/HOL", was developed by Yutaka Nagashima from Czech Technical University and University of Innsbruck. It contains 425,334 records of proof method applications, with each record accompanied by over 100 extracted features and can be processed without specialized expertise in the field of logic. The dataset construction involved applying 113 assertions to proof method calls, and it was built to support machine learning algorithms in predicting proof methods within Isabelle/HOL. Primarily applied in the machine learning domain, this dataset aims to assist users in conducting effective proofs in Isabelle/HOL by predicting appropriate proof methods.