HOL4 Theorems
收藏arXiv2025-09-30 收录
下载链接：
http://cl-informatik.uibk.ac.at/users/tgauthier/tactictoe/
下载链接
链接失效反馈官方服务：
资源简介：
该数据集包含了7902个在HOL4证明助手中证明的定理，用于训练和验证TacticToe方法。其中，数据集不仅包括了一个较小的训练集，包含了860个定理，还包含了一个更大的验证集，用于测试不同策略的性能。该数据集的规模较大，共有7902个定理，其任务是自动定理证明。
This dataset contains 7902 theorems formally proven in the HOL4 proof assistant, which is used for training and validating the TacticToe method. Specifically, it includes not only a smaller training set with 860 theorems, but also a larger validation set for evaluating the performance of different strategies. With a total of 7902 theorems, this dataset is tailored for the task of automated theorem proving.
提供机构：
University of Innsbruck
