The MPTP2078 benchmark

The MPTP2078 benchmark is a collection of 2078 ATP problems generated from MML by the MpTP02 system.

The benchmark was created as follows: The 33 Mizar articles from which problems were previously selected for constructing the MpTPChallenge are used. Instead of just the 252 problems used in the MpTPChallenge, all problems from these articles are used. This yields 2078 problems. As with the MPTP Challenge benchmark, we create two groups (divisions) of problems: bushy (small versions with just the Mizar-needed premises), and chainy (large version, where all previous knowledge is always available).

-- JosefUrban - 2012-04-05

TopicClassification Select one...

ImplementationDate? N/A
Topic attachments
I Attachment Action Size Date Who Comment
else7z MPTP2078.tar.7z manage 5410.1 K 2012-04-06 - 00:07 JosefUrban MPTP2078 distribution in the 7-zip format
Topic revision: r1 - 2012-04-06 - 00:07:48 - JosefUrban
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback