Email Gateway (Aug 18 2022 at 20:24): Email Gateway (Aug 18 2022 at 20:24):From: John Munroe <munddr@gmail.com>
Hi,
I had a conversation with someone at a conference re. why most HO
provers need interaction and their reason was that because HO
unification is undecidable. My impression always has been that it's
because HO logic is undecidable and not because the unification is
undecidable. Interaction is needed to make the problem simpler.
Am I missing something completely?
Cheers!
John
Email Gateway (Aug 18 2022 at 20:24):From: Lawrence Paulson <lp15@cam.ac.uk>
Indeed, the validity problem is undecidable even in pure first-order logic. Most automatic theorem provers for first-order logic are complete, which means that if your conjecture is a theorem, you simply have to wait for the proof. However, you may have to wait until the sun grows into a red giant, engulfing the Earth. Or you could guide the proof interactively.
Very few higher-order interactive theorem provers use higher-order unification anyway. It is much more commonly found in automatic provers. So your informant is 100% wrong.
Larry Paulson
Last updated: Apr 26 2024 at 04:17 UTC