Re: [isabelle] question



Hi,

Am Freitag, den 24.01.2014, 16:54 +0000 schrieb John Wickerson:
> 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."

it is certainly good advice, but Isabelle has its merits also when
exploring and finding a proof. One could also say

        „Don’t even *think* about completing as solid pencil-and-paper
        proof of your theorem until you have finalized your
        formalisation, your definition, and your theorem.“

Because when you change some of these, fixing a pencil-and-paper-proof
is tedious and error-prone, while Isabelle will easily tell you where
you need to adjust stuff.

So while there were certainly cases where I should have worked on paper
before, I would not make it an absolute rule.

Also, depending on your hand writing, there are good reason to avoid
pen-and-pencil proofs that need to be readable even the next day :-)

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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