Email Gateway (Jan 10 2023 at 14:50): Email Gateway (Jan 10 2023 at 14:50):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: Feb 05 2025 at 16:23 UTC