Megalodon 1.3 and Ramsey Problems

by Brown, Monday, December 28, 2020, 18:33 (272 days ago)

Here is Megalodon 1.3:

http://grid01.ciirc.cvut.cz/~chad/megalodon-1.3.tgz

I added a new theory (HOTG in Egal style) and made it the default. Megalodon can still be used to create documents in the "HOTG in Mizar style" theory by using the -mizar command line argument. I ported the files in form100p1 over to the HOTG-Egal theory.

In examples/egal there are formulations of Ramsey problems. These could be good candidates for bounties. I went ahead and proved the easiest nontrivial cases, namely that R(3,3) > 5 and R(3,3) <= 6 (so, R(3,3) = 6). I wrote a description available here:

http://grid01.ciirc.cvut.cz/~chad/mgpfgramsey.pdf

Megalodon 1.3 and Ramsey Problems

by BlakeKeiller, Tuesday, December 29, 2020, 08:55 (272 days ago) @ Brown

The Ramsey problems do look like good candidates for bounties.

I skimmed through the pdf and found two errors:

On Page 4 just before Section 3 begins you write "R(m,n) < K" where you clearly mean "R(m,n) > K".

On Page 11 you write "Our witness the existence of a clique ..." which seems to have a missing word?

Megalodon 1.3 and Ramsey Problems

by Brown, Tuesday, December 29, 2020, 13:31 (271 days ago) @ BlakeKeiller

Thanks. I corrected the typos you found.

RSS Feed of thread
powered by my little forum