[isabelle] Real reason for interaction


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 MHonArc.