Megalodon 1.3 and Ramsey Problems

by Brown, Monday, December 28, 2020, 18:33 (342 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