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.