Re: [isabelle] question



For my Master's thesis, I formalized in Isabelle a proof of the
independence of the equivalent of the parallels postulate in Tarski's
axioms of geometry [1].  That would have been far too big to do by hand
first (at least at the speed I write).  But when I couldn't easily keep
a part of the proof in my head all at once, I'd draw myself a map of
which lemmas were required to prove which other lemmas, and then I could
concentrate one at a time on any lemma such that all of the lemmas it
depended on had already been formalized.  I've attached a couple of
examples.  Having said that, I did do pen-and-paper working for some of
the lemmas mentioned on those pages, though many of them went straight
from my head into Isabelle, probably including some that were never even
mentioned on the map.

This suited my style well, but I suspect that the best strategy is
highly dependent on the style of the person using it.  For me, I
naturally tend to write proofs in more detail than most, so writing
proofs for Isabelle wasn't as much of a hurdle as it probably is for
some other people.  And I grew up with computers, too; I often feel more
comfortable writing a letter on a computer, rather than writing it by
hand, but some people prefer to write by hand first, even if they're
going to type up the result in the end.

Tim
<><

[1] http://afp.sourceforge.net/entries/Tarskis_Geometry.shtml

On 25/01/14 05:54, John Wickerson wrote:
> Hi all,
> 
> I wonder if I might invite comment on the following statement?
> 
> "Don't even *think* about firing up Isabelle until you've completed a really solid pencil-and-paper proof of the theorem you want to mechanise."
> 
> Thanks!
> John
> 

Attachment: IMG_20140125_125138.jpg
Description: JPEG image

Attachment: IMG_20140125_125401.jpg
Description: JPEG image

Attachment: signature.asc
Description: OpenPGP digital signature



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