Megalodon 1.0

by Brown, Monday, September 14, 2020, 16:09 (447 days ago)

I'm releasing a first version of Megalodon today:

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

Megalodon is an interactive theorem prover/proof checker and is essentially an updated Egal. One of the main updates is that Megalodon can produce Proofgold documents. But default the documents are in the HF set theory, but with the -mizar command line argument it switches to Mizar's TG set theory and with the -hoas command line argument it switches to the HOAS theory.

There are two examples of solutions to reward bounties in HF, one small Mizar related example, and a few HOAS examples. Details are in examples/README. Until Proofgold is linked up with some ATPs probably the easiest way to resolve reward bounty conjectures is interactively using Megalodon. That is, the user does the proof and Megalodon checks and (if it's correct) creates the Proofgold document. Once you have the Proofgold document, the instructions from this earlier post applies:

https://proofgold.org/forum/index.php?id=43