From: Lawrence Paulson <lp15@cam.ac.uk>
We have an interesting new entry which can be seen as an extension to the previous entry, by Ketland, on the “curious inference” of George Boolos. Where Ketland had done the proofs manually, here we find that sledgehammer alone, with the merest of hints, can prove these rather peculiar formulas.
https://www.isa-afp.org/entries/Boolos_Curious_Inference_Automated.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC