Re: [isabelle] Real reason for interaction
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.
On 14 Jun 2012, at 11:45, John Munroe wrote:
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and