Re: [isabelle] Automation is awesome; one bibliography leads to another



Proof assistants are not the opposite of automatic provers.
Ideally, and Isabelle approaches this ideal, a proof assistant should let
you choose where you want to write your proof in detailed steps and which
bits you want to fob off to an automated prover.
That is, within an interactive proof assistant, you can take the option at
any point of saying "and solve this trivial bit of grunge work/similar
case/uninteresting lemma automatically".

The reality these days is that there are still lots of places where we
might want to use automation but it is lacking; however it's always getting
better, especially as more powerful automatic tools are integrated into
proof assistants.

The educational content of a formal development does not need to reside in
explicit proof steps.
I'd say in any development involving more than 2 or 3 major theorems, it is
the *statements of the lemmas* which are used (by automatic tactics) in the
proofs of the major theorems that offer the most educational content.
The lemmas and the overall structure of the big proofs are the interesting
story.
The rest can be handed over to automation to whatever extent it can cope.

On Thu, May 31, 2012 at 1:47 AM, <gottfried.barrow at gmx.com> wrote:

> This comment falls under the "Dude, this is awesome" category, and no
> reply is needed. I try to keep my comments to a minimum, but I make this
> one.
>
> Bibliographies leading to bibliographies led me to Blanchett's "Automatic
> Proofs and Refutations for Higher-Order Logic" <http://www4.in.tum.de/%**
> 7Eblanchet/ <http://www4.in.tum.de/%7Eblanchet/>>.
>
> There are developers of other provers who listen in, so this comment could
> also serve as a feature request from one user, me, for their products.
>
> I've said that I don't care about automatic proving. For my purposes,
> whatever I prove I have to understand, so automatic proving doesn't help me
> unless I can be shown the automatic prover's proof, and understand the
> details, or have a general idea of what the prover did. My intended
> audience, by and large, also won't be impressed by automatic proofs. There
> has to be educational content in the details of my proofs, where the amount
> of detail has to be balanced (which, of course, requires some auto
> proving), but where there isn't a total absence of details.
>
> On the other hand, as to counterexamples, there's no requirement that I
> understand anything other than that the counterexample has proven me wrong,
> so I'll be keeping in mind the Isabelle tools that will look for
> counterexamples. As Blanchett says,
>
>    Novices and experts alike can enter invalid formulas and find
> themselves wasting hours
>    (or days) on an impossible proof; once they identify and correct the
> error, the proof is often easy.
>
> I saw in the past a little of the results of Quickcheck, but I had
> forgotten about the counterexample tools.
>
> But back to automatic proving, I'm sure it'll come in handy when I have
> "The Important Promising Conjecture", or even under less important
> circumstances. What I think I don't want, I sometimes do want.
>
> Power is whatever you need. I had a mini-debate with someone who had no
> sympathy with the idea that I needed a proof assistant instead of an
> automatic prover. Power to him was automatic proving. Power to me was being
> able to specify the proof steps. I guess both are powerful, since both take
> a massive amount of work to implement.
>
> --GB
>




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