Connection Tableau Proofs from Mizar Mathematical Library
收藏arXiv2025-09-30 收录
下载链接：
https://github.com/BartoszPiotrowski/guiding-connection-tableau-by-RNNs
下载链接
链接失效反馈官方服务：
资源简介：
该数据集包含了13,822个由Mizar数学库生成的连接证明，这些证明被翻译成了TPTP语言，并被用于训练递归神经网络（RNNs），以指导连接表格证明计算中的子句选择。该数据集被分为训练集、验证集和测试集，分别占比为0.6、0.1和0.3。规模上，共有13,822个证明和567,273个训练对。所承担的任务是证明计算中的子句选择。
This dataset contains 13,822 connection proofs generated from the Mizar Mathematical Library, which have been translated into the TPTP language. It is used to train Recurrent Neural Networks (RNNs) to guide clause selection in connection tableau proof search. The dataset is split into training, validation, and test sets with respective proportions of 0.6, 0.1, and 0.3. In terms of scale, it includes a total of 13,822 proofs and 567,273 training pairs. The targeted task of this dataset is clause selection in automated proof computation.
提供机构：
Bartosz Piotrowski
