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.

Larry Paulson

On 14 Jun 2012, at 11:45, John Munroe wrote:

> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.