Re: [isabelle] novice (first year undergrad) learning time



Yes yes yes! A machine proof is much easier if you already understand the intuition behind the traditional proof. It is a myth that machine assistance can replace the need for competence and understanding. The machine magnifies competence, but it also magnifies incompetence...

Larry Paulson


On 21 Feb 2007, at 21:22, Robert Lamar wrote:

This is something I missed almost completely for
the longest time, but which is being corrected now in my work as a PhD
student.  When one is trying to develop proofs in Isabelle and other
proof assistants, it is very desirable to model the proof structure upon
an existing, natural-language proof.






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