Mizar CNF Problems and Prover9 Proofs

by Brown, Sunday, September 05, 2021, 11:49 (91 days ago)

Here is a tgz file with 1436 problems that could be interesting candidates for the bounty fund:

http://grid01.ciirc.cvut.cz/~chad/cnf_todo_files.tgz

They come from a dataset of ATP problems originating from the MML (Mizar Mathematical Library). They're in CNF form and have been transformed enough that probably there are no copyright issues. Even if there are, the problems were suggested to me and given to me by the head of the relevant committee, so they're almost certainly safe to use from the copyright point of view. The 1436 problems included here are a subset of 14165 problems that seem to be hard for ATPs. (The 1436 were chosen since the 'obvious' translation of the problem would lead to too many local variables for the other problems. It took me a while to determine this since Proofgold's readdraft command reports that it had trouble normalizing the problems -- which was obviously wrong since there were no betas, etas and no definitions. There should be a clearer failure message in the case where the de Bruijn indices exceed the bound of 90.)

Each problem is a set of first order clauses. The corresponding Megalodon/Proofgold proposition asserts the set of clauses together yield False. As a small example to show how the transformation is done, suppose the set of clauses were

p(a)
-p(X) | p(f(X))
-p(f(a))

then the Megalodon/Proofgold proposition would be

forall p:set -> prop,
forall a:set,
forall f:set -> set,
(~p a -> False)
-> (forall X, p X -> ~p (f X) -> False)
-> (p (f a) -> False)
-> False

The problems have also been converted to Prover9's LADR format. If Prover9 can find a proof, it can transform it to an IVY proof. An IVY proof is detailed enough to produce a Megalodon proof and lisp code to do this is included.

If bounties are placed on these 1436 problems, then people could try to collect the bounties by running Prover9 with different options on the input file. If Prover9 finds a proof, then via IVY a Megalodon proof can be produced. Megalodon can then produce the Proofgold document to publish into the block chain and collect the bounty. This is a realistic workflow for people who would like to take part but for whatever reason do not want to directly prove propositions using Megalodon or modify another prover to produce Proofgold's Curry-Howard style proof terms.

A README in the directory has more information about what is included and how to use it.

Feedback is welcome.