Mizar CNF Problems and Prover9 Proofs

by Brown, Sunday, September 05, 2021, 11:49 (22 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.

Mizar CNF Problems and Prover9 Proofs

by BlakeKeiller, Sunday, September 05, 2021, 20:17 (21 days ago) @ Brown

I've downloaded it and had a quick look. I'll consider it. It's good timing in two ways: First, it's been roughly 1500 blocks since the last time I distributed bounty fund rewards, so it would be easy to put roughly 25 bars as a bounty on this many problems. Second, I had already prepared more Category Theory problems and was planning to distribute bounties to those today (after spending the weekend publishing the corresponding documents). I'd really rather give preference to problems chosen by someone else. I want to spend more time looking at the Mizar CNF dataset before deciding for sure though. I'll post here if I have questions or find potential issues.

Mizar CNF Problems and Prover9 Proofs (1439 New Bounties)

by BlakeKeiller, Sunday, September 12, 2021, 16:32 (14 days ago) @ BlakeKeiller

The problems look good to me. One minor thing I noticed: the clauses are reversed from the .cnf file to the .mg file. The order doesn't matter, of course, but just in case someone else is trying to see the correspondence I thought I'd point it out.

This weekend I used the bounty fund to place a bounty of (almost) 25 bars on each of these 1436 problems. For people who want to solve some of them, I'd suggest downloading the .tgz file in the OP and trying to use Prover9 and the distributed lisp files to obtain a Megalodon proof and then use Megalodon to obtain a Proofgold proof.

There are roughly 3800 blocks remaining during the phase where 25 bars of the reward goes into the bounty fund. More suggestions for problems to place bounties on are welcome.

Mizar CNF Problems and Prover9 Proofs (1439 New Bounties)

by Brown, Monday, September 13, 2021, 19:00 (13 days ago) @ BlakeKeiller

I used reportbounties to get a list of all bounties to doublecheck the bounties are there. They are, but I noticed some problems had multiple 25 bar bounties. I now realize this happened because 18 of the 1439 problems are duplicates. To be specific 7 addresses correspond to 2 problems each and 1 address corresponds to 4 problems. I didn't think to check for this before, but it's only a few cases so I suppose it's not a huge deal. Essentially there are only 1429 problems. Here is a list of the 8 addresses with the multiple bounties and a list of the Mizar problems they were derived from.

TMZPAPyEPS2GSQjei1QuePMKCa7TyyrZ5LW: t6_cat_3 t7_cat_3
TMHf56pApyotpY8gCP4bupxVi8DUpVHhmci: t8_complex2 t9_complex2
TMYojCRLszJwjbrkaAkLcncph364s5kmzbJ: t80_transgeo t51_transgeo
TMXeAgzusRtUTzsYk3AdMwsBvZ8ctA1FsET: t48_transgeo t75_transgeo
TMRXVZNXJVHJmuCnpoyvfY5hUPG8PZ9cJLp: t49_sin_cos3 t47_sin_cos3
TMZUqc5UpZHn6b2goxw31ZE6HtEKzdh2EYb: t47_yellow_4 t20_yellow_4
TMQco5oyqUAmmJMfsUmVPeWQusKwbwovorW: t25_tex_4 t26_tex_4
TMJBwMsMMNr2Svj6GbTq3jFce1E7H9mqmuE: t42_tdlat_1 t43_tdlat_1 t39_tdlat_1 t40_tdlat_1

RSS Feed of thread
powered by my little forum