Second Proposal for Reward Bounties

by Brown, Tuesday, October 27, 2020, 13:20 (404 days ago) @

The HOL4 translation worked fine for over 90% of the GRUNGE examples. I essentially use the "set style" TH0 translation with some minor modifications (no special types, and so on). There were some other choices I made that seemed appropriate here: translating the "ind" type to the set "omega" (any infinite set would work), the SELECT operator using the choice operator on sets, and so on.

If you're interested, you could pick a HOL4 theorem you're familiar with and look at the translation and see if you think it looks right to you.

For each one I'm (currently) including there are several files: Megalodon, Proofgold, tex, pdf. The latex/pdf are automatically generated, so they're not very pretty.

Here's an example from "bool":

http://grid01.ciirc.cvut.cz/~chad/hol4_bushy_mg/thm_2Ebool_2ECOND__ID/

Looking again to find an example, there are a lot of (probably) easy ones from bool that could be left out. COND__ID requires the work of unwinding the definition of COND. Other examples like PEIRCE are just trivial.

http://grid01.ciirc.cvut.cz/~chad/hol4_bushy_mg/thm_2Ebool_2EPEIRCE/